From 1bbedcc6a785d0cef637350b1f2f624b290f149f Mon Sep 17 00:00:00 2001 From: bdemsky Date: Fri, 25 Aug 2017 15:59:28 -0700 Subject: [PATCH] edits --- src/Test/elemequalsattest.cc | 22 ++++++------ src/Test/logicopstest.cc | 30 ++++++++--------- src/Test/ltelemconsttest.cc | 24 ++++++------- src/Test/ordergraphtest.cc | 37 ++++++++++---------- src/Test/tablefuncencodetest.cc | 48 +++++++++++++------------- src/Test/tablepredicencodetest.cc | 56 +++++++++++++++---------------- 6 files changed, 109 insertions(+), 108 deletions(-) diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc index 7841a70..7780f57 100644 --- a/src/Test/elemequalsattest.cc +++ b/src/Test/elemequalsattest.cc @@ -12,22 +12,22 @@ * e1=2 e2=7 */ int main(int numargs, char **argv) { - CSolver *solver = allocCSolver(); + CSolver *solver = new CSolver(); uint64_t set1[] = {0, 1, 2}; uint64_t set2[] = {3, 1, 7}; - Set *s1 = createSet(solver, 0, set1, 3); - Set *s2 = createSet(solver, 0, set2, 3); - Element *e1 = getElementVar(solver, s1); - Element *e2 = getElementVar(solver, s2); + Set *s1 = solver->createSet(0, set1, 3); + Set *s2 = solver->createSet(0, set2, 3); + Element *e1 = solver->getElementVar(s1); + Element *e2 = solver->getElementVar(s2); Set *domain[] = {s1, s2}; - Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2); + Predicate *equals = solver->createPredicateOperator(EQUALS, domain, 2); Element *inputs[] = {e1, e2}; - Boolean *b = applyPredicate(solver, equals, inputs, 2); - addConstraint(solver, b); + Boolean *b = solver->applyPredicate(equals, inputs, 2); + solver->addConstraint(b); - if (startEncoding(solver) == 1) - printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2)); + if (solver->startEncoding() == 1) + printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2)); else printf("UNSAT\n"); - deleteSolver(solver); + delete solver; } diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc index d0b2976..df80fa7 100644 --- a/src/Test/logicopstest.cc +++ b/src/Test/logicopstest.cc @@ -7,28 +7,28 @@ * Result: b1=1 b2=0 b3=0 b4=0 */ int main(int numargs, char **argv) { - CSolver *solver = allocCSolver(); - Boolean *b1 = getBooleanVar(solver, 0); - Boolean *b2 = getBooleanVar(solver, 0); - Boolean *b3 = getBooleanVar(solver, 0); - Boolean *b4 = getBooleanVar(solver, 0); + CSolver *solver = new CSolver(); + Boolean *b1 = solver->getBooleanVar(0); + Boolean *b2 = solver->getBooleanVar(0); + Boolean *b3 = solver->getBooleanVar(0); + Boolean *b4 = solver->getBooleanVar(0); //L_AND, L_OR, L_NOT, L_XOR, L_IMPLIES Boolean * barray1[]={b1,b2}; - Boolean *andb1b2 = applyLogicalOperation(solver, L_AND, barray1, 2); + Boolean *andb1b2 = solver->applyLogicalOperation(L_AND, barray1, 2); Boolean * barray2[]={andb1b2, b3}; - Boolean *imply = applyLogicalOperation(solver, L_IMPLIES, barray2, 2); - addConstraint(solver, imply); + Boolean *imply = solver->applyLogicalOperation(L_IMPLIES, barray2, 2); + solver->addConstraint(imply); Boolean * barray3[] ={b3}; - Boolean *notb3 = applyLogicalOperation(solver, L_NOT, barray3, 1); + Boolean *notb3 = solver->applyLogicalOperation(L_NOT, barray3, 1); Boolean * barray4[] ={notb3, b4}; - addConstraint(solver, applyLogicalOperation(solver, L_OR, barray4, 2)); + solver->addConstraint(solver->applyLogicalOperation(L_OR, barray4, 2)); Boolean * barray5[] ={b1, b4}; - addConstraint(solver, applyLogicalOperation(solver, L_XOR, barray5, 2)); - if (startEncoding(solver) == 1) + solver->addConstraint(solver->applyLogicalOperation(L_XOR, barray5, 2)); + if (solver->startEncoding() == 1) printf("b1=%d b2=%d b3=%d b4=%d\n", - getBooleanValue(solver,b1), getBooleanValue(solver, b2), - getBooleanValue(solver, b3), getBooleanValue(solver, b4)); + solver->getBooleanValue(b1), solver->getBooleanValue(b2), + solver->getBooleanValue(b3), solver->getBooleanValue(b4)); else printf("UNSAT\n"); - deleteSolver(solver); + delete solver; } diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc index 4818f24..c857828 100644 --- a/src/Test/ltelemconsttest.cc +++ b/src/Test/ltelemconsttest.cc @@ -6,21 +6,21 @@ * Result: e1=5 e2=6 */ int main(int numargs, char **argv) { - CSolver *solver = allocCSolver(); + CSolver *solver = new CSolver(); uint64_t set1[] = {5}; uint64_t set3[] = {1, 3, 4, 6}; - Set *s1 = createSet(solver, 0, set1, 3); - Set *s3 = createSet(solver, 0, set3, 4); - Element *e1 = getElementConst(solver, 4, 5); - Element *e2 = getElementVar(solver, s3); + Set *s1 = solver->createSet(0, set1, 3); + Set *s3 = solver->createSet(0, set3, 4); + Element *e1 = solver->getElementConst(4, 5); + Element *e2 = solver->getElementVar(s3); Set *domain2[] = {s1, s3}; - Predicate *lt = createPredicateOperator(solver, LT, domain2, 2); + Predicate *lt = solver->createPredicateOperator(LT, domain2, 2); Element *inputs2[] = {e1, e2}; - Boolean *b = applyPredicate(solver, lt, inputs2, 2); - addConstraint(solver, b); - if (startEncoding(solver) == 1) - printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2)); + Boolean *b = solver->applyPredicate(lt, inputs2, 2); + solver->addConstraint(b); + if (solver->startEncoding() == 1) + printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2)); else printf("UNSAT\n"); - deleteSolver(solver); -} \ No newline at end of file + delete solver; +} diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc index f32d447..f9f9c07 100644 --- a/src/Test/ordergraphtest.cc +++ b/src/Test/ordergraphtest.cc @@ -1,22 +1,22 @@ #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); - - /* + Set *s = solver->createSet(0, set1, 8); + Order *order = solver->createOrder(TOTAL, s); + Boolean *o12 = solver->orderConstraint(order, 1, 2); + Boolean *o13 = solver->orderConstraint(order, 1, 3); + Boolean *o24 = solver->orderConstraint(order, 2, 4); + Boolean *o34 = solver->orderConstraint(order, 3, 4); + Boolean *o41 = solver->orderConstraint(order, 4, 1); + Boolean *o57 = solver->orderConstraint(order, 5, 7); + Boolean *o76 = solver->orderConstraint(order, 7, 6); + Boolean *o65 = solver->orderConstraint(order, 6, 5); + Boolean *o58 = solver->orderConstraint(order, 5, 8); + Boolean *o81 = solver->orderConstraint(order, 8, 1); + + /* 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); @@ -30,9 +30,10 @@ int main(int numargs, char **argv) { addConstraint(solver, applyLogicalOperation(solver, L_IMPLIES,(Boolean *[]) {b3, o57n}, 2) ); addConstraint(solver, applyLogicalOperation(solver, L_AND,(Boolean *[]) {o58, o81}, 2) ); - if (startEncoding(solver) == 1) + if (solver->startEncoding() == 1) printf("SAT\n"); else - printf("UNSAT\n");*/ - deleteSolver(solver); + printf("UNSAT\n"); + */ + delete solver; } diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc index 98b4a27..10e7f85 100644 --- a/src/Test/tablefuncencodetest.cc +++ b/src/Test/tablefuncencodetest.cc @@ -14,47 +14,47 @@ * Result: e1=1, e2=5, e3=7, e4=6, overflow=0 */ int main(int numargs, char **argv) { - CSolver *solver = allocCSolver(); + CSolver *solver = new CSolver(); uint64_t set1[] = {1, 2}; uint64_t set2[] = {3, 5, 7}; uint64_t set3[] = {6, 10, 19}; - Set *s1 = createSet(solver, 0, set1, 2); - Set *s2 = createSet(solver, 0, set2, 3); - Set *s3 = createSet(solver, 0, set3, 3); - Element *e1 = getElementVar(solver, s1); - Element *e2 = getElementVar(solver, s2); - Element *e4 = getElementVar(solver, s3); - Boolean *overflow = getBooleanVar(solver, 2); + Set *s1 = solver->createSet(0, set1, 2); + Set *s2 = solver->createSet(0, set2, 3); + Set *s3 = solver->createSet(0, set3, 3); + Element *e1 = solver->getElementVar(s1); + Element *e2 = solver->getElementVar(s2); + Element *e4 = solver->getElementVar(s3); + Boolean *overflow = solver->getBooleanVar(2); Set *d1[] = {s1, s2}; //change the overflow flag - Table *t1 = createTable(solver, d1, 2, s2); + Table *t1 = solver->createTable(d1, 2, s2); uint64_t row1[] = {1, 5}; uint64_t row2[] = {2, 3}; uint64_t row3[] = {1, 7}; uint64_t row4[] = {2, 7}; uint64_t row5[] = {2, 5}; uint64_t row6[] = {1, 3}; - addTableEntry(solver, t1, row1, 2, 7); - addTableEntry(solver, t1, row2, 2, 5); - addTableEntry(solver, t1, row3, 2, 3); - addTableEntry(solver, t1, row4, 2, 5); - addTableEntry(solver, t1, row5, 2, 3); - addTableEntry(solver, t1, row6, 2, 5); - Function *f1 = completeTable(solver, t1, FLAGIFFUNDEFINED); + solver->addTableEntry(t1, row1, 2, 7); + solver->addTableEntry(t1, row2, 2, 5); + solver->addTableEntry(t1, row3, 2, 3); + solver->addTableEntry(t1, row4, 2, 5); + solver->addTableEntry(t1, row5, 2, 3); + solver->addTableEntry(t1, row6, 2, 5); + Function *f1 = solver->completeTable(t1, FLAGIFFUNDEFINED); Element * tmparray[]={e1, e2}; - Element *e3 = applyFunction(solver, f1, tmparray, 2, overflow); + Element *e3 = solver->applyFunction(f1, tmparray, 2, overflow); Set *deq[] = {s3,s2}; - Predicate *lte = createPredicateOperator(solver, LTE, deq, 2); + Predicate *lte = solver->createPredicateOperator(LTE, deq, 2); Element *inputs2 [] = {e4, e3}; - Boolean *pred = applyPredicate(solver, lte, inputs2, 2); - addConstraint(solver, pred); + Boolean *pred = solver->applyPredicate(lte, inputs2, 2); + solver->addConstraint(pred); - if (startEncoding(solver) == 1) + if (solver->startEncoding() == 1) printf("e1=%llu e2=%llu e3=%llu e4=%llu overFlow:%d\n", - getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e3), - getElementValue(solver, e4), getBooleanValue(solver, overflow)); + solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e3), + solver->getElementValue(e4), solver->getBooleanValue(overflow)); else printf("UNSAT\n"); - deleteSolver(solver); + delete solver; } diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc index 4f19f67..8a13e4e 100644 --- a/src/Test/tablepredicencodetest.cc +++ b/src/Test/tablepredicencodetest.cc @@ -15,54 +15,54 @@ * Result: e1=1, e2=1, e3=6 OR 10 OR 19, overflow=1 */ int main(int numargs, char **argv) { - CSolver *solver = allocCSolver(); + CSolver *solver = new CSolver(); uint64_t set1[] = {1, 2}; uint64_t set2[] = {1, 3, 5, 7}; uint64_t set3[] = {6, 10, 19}; - Set *s1 = createSet(solver, 0, set1, 2); - Set *s2 = createSet(solver, 0, set2, 4); - Set *s3 = createSet(solver, 0, set3, 3); - Element *e1 = getElementVar(solver, s1); - Element *e2 = getElementVar(solver, s2); - Element *e3 = getElementVar(solver, s3); + Set *s1 = solver->createSet(0, set1, 2); + Set *s2 = solver->createSet(0, set2, 4); + Set *s3 = solver->createSet(0, set3, 3); + Element *e1 = solver->getElementVar(s1); + Element *e2 = solver->getElementVar(s2); + Element *e3 = solver->getElementVar(s3); Set *d2[] = {s1, s2, s3}; //change the overflow flag - Table *t1 = createTableForPredicate(solver, d2, 3); + Table *t1 = solver->createTableForPredicate(d2, 3); uint64_t row1[] = {1, 5, 6}; uint64_t row2[] = {2, 3, 19}; uint64_t row3[] = {1, 3, 19}; uint64_t row4[] = {2, 7, 10}; uint64_t row5[] = {1, 7, 6}; uint64_t row6[] = {2, 5, 6}; - addTableEntry(solver, t1, row1, 3, true); - addTableEntry(solver, t1, row2, 3, true); - addTableEntry(solver, t1, row3, 3, false); - addTableEntry(solver, t1, row4, 3, false); - addTableEntry(solver, t1, row5, 3, false); - addTableEntry(solver, t1, row6, 3, true); - Predicate *p1 = createPredicateTable(solver, t1, FLAGIFFUNDEFINED); - Boolean *undef = getBooleanVar(solver, 2); + solver->addTableEntry(t1, row1, 3, true); + solver->addTableEntry(t1, row2, 3, true); + solver->addTableEntry(t1, row3, 3, false); + solver->addTableEntry(t1, row4, 3, false); + solver->addTableEntry(t1, row5, 3, false); + solver->addTableEntry(t1, row6, 3, true); + Predicate *p1 = solver->createPredicateTable(t1, FLAGIFFUNDEFINED); + Boolean *undef = solver->getBooleanVar(2); Element * tmparray[] = {e1, e2, e3}; - Boolean *b1 = applyPredicateTable(solver, p1, tmparray, 3, undef); - addConstraint(solver, b1); + Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef); + solver->addConstraint(b1); Set *deq[] = {s3,s2}; - Predicate *gte = createPredicateOperator(solver, GTE, deq, 2); + Predicate *gte = solver->createPredicateOperator(GTE, deq, 2); Element *inputs2 [] = {e3, e2}; - Boolean *pred = applyPredicate(solver, gte, inputs2, 2); - addConstraint(solver, pred); + Boolean *pred = solver->applyPredicate(gte, inputs2, 2); + solver->addConstraint(pred); Set *d1[] = {s1, s2}; - Predicate *eq = createPredicateOperator(solver, EQUALS, d1, 2); + Predicate *eq = solver->createPredicateOperator(EQUALS, d1, 2); Element * tmparray2[] = {e1, e2}; - Boolean *pred2 = applyPredicate(solver, eq, tmparray2, 2); - addConstraint(solver, pred2); + Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2); + solver->addConstraint(pred2); - if (startEncoding(solver) == 1) + if (solver->startEncoding() == 1) printf("e1=%llu e2=%llu e3=%llu undefFlag:%d\n", - getElementValue(solver,e1), getElementValue(solver, e2), - getElementValue(solver, e3), getBooleanValue(solver, undef)); + solver->getElementValue(e1), solver->getElementValue(e2), + solver->getElementValue(e3), solver->getBooleanValue(undef)); else printf("UNSAT\n"); - deleteSolver(solver); + delete solver; } -- 2.34.1