test_solver.cc

   1 #include "inc_solver.h"
   2
   3 int main(int argc, char **argv) {
   4   IncrementalSolver * s=new IncrementalSolver();
   5   s->addClauseLiteral(1);s->addClauseLiteral(2);s->addClauseLiteral(0);
   6   s->finishedClauses();
   7   s->freeze(1); s->freeze(2);
   8   printf("solution=%d\n", s->solve());
   9   for(int i=0;i<=2;i++) {
  10     printf("%d: %d\n",i, s->getValue(i));
  11   }
  12   s->addClauseLiteral(-1);s->addClauseLiteral(0);
  13   s->finishedClauses();
  14   printf("solution=%d\n", s->solve());
  15   for(int i=0;i<=2;i++) {
  16     printf("%d: %d\n",i, s->getValue(i));
  17   }
  18   s->addClauseLiteral(-2);s->addClauseLiteral(0);
  19   s->finishedClauses();
  20   printf("solution=%d\n", s->solve());
  21   for(int i=0;i<=2;i++) {
  22     printf("%d: %d\n",i, s->getValue(i));
  23   }
  24   delete s;
  25 }