e2d974bed1d3893d256d491bcc9fd284a7f9e508
[satune.git] / 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(TOTAL, s);
14         Boolean *b1 =  solver->orderConstraint(order, 5, 1);
15         Boolean *b2 =  solver->orderConstraint(order, 1, 4);
16         solver->addConstraint(b1);
17         solver->addConstraint(b2);
18         if (solver->startEncoding() == 1)
19                 printf("SAT\n");
20         else
21                 printf("UNSAT\n");
22         delete solver;
23 }