src/Test/ordertest.c

   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=allocCSolver();
  11         uint64_t set1[]={5, 1, 4};
  12         Set * s=createSet(solver, 0, set1, 3);
  13         Order* order = createOrder(solver, TOTAL, s);
  14         Boolean* b1=  orderConstraint(solver, order, 5, 1);
  15         Boolean* b2=  orderConstraint(solver, order, 1, 4);
  16         addConstraint(solver, b1);
  17         addConstraint(solver, b2);
  18         if (startEncoding(solver)==1)
  19                 printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d O(1111,5)=%d\n",
  20                         getOrderConstraintValue(solver, order, 5, 1),
  21                         getOrderConstraintValue(solver, order, 1, 4),
  22                         getOrderConstraintValue(solver, order, 5, 4),
  23                         getOrderConstraintValue(solver, order, 1, 5),
  24                         getOrderConstraintValue(solver, order, 1111, 5));
  25         else
  26                 printf("UNSAT\n");
  27         deleteSolver(solver);
  28 }