src/Test/ltelemconsttest.c

   1 #include "csolver.h"
   2
   3 int main(int numargs, char ** argv){
   4         CSolver *solver=allocCSolver();
   5         uint64_t set1[]={5};
   6         uint64_t set3[]={1, 3, 4, 6};
   7         Set * s1=createSet(solver, 0, set1, 3);
   8         Set * s3=createSet(solver, 0, set3, 4);
   9         Element * e1=getElementConst(solver, 4, 5);
  10         Element * e2=getElementVar(solver, s3);
  11         Set * domain2[]={s1, s3};
  12         Predicate *lt=createPredicateOperator(solver, LT, domain2, 2);
  13         Element * inputs2[]={e1, e2};
  14         Boolean *b=applyPredicate(solver, lt, inputs2, 2, NULL);
  15         addConstraint(solver, b);
  16         if (startEncoding(solver)==1)
  17                 printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
  18         else
  19                 printf("UNSAT\n");
  20         deleteSolver(solver);
  21 }