src/Test/constraint.cc

   1 #include "csolver.h"
   2
   3 int main(int numargs, char **argv) {
   4         CSolver *solver = new CSolver();
   5         uint64_t elements[] = {0, 1};
   6         Set *s = solver->createSet(1, elements, 2);
   7         Element *e1 = solver->getElementVar(s);
   8         Element *e2 = solver->getElementVar(s);
   9         Set *sarray[] = {s, s};
  10         Predicate *p = solver->createPredicateOperator(SATC_LT, sarray, 2);
  11         Element *earray[] = {e1, e2};
  12         BooleanEdge be = solver->applyPredicate(p, earray, 2);
  13         solver->addConstraint(be);
  14
  15         if (solver->solve() == 1) {
  16                 printf("SAT\n");
  17         } else {
  18                 printf("UNSAT\n");
  19         }
  20         delete solver;
  21 }