src/Test/elemequalunsattest.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);
  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 }