09bc923663df7d8831c47707949d1a44f94b49f2
[satlib.git] / 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 }