src/Test/ltelemconsttest.c

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