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