src/Test/incrementaltest.cc

   1 #include "csolver.h"
   2
   3 #define INPUTSIZE 2
   4 #define DOMAINSIZE 3
   5
   6 int main(int numargs, char **argv) {
   7         CSolver *solver = new CSolver();
   8         uint64_t set1[] = {3, 1, 2};
   9         uint64_t set2[] = {3, 1, 7};
  10         Set *s1 = solver->createSet(0, set1, DOMAINSIZE);
  11         Set *s2 = solver->createSet(0, set2, DOMAINSIZE);
  12         Element *e1 = solver->getElementVar(s1);
  13         Element *e2 = solver->getElementVar(s2);
  14         Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
  15         Element *inputs[] = {e1, e2};
  16         BooleanEdge b = solver->applyPredicate(equals, inputs, INPUTSIZE);
  17         solver->addConstraint(b);
  18         solver->freezeElement(e1);
  19         solver->freezeElement(e2);
  20         if (solver->solve() == 1) {
  21                 int run = 1;
  22                 do {
  23                         printf("result %d: e1=%" PRIu64 " e2=%" PRIu64 "\n", run, solver->getElementValue(e1), solver->getElementValue(e2));
  24                         for (int i = 0; i < INPUTSIZE; i++) {
  25                                 uint64_t val = solver->getElementValue(inputs[i]);
  26                                 Element *econst = solver->getElementConst(0, val);
  27                                 Element *tmpInputs[] = {inputs[i], econst};
  28                                 BooleanEdge b = solver->applyPredicate(equals, tmpInputs, INPUTSIZE);
  29                                 solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, b));
  30                         }
  31                         run++;
  32                 } while (solver->solveIncremental() == 1);
  33                 printf("After %d runs, there are no more models to find ...\n", run);
  34         } else {
  35                 printf("UNSAT\n");
  36         }
  37         delete solver;
  38 }