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 set1[] = {5};
  11         uint64_t set3[] = {1, 3, 4, 6};
  12         Set *s1 = solver->createSet(0, set1, 1);
  13         Set *s3 = solver->createSet(0, set3, 4);
  14         Element *e1 = solver->getElementConst(4, 5);
  15         Element *e2 = solver->getElementVar(s3);
  16         Predicate *lt = solver->createPredicateOperator(SATC_LT);
  17         Element *inputs2[] = {e1, e2};
  18         BooleanEdge b = solver->applyPredicate(lt, inputs2, 2);
  19         solver->addConstraint(b);
  20         solver->serialize();
  21         if (solver->solve() == 1)
  22                 printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
  23         else
  24                 printf("UNSAT\n");
  25         delete solver;
  26 }