src/Test/buildsimple.cc

   1 #include "csolver.h"
   2 #include <unistd.h>
   3
   4 /**
   5  * e1={0, 1, 2}
   6  * e2={0, 1, 2}
   7  * e1 == e2
   8  * e3= e1+e2 {0, 1, 2, 3, 4}
   9  * e4 = f(e1, e2)
  10  *      0 1 => 0
  11  *      1 1 => 0
  12  *      2 1 => 2
  13  *      2 2 => 2
  14  * e3 == e4
  15  * Result: UNSAT!
  16  */
  17 int main(int numargs, char **argv) {
  18         CSolver *solver = new CSolver();
  19         uint64_t set1[] = {1, 2, 3};
  20         Set *s1 = solver->createSet(1, set1, 3);
  21         Set *s2 = solver->createSet(1, set1, 3);
  22         Element *e1 = solver->getElementVar(s1);
  23         Element *e2 = solver->getElementVar(s2);
  24         solver->mustHaveValue(e1);
  25         solver->mustHaveValue(e2);
  26         Element *inputs[] = {e1, e2};
  27
  28         uint64_t set2[] = {3};
  29         Set *rangef1 = solver->createSet(1, set2, 1);
  30         Function *f1 = solver->createFunctionOperator(SATC_ADD, rangef1, SATC_FLAGIFFOVERFLOW);
  31
  32         BooleanEdge overflow = solver->getBooleanVar(2);
  33         Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
  34         Element *e4 = solver->getElementConst(5, 3);
  35         Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS);
  36         Element *inputs2 [] = {e4, e3};
  37         BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
  38         solver->addConstraint(pred);
  39         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, overflow));
  40         if (solver->solve() == 1)
  41                 printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
  42         else
  43                 printf("UNSAT\n");
  44         delete solver;
  45 }