src/Test/ltelemconsttest.cc

   1 #include "csolver.h"
   2 /**
   3  * e1 = 5
   4  * e2 = {1, 3, 4, 6}
   5  * e1 < e2
   6  * Result: e1=5 e2=6
   7  */
   8 int main(int numargs, char **argv) {
   9         CSolver *solver = new CSolver();
  10         uint64_t set3[] = {1, 3, 4, 6};
  11         Set *s3 = solver->createSet(0, set3, 4);
  12         Element *e1 = solver->getElementConst(4, 5);
  13         Element *e2 = solver->getElementVar(s3);
  14         Predicate *lt = solver->createPredicateOperator(SATC_LT);
  15         Element *inputs2[] = {e1, e2};
  16         BooleanEdge b = solver->applyPredicate(lt, inputs2, 2);
  17         solver->addConstraint(b);
  18         solver->serialize();
  19         if (solver->solve() == 1)
  20                 printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
  21         else
  22                 printf("UNSAT\n");
  23         delete solver;
  24 }