src/Test/elemequalsattest.cc

   1 #include "csolver.h"
   2 /**
   3  * e1 = {0, 1, 2}
   4  * e2 = {3, 1, 7}
   5  * e1 == e2
   6  *
   7  * Result (Enumeration):
   8  *      e1=1 e2=1
   9  * Result (circuit):
  10  *      e1=0 e2=3
  11  *      e1=1 e2=1
  12  *      e1=2 e2=7
  13  */
  14 int main(int numargs, char **argv) {
  15         CSolver *solver = new CSolver();
  16         uint64_t set1[] = {0, 1, 2};
  17         uint64_t set2[] = {3, 1, 7};
  18         Set *s1 = solver->createSet(0, set1, 3);
  19         Set *s2 = solver->createSet(0, set2, 3);
  20         Element *e1 = solver->getElementVar(s1);
  21         Element *e2 = solver->getElementVar(s2);
  22         Set *domain[] = {s1, s2};
  23         Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
  24         Element *inputs[] = {e1, e2};
  25         BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
  26         solver->addConstraint(b);
  27         solver->serialize();
  28
  29         if (solver->solve() == 1)
  30                 printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
  31         else
  32                 printf("UNSAT\n");
  33         delete solver;
  34 }