Fix test cases

diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
old mode 100644 (file)
new mode 100755 (executable)
index d3f4a24..af17a4b
--- a/src/Test/buildconstraintstest.cc
+++ b/src/Test/buildconstraintstest.cc
@@ -25,7 +25,7 @@ int main(int numargs, char **argv) {
        Set *domain[] = {s, s};
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};
        Set *domain[] = {s, s};
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};

-       Boolean *b = solver->applyPredicate(equals, inputs, 2);
+       BooleanEdge b = solver->applyPredicate(equals, inputs, 2);

        solver->addConstraint(b);
 
        uint64_t set2[] = {2, 3};
        solver->addConstraint(b);
 
        uint64_t set2[] = {2, 3};


@@ -42,13 +42,13 @@ int main(int numargs, char **argv) {
        solver->addTableEntry(table, row3, 2, 2);
        solver->addTableEntry(table, row4, 2, 2);
        Function *f2 = solver->completeTable(table, SATC_IGNOREBEHAVIOR);       //its range would be as same as s
        solver->addTableEntry(table, row3, 2, 2);
        solver->addTableEntry(table, row4, 2, 2);
        Function *f2 = solver->completeTable(table, SATC_IGNOREBEHAVIOR);       //its range would be as same as s

-       Boolean *overflow = solver->getBooleanVar(2);
+       BooleanEdge overflow = solver->getBooleanVar(2);

        Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
        Element *e4 = solver->applyFunction(f2, inputs, 2, overflow);
        Set *domain2[] = {s,rangef1};
        Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
        Element *inputs2 [] = {e4, e3};
        Element *e3 = solver->applyFunction(f1, inputs, 2, overflow);
        Element *e4 = solver->applyFunction(f2, inputs, 2, overflow);
        Set *domain2[] = {s,rangef1};
        Predicate *equal2 = solver->createPredicateOperator(SATC_EQUALS, domain2, 2);
        Element *inputs2 [] = {e4, e3};

-       Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
+       BooleanEdge pred = solver->applyPredicate(equal2, inputs2, 2);

        solver->addConstraint(pred);
 
        if (solver->solve() == 1)
        solver->addConstraint(pred);
 
        if (solver->solve() == 1)

diff --git a/src/Test/cnftest.cc b/src/Test/cnftest.cc
old mode 100644 (file)
new mode 100755 (executable)

diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc
old mode 100644 (file)
new mode 100755 (executable)
index ff2f59b..aeab4a5
--- a/src/Test/elemequalsattest.cc
+++ b/src/Test/elemequalsattest.cc
@@ -22,7 +22,7 @@ int main(int numargs, char **argv) {
        Set *domain[] = {s1, s2};
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};
        Set *domain[] = {s1, s2};
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};

-       Boolean *b = solver->applyPredicate(equals, inputs, 2);
+       BooleanEdge b = solver->applyPredicate(equals, inputs, 2);

        solver->addConstraint(b);
 
        if (solver->solve() == 1)
        solver->addConstraint(b);
 
        if (solver->solve() == 1)

diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc
old mode 100644 (file)
new mode 100755 (executable)
index cd35ba7..6a7a067
--- a/src/Test/elemequalunsattest.cc
+++ b/src/Test/elemequalunsattest.cc
@@ -17,7 +17,7 @@ int main(int numargs, char **argv) {
        Set *domain[] = {s1, s2};
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};
        Set *domain[] = {s1, s2};
        Predicate *equals = solver->createPredicateOperator(SATC_EQUALS, domain, 2);
        Element *inputs[] = {e1, e2};

-       Boolean *b = solver->applyPredicate(equals, inputs, 2);
+       BooleanEdge b = solver->applyPredicate(equals, inputs, 2);

        solver->addConstraint(b);
 
        if (solver->solve() == 1)
        solver->addConstraint(b);
 
        if (solver->solve() == 1)

diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc
old mode 100644 (file)
new mode 100755 (executable)
index 87315f5..e3baeb9
--- a/src/Test/funcencodingtest.cc
+++ b/src/Test/funcencodingtest.cc
@@ -31,7 +31,7 @@ int main(int numargs, char **argv) {
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
        Element *e7 = solver->getElementVar(s5);
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
        Element *e7 = solver->getElementVar(s5);

-       Boolean *overflow = solver->getBooleanVar(2);
+       BooleanEdge overflow = solver->getBooleanVar(2);

        Set *d1[] = {s1, s2};
        //change the overflow flag
        Function *f1 = solver->createFunctionOperator(SATC_SUB, d1, 2, s2, SATC_IGNORE);
        Set *d1[] = {s1, s2};
        //change the overflow flag
        Function *f1 = solver->createFunctionOperator(SATC_SUB, d1, 2, s2, SATC_IGNORE);


@@ -70,7 +70,7 @@ int main(int numargs, char **argv) {
        Set *deq[] = {s5,s4};
        Predicate *gt = solver->createPredicateOperator(SATC_GT, deq, 2);
        Element *inputs2 [] = {e7, e6};
        Set *deq[] = {s5,s4};
        Predicate *gt = solver->createPredicateOperator(SATC_GT, deq, 2);
        Element *inputs2 [] = {e7, e6};

-       Boolean *pred = solver->applyPredicate(gt, inputs2, 2);
+       BooleanEdge pred = solver->applyPredicate(gt, inputs2, 2);

        solver->addConstraint(pred);
 
        if (solver->solve() == 1)
        solver->addConstraint(pred);
 
        if (solver->solve() == 1)

diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc
old mode 100644 (file)
new mode 100755 (executable)
index a21e9c6..9b20015
--- a/src/Test/logicopstest.cc
+++ b/src/Test/logicopstest.cc
@@ -8,21 +8,21 @@
  */
 int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();
  */
 int main(int numargs, char **argv) {
        CSolver *solver = new CSolver();

-       Boolean *b1 = solver->getBooleanVar(0);
-       Boolean *b2 = solver->getBooleanVar(0);
-       Boolean *b3 = solver->getBooleanVar(0);
-       Boolean *b4 = solver->getBooleanVar(0);
+       BooleanEdge b1 = solver->getBooleanVar(0);
+       BooleanEdge b2 = solver->getBooleanVar(0);
+       BooleanEdge b3 = solver->getBooleanVar(0);
+       BooleanEdge b4 = solver->getBooleanVar(0);

        //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES
        //SATC_AND, SATC_OR, SATC_NOT, SATC_XOR, SATC_IMPLIES

-       Boolean *barray1[] = {b1,b2};
-       Boolean *andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);
-       Boolean *barray2[] = {andb1b2, b3};
-       Boolean *imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2);
+       BooleanEdge barray1[] = {b1,b2};
+       BooleanEdge andb1b2 = solver->applyLogicalOperation(SATC_AND, barray1, 2);
+       BooleanEdge barray2[] = {andb1b2, b3};
+       BooleanEdge imply = solver->applyLogicalOperation(SATC_IMPLIES, barray2, 2);

        solver->addConstraint(imply);
        solver->addConstraint(imply);

-       Boolean *barray3[] = {b3};
-       Boolean *notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
-       Boolean *barray4[] = {notb3, b4};
+       BooleanEdge barray3[] = {b3};
+       BooleanEdge notb3 = solver->applyLogicalOperation(SATC_NOT, barray3, 1);
+       BooleanEdge barray4[] = {notb3, b4};

        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));

