edits

diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc
index 7841a70eda242ce46789730372c420fc2e2c847d..7780f577e20a03bcaf2388035e157f708aae5146 100644 (file)
--- 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 d0b29760a423ee6edf46c4aa44de2a4f2c1fa927..df80fa73a50239a8a83d4fb56916917f68f5dbdd 100644 (file)
--- 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 4818f246e90cb1aff667d00a9d986993b909b182..c85782840dd0469dbe8807a63c6c087f34cdae02 100644 (file)
--- 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 f32d4479f2b546996fd42b079b9c3f57afb3f6fe..f9f9c07efcef407b2cbae639a47b29300aa3d8f6 100644 (file)
--- 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 98b4a27e6e158a5d57b05966aa6404a964836171..10e7f859555cc09a6a2b91338d38ea1a5312480a 100644 (file)
--- 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 4f19f6769dc7098bbf5eb912f92711b0440891b9..8a13e4e6e2737a0114b98af5b769f999bca36275 100644 (file)
--- 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;
 }