src/Test/ordertest.cc

   1
   2 #include "csolver.h"
   3 /**
   4  * TotalOrder(5, 1, 4)
   5  * 5 => 1
   6  * 1 => 4
   7  * Result: O(5,1)=0 O(1,4)=0 O(5,4)=0 O(1,5)=1 O(1111,5)=2
   8  */
   9 int main(int numargs, char **argv) {
  10         CSolver *solver = new CSolver();
  11         uint64_t set1[] = {5, 1, 4};
  12         Set *s = solver->createSet(0, set1, 3);
  13         Order *order = solver->createOrder(SATC_TOTAL, s);
  14         BooleanEdge b1 =  solver->orderConstraint(order, 5, 1);
  15         BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
  16
  17         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
  18         solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
  19         solver->serialize();
  20         if (solver->solve() == 1){
  21                 printf("SAT\n");
  22                 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
  23                         solver->getOrderConstraintValue(order, 5, 1),
  24                         solver->getOrderConstraintValue(order, 1, 4),
  25                         solver->getOrderConstraintValue(order, 5, 4),
  26                         solver->getOrderConstraintValue(order, 1, 5));
  27         } else {
  28                 printf("UNSAT\n");
  29         }
  30         delete solver;
  31 }