Adding more checks ...

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

diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc
index 646b195feff3ca2050af9a29d4a19ecb4395ad29..fea3a9ff72838807f8c81de2228e67a1e0793411 100644 (file)
--- a/src/Test/ordergraphtest.cc
+++ b/src/Test/ordergraphtest.cc
@@ -1,37 +1,56 @@
 #include "csolver.h"
 
 int main(int numargs, char **argv) {
-       CSolver *solver = allocCSolver();
+       CSolver *solver = new CSolver();
        uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
-       Set *s = createSet(solver, 0, set1, 8);
-       Order *order = createOrder(solver, TOTAL, s);
-       Boolean *o12 =  orderConstraint(solver, order, 1, 2);
-       Boolean *o13 =  orderConstraint(solver, order, 1, 3);
-       Boolean *o24 =  orderConstraint(solver, order, 2, 4);
-       Boolean *o34 =  orderConstraint(solver, order, 3, 4);
-       Boolean *o41 =  orderConstraint(solver, order, 4, 1);
-       Boolean *o57 =  orderConstraint(solver, order, 5, 7);
-       Boolean *o76 =  orderConstraint(solver, order, 7, 6);
-       Boolean *o65 =  orderConstraint(solver, order, 6, 5);
-       Boolean *o58 =  orderConstraint(solver, order, 5, 8);
-       Boolean *o81 =  orderConstraint(solver, order, 8, 1);
-       
-       addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o12, o13, o24, o34}, 4) );
-       Boolean *b1 = applyLogicalOperation(solver, L_XOR, (Boolean *[]) {o41, o57}, 2);
-       Boolean *o34n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o34}, 1);
-       Boolean *o24n = applyLogicalOperation(solver, L_NOT, (Boolean *[]) {o24}, 1);
-       Boolean *b2 = applyLogicalOperation(solver, L_OR, (Boolean *[]) {o34n, o24n}, 2);
-       addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b1, b2}, 2) );
-       addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o12, o13}, 2) );
-       addConstraint(solver, applyLogicalOperation(solver, L_OR,(Boolean *[]) {o76, o65}, 2) );
-       Boolean* b3= applyLogicalOperation(solver, L_AND,(Boolean *[]) {o76, o65}, 2) ;
-       Boolean* o57n= applyLogicalOperation(solver, L_NOT,(Boolean *[]) {o57}, 1);
-       addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) );
-       addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) );
-       
-       if (startEncoding(solver) == 1)
-               printf("SAT\n");
-       else
-               printf("UNSAT\n");
-       deleteSolver(solver);
-}
\ No newline at end of file
+       Set *s = solver->createSet(0, set1, 8);
+       Order *order = solver->createOrder(SATC_TOTAL, s);
+       BooleanEdge o12 =  solver->orderConstraint(order, 1, 2);
+       BooleanEdge o13 =  solver->orderConstraint(order, 1, 3);
+       BooleanEdge o24 =  solver->orderConstraint(order, 2, 4);
+       BooleanEdge o34 =  solver->orderConstraint(order, 3, 4);
+       BooleanEdge o41 =  solver->orderConstraint(order, 4, 1);
+       BooleanEdge o57 =  solver->orderConstraint(order, 5, 7);
+       BooleanEdge o76 =  solver->orderConstraint(order, 7, 6);
+       BooleanEdge o65 =  solver->orderConstraint(order, 6, 5);
+       BooleanEdge o58 =  solver->orderConstraint(order, 5, 8);
+       BooleanEdge o81 =  solver->orderConstraint(order, 8, 1);
+
+       BooleanEdge array1[] = {o12, o13, o24, o34};
+       solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) );
+       BooleanEdge array2[] = {o41, o57};
+
+       BooleanEdge b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
+       BooleanEdge array3[] = {o34};
+       BooleanEdge o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
+       BooleanEdge array4[] = {o24};
+       BooleanEdge o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
+       BooleanEdge array5[] = {o34n, o24n};
+       BooleanEdge b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
+       BooleanEdge array6[] = {b1, b2};
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );
+
+       BooleanEdge array7[] = {o12, o13};
+       solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
+
+       BooleanEdge array8[] = {o76, o65};
+       solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
+
+       BooleanEdge array9[] = {o76, o65};
+       BooleanEdge b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
+       BooleanEdge array10[] = {o57};
+       BooleanEdge o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
+       BooleanEdge array11[] = {b3, o57n};
+       solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));
+
+       BooleanEdge array12[] = {o58, o81};
+       solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
+       solver->serialize();
+       /*      if (solver->solve() == 1)
+          printf("SAT\n");
+          else
+          printf("UNSAT\n");*/
+
+       solver->autoTune(100);
+       delete solver;
+}