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 }