From 4bf1bdbb11d9b5db95673b599cf5c4c8b0615eeb Mon Sep 17 00:00:00 2001 From: Hamed Date: Sun, 27 Aug 2017 16:12:19 -0700 Subject: [PATCH] Fixing the ordergraphtest --- src/Test/ordergraphtest.cc | 46 +++++++++++++++++++++++--------------- 1 file changed, 28 insertions(+), 18 deletions(-) diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index 4562176..69d0d3d 100644 --- 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; } -- 2.34.1