Fixing bugs + adding descriptions to test cases
[satune.git] / src / Test / elemequalityunsattest.c
1 #include "csolver.h"
2 /**
3  * e1 = {0, 1, 2}
4  * e2 = {3, 4}
5  * e1 == e2
6  * 
7  * Result: UNSAT
8  */
9 int main(int numargs, char ** argv) {
10         CSolver * solver=allocCSolver();
11         uint64_t set1[]={0, 1, 2};
12         uint64_t set2[]={3, 4};
13         Set * s1=createSet(solver, 0, set1, 3);
14         Set * s2=createSet(solver, 0, set2, 2);
15         Element * e1=getElementVar(solver, s1);
16         Element * e2=getElementVar(solver, s2);
17         Set * domain[]={s1, s2};
18         Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
19         Element * inputs[]={e1, e2};
20         Boolean *b=applyPredicate(solver, equals, inputs, 2, NULL);
21         addConstraint(solver, b);
22         
23         if (startEncoding(solver)==1)
24                 printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
25         else
26                 printf("UNSAT\n");
27         deleteSolver(solver);
28 }