Fixing the ordergraphtest

diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc
index 4562176d0bc937a9ac79669f98a16dc0dce5b090..69d0d3d3da9167e8c133ebd8a83ef1410d5015cc 100644 (file)
--- a/src/Test/ordergraphtest.cc
+++ b/src/Test/ordergraphtest.cc
@@ -15,25 +15,35 @@ int main(int numargs, char **argv) {
        Boolean *o65 =  solver->orderConstraint(order, 6, 5);
        Boolean *o58 =  solver->orderConstraint(order, 5, 8);
        Boolean *o81 =  solver->orderConstraint(order, 8, 1);
+       Boolean *in1 [] = {o12, o13, o24, o34};
+       solver->addConstraint(solver->applyLogicalOperation( L_OR, in1, 4) );
+       Boolean *in2[] = {o41, o57};
+       Boolean *b1 = solver->applyLogicalOperation(L_XOR, in2, 2);
+       Boolean *in3[]= {o34};
+       Boolean *o34n = solver->applyLogicalOperation(L_NOT,in3 , 1);
+       Boolean *in4[] = {o24};
+       Boolean *o24n = solver->applyLogicalOperation(L_NOT, in4, 1);
+       Boolean *in5[] ={o34n, o24n};
+       Boolean *b2 = solver->applyLogicalOperation(L_OR, in5, 2);
+       Boolean *in6[] = {b1, b2};
+       solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, in6, 2) );
+       Boolean *in7[] = {o12, o13};
+       solver->addConstraint(solver->applyLogicalOperation(L_AND, in7, 2) );
+       Boolean *in8[] = {o76, o65};
+       solver->addConstraint(solver->applyLogicalOperation(L_OR, in8, 2) );
+       Boolean *in9[] = {o76, o65};
+       Boolean* b3= solver->applyLogicalOperation(L_AND, in9, 2) ;
+       Boolean *in10[] = {o57};
+       Boolean* o57n= solver->applyLogicalOperation(L_NOT, in10, 1);
+       Boolean *in11[] = {b3, o57n};
+       solver->addConstraint(solver->applyLogicalOperation(L_IMPLIES, in11, 2) );
+       Boolean *in12[] = {o58, o81};
+       solver->addConstraint(solver->applyLogicalOperation(L_AND, in12, 2) );
 
-       /* Not Valid c++...Let Hamed fix...
-          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 (solver->startEncoding() == 1)
+       printf("SAT\n");
+       else
+       printf("UNSAT\n");
 
-          if (solver->startEncoding() == 1)
-          printf("SAT\n");
-          else
-          printf("UNSAT\n");
-        */
        delete solver;
 }