Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler

[satune.git] / src / Test / ordertest.cc

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index e2d974bed1d3893d256d491bcc9fd284a7f9e508..9ffcab56c91acf7efab1f200e02b9a021451c881 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -10,14 +10,21 @@ int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();
        uint64_t set1[] = {5, 1, 4};
        Set *s = solver->createSet(0, set1, 3);
-       Order *order = solver->createOrder(TOTAL, s);
-       Boolean *b1 =  solver->orderConstraint(order, 5, 1);
-       Boolean *b2 =  solver->orderConstraint(order, 1, 4);
+       Order *order = solver->createOrder(SATC_TOTAL, s);
+       BooleanEdge b1 =  solver->orderConstraint(order, 5, 1);
+       BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
        solver->addConstraint(b1);
        solver->addConstraint(b2);
-       if (solver->startEncoding() == 1)
+       solver->serialize();
+       if (solver->solve() == 1){
                printf("SAT\n");
-       else
+               printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
+                       solver->getOrderConstraintValue(order, 5, 1), 
+                       solver->getOrderConstraintValue(order, 1, 4),
+                       solver->getOrderConstraintValue(order, 5, 4),
+                       solver->getOrderConstraintValue(order, 1, 5));
+       } else {
                printf("UNSAT\n");
+       }
        delete solver;
 }