-       Boolean *barray5[] = {b1, b4};
+       BooleanEdge barray5[] = {b1, b4};

        solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
        if (solver->solve() == 1)
                printf("b1=%d b2=%d b3=%d b4=%d\n",
        solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
        if (solver->solve() == 1)
                printf("b1=%d b2=%d b3=%d b4=%d\n",

diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc
old mode 100644 (file)
new mode 100755 (executable)
index b75bfb6..d666833
--- a/src/Test/ltelemconsttest.cc
+++ b/src/Test/ltelemconsttest.cc
@@ -16,7 +16,7 @@ int main(int numargs, char **argv) {
        Set *domain2[] = {s1, s3};
        Predicate *lt = solver->createPredicateOperator(SATC_LT, domain2, 2);
        Element *inputs2[] = {e1, e2};
        Set *domain2[] = {s1, s3};
        Predicate *lt = solver->createPredicateOperator(SATC_LT, domain2, 2);
        Element *inputs2[] = {e1, e2};

-       Boolean *b = solver->applyPredicate(lt, inputs2, 2);
+       BooleanEdge b = solver->applyPredicate(lt, inputs2, 2);

        solver->addConstraint(b);
        if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        solver->addConstraint(b);
        if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));

diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc
old mode 100644 (file)
new mode 100755 (executable)
index 092e0ed..80a57ff
--- a/src/Test/ordergraphtest.cc
+++ b/src/Test/ordergraphtest.cc
@@ -5,45 +5,45 @@ int main(int numargs, char **argv) {
        uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
        Set *s = solver->createSet(0, set1, 8);
        Order *order = solver->createOrder(SATC_TOTAL, s);
        uint64_t set1[] = {1, 2, 3, 4, 5, 6, 7, 8};
        Set *s = solver->createSet(0, set1, 8);
        Order *order = solver->createOrder(SATC_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);
-
-       Boolean *array1[] = {o12, o13, o24, o34};
+       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) );
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array1, 4) );

-       Boolean *array2[] = {o41, o57};
-
-       Boolean *b1 = solver->applyLogicalOperation(SATC_XOR, array2, 2);
-       Boolean *array3[] = {o34};
-       Boolean *o34n = solver->applyLogicalOperation(SATC_NOT, array3, 1);
-       Boolean *array4[] = {o24};
-       Boolean *o24n = solver->applyLogicalOperation(SATC_NOT, array4, 1);
-       Boolean *array5[] = {o34n, o24n};
-       Boolean *b2 = solver->applyLogicalOperation(SATC_OR, array5, 2);
-       Boolean *array6[] = {b1, b2};
+       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) );
 
        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array6, 2) );
 

-       Boolean *array7[] = {o12, o13};
+       BooleanEdge array7[] = {o12, o13};

        solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
 
        solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array7, 2) );
 

-       Boolean *array8[] = {o76, o65};
+       BooleanEdge array8[] = {o76, o65};

        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
 
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, array8, 2) );
 

-       Boolean *array9[] = {o76, o65};
-       Boolean *b3 = solver->applyLogicalOperation(SATC_AND, array9, 2) ;
-       Boolean *array10[] = {o57};
-       Boolean *o57n = solver->applyLogicalOperation(SATC_NOT, array10, 1);
-       Boolean *array11[] = {b3, o57n};
+       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));
 
        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, array11, 2));
 

