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         Set *domain[] = {s1, s2};
  27         Element *inputs[] = {e1, e2};
  28
  29         uint64_t set2[] = {3};
  30         Set *rangef1 = solver->createSet(1, set2, 1);
  31         Function *f1 = solver->createFunctionOperator(SATC_ADD, domain, 2, rangef1, SATC_FLAGIFFOVERFLOW);
  32
  33         BooleanEdge overflow = solver->getBooleanVar(2);
  34         Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
  35         Element *e4 = solver->getElementConst(5, 3);
  36         Set *domain2[] = {rangef1,rangef1};
  37         Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
  38         Element *inputs2 [] = {e4, e3};
  39         BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);
  40         solver->addConstraint(pred);
  41         solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, overflow));
  42         if (solver->solve() == 1)
  43                 printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
  44         else
  45                 printf("UNSAT\n");
  46         delete solver;
  47 }