Breaking Multituner into comptuner and kmeanstuner

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

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 9ffcab56c91acf7efab1f200e02b9a021451c881..148235adf1f67dc971ab255f626a6a4782ae3aad 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -13,16 +13,17 @@ int main(int numargs, char **argv) {
        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);
+
+       solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
+       solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
        solver->serialize();
-       if (solver->solve() == 1){
+       if (solver->solve() == 1) {
                printf("SAT\n");
-               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));
+               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");
        }