-       Boolean *array12[] = {o58, o81};
+       BooleanEdge array12[] = {o58, o81};

        solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
 
        /*      if (solver->solve() == 1)
        solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
 
        /*      if (solver->solve() == 1)

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
old mode 100644 (file)
new mode 100755 (executable)
index 1d90290..8633415
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -11,8 +11,8 @@ int main(int numargs, char **argv) {
        uint64_t set1[] = {5, 1, 4};
        Set *s = solver->createSet(0, set1, 3);
        Order *order = solver->createOrder(SATC_TOTAL, s);
        uint64_t set1[] = {5, 1, 4};
        Set *s = solver->createSet(0, set1, 3);
        Order *order = solver->createOrder(SATC_TOTAL, s);

-       Boolean *b1 =  solver->orderConstraint(order, 5, 1);
-       Boolean *b2 =  solver->orderConstraint(order, 1, 4);
+       BooleanEdge b1 =  solver->orderConstraint(order, 5, 1);
+       BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);

        solver->addConstraint(b1);
        solver->addConstraint(b2);
        if (solver->solve() == 1)
        solver->addConstraint(b1);
        solver->addConstraint(b2);
        if (solver->solve() == 1)

diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc
old mode 100644 (file)
new mode 100755 (executable)
index 3252247..11017c6
--- a/src/Test/tablefuncencodetest.cc
+++ b/src/Test/tablefuncencodetest.cc
@@ -24,7 +24,7 @@ int main(int numargs, char **argv) {
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
        Element *e4 = solver->getElementVar(s3);
        Element *e1 = solver->getElementVar(s1);
        Element *e2 = solver->getElementVar(s2);
        Element *e4 = solver->getElementVar(s3);

-       Boolean *overflow = solver->getBooleanVar(2);
+       BooleanEdge overflow = solver->getBooleanVar(2);

        Set *d1[] = {s1, s2};
        //change the overflow flag
        Table *t1 = solver->createTable(d1, 2, s2);
        Set *d1[] = {s1, s2};
        //change the overflow flag
        Table *t1 = solver->createTable(d1, 2, s2);


@@ -47,7 +47,7 @@ int main(int numargs, char **argv) {
        Set *deq[] = {s3,s2};
        Predicate *lte = solver->createPredicateOperator(SATC_LTE, deq, 2);
        Element *inputs2 [] = {e4, e3};
        Set *deq[] = {s3,s2};
        Predicate *lte = solver->createPredicateOperator(SATC_LTE, deq, 2);
        Element *inputs2 [] = {e4, e3};

-       Boolean *pred = solver->applyPredicate(lte, inputs2, 2);
+       BooleanEdge pred = solver->applyPredicate(lte, inputs2, 2);

        solver->addConstraint(pred);
 
        if (solver->solve() == 1)
        solver->addConstraint(pred);
 
        if (solver->solve() == 1)

diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc
old mode 100644 (file)
new mode 100755 (executable)
index 02195ea..47113fd
--- a/src/Test/tablepredicencodetest.cc
+++ b/src/Test/tablepredicencodetest.cc
@@ -41,21 +41,21 @@ int main(int numargs, char **argv) {
        solver->addTableEntry(t1, row5, 3, false);
        solver->addTableEntry(t1, row6, 3, true);
        Predicate *p1 = solver->createPredicateTable(t1, SATC_FLAGIFFUNDEFINED);
        solver->addTableEntry(t1, row5, 3, false);
        solver->addTableEntry(t1, row6, 3, true);
        Predicate *p1 = solver->createPredicateTable(t1, SATC_FLAGIFFUNDEFINED);

-       Boolean *undef = solver->getBooleanVar(2);
+       BooleanEdge undef = solver->getBooleanVar(2);

        Element *tmparray[] = {e1, e2, e3};
        Element *tmparray[] = {e1, e2, e3};

-       Boolean *b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);
+       BooleanEdge b1 = solver->applyPredicateTable(p1, tmparray, 3, undef);

        solver->addConstraint(b1);
 
        Set *deq[] = {s3,s2};
        Predicate *gte = solver->createPredicateOperator(SATC_GTE, deq, 2);
        Element *inputs2 [] = {e3, e2};
        solver->addConstraint(b1);
 
        Set *deq[] = {s3,s2};
        Predicate *gte = solver->createPredicateOperator(SATC_GTE, deq, 2);
        Element *inputs2 [] = {e3, e2};

-       Boolean *pred = solver->applyPredicate(gte, inputs2, 2);
+       BooleanEdge pred = solver->applyPredicate(gte, inputs2, 2);

        solver->addConstraint(pred);
 
        Set *d1[] = {s1, s2};
        Predicate *eq = solver->createPredicateOperator(SATC_EQUALS, d1, 2);
        Element *tmparray2[] = {e1, e2};
        solver->addConstraint(pred);
 
        Set *d1[] = {s1, s2};
        Predicate *eq = solver->createPredicateOperator(SATC_EQUALS, d1, 2);
        Element *tmparray2[] = {e1, e2};

-       Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
+       BooleanEdge pred2 = solver->applyPredicate(eq, tmparray2, 2);

        solver->addConstraint(pred2);
 
        if (solver->solve() == 1)
        solver->addConstraint(pred2);
 
        if (solver->solve() == 1)