Rename startEncoding function
authorbdemsky <bdemsky@uci.edu>
Thu, 31 Aug 2017 04:16:56 +0000 (21:16 -0700)
committerbdemsky <bdemsky@uci.edu>
Thu, 31 Aug 2017 04:17:19 +0000 (21:17 -0700)
13 files changed:
src/Test/buildconstraintstest.cc
src/Test/elemequalsattest.cc
src/Test/elemequalunsattest.cc
src/Test/funcencodingtest.cc
src/Test/logicopstest.cc
src/Test/ltelemconsttest.cc
src/Test/ordergraphtest.cc
src/Test/ordertest.cc
src/Test/tablefuncencodetest.cc
src/Test/tablepredicencodetest.cc
src/Tuner/autotuner.cc
src/csolver.cc
src/csolver.h

index bbb2485..d3f4a24 100644 (file)
@@ -51,7 +51,7 @@ int main(int numargs, char **argv) {
        Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
        solver->addConstraint(pred);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " \n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
index 53f8212..ff2f59b 100644 (file)
@@ -25,7 +25,7 @@ int main(int numargs, char **argv) {
        Boolean *b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
index 5ec2bca..cd35ba7 100644 (file)
@@ -20,7 +20,7 @@ int main(int numargs, char **argv) {
        Boolean *b = solver->applyPredicate(equals, inputs, 2);
        solver->addConstraint(b);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
index d6a7962..87315f5 100644 (file)
@@ -73,7 +73,7 @@ int main(int numargs, char **argv) {
        Boolean *pred = solver->applyPredicate(gt, inputs2, 2);
        solver->addConstraint(pred);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e7=%" PRIu64 "\n",
                                         solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e7));
        else
index ece659e..a21e9c6 100644 (file)
@@ -24,7 +24,7 @@ int main(int numargs, char **argv) {
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, barray4, 2));
        Boolean *barray5[] = {b1, b4};
        solver->addConstraint(solver->applyLogicalOperation(SATC_XOR, barray5, 2));
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("b1=%d b2=%d b3=%d b4=%d\n",
                                         solver->getBooleanValue(b1), solver->getBooleanValue(b2),
                                         solver->getBooleanValue(b3), solver->getBooleanValue(b4));
index b110f29..b75bfb6 100644 (file)
@@ -18,7 +18,7 @@ int main(int numargs, char **argv) {
        Element *inputs2[] = {e1, e2};
        Boolean *b = solver->applyPredicate(lt, inputs2, 2);
        solver->addConstraint(b);
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
        else
                printf("UNSAT\n");
index ccf1933..72ad021 100644 (file)
@@ -46,7 +46,7 @@ int main(int numargs, char **argv) {
        Boolean * array12[] = {o58, o81};
        solver->addConstraint(solver->applyLogicalOperation(SATC_AND, array12, 2) );
        
-       /*      if (solver->startEncoding() == 1)
+       /*      if (solver->solve() == 1)
                printf("SAT\n");
        else
        printf("UNSAT\n");*/
index 893338d..1d90290 100644 (file)
@@ -15,7 +15,7 @@ int main(int numargs, char **argv) {
        Boolean *b2 =  solver->orderConstraint(order, 1, 4);
        solver->addConstraint(b1);
        solver->addConstraint(b2);
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("SAT\n");
        else
                printf("UNSAT\n");
index e998f3b..3252247 100644 (file)
@@ -50,7 +50,7 @@ int main(int numargs, char **argv) {
        Boolean *pred = solver->applyPredicate(lte, inputs2, 2);
        solver->addConstraint(pred);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " e4=%" PRIu64 " overFlow:%d\n",
                                         solver->getElementValue(e1), solver->getElementValue(e2), solver->getElementValue(e3),
                                         solver->getElementValue(e4), solver->getBooleanValue(overflow));
index e0575e7..02195ea 100644 (file)
@@ -58,7 +58,7 @@ int main(int numargs, char **argv) {
        Boolean *pred2 = solver->applyPredicate(eq, tmparray2, 2);
        solver->addConstraint(pred2);
 
-       if (solver->startEncoding() == 1)
+       if (solver->solve() == 1)
                printf("e1=%" PRIu64 " e2=%" PRIu64 " e3=%" PRIu64 " undefFlag:%d\n",
                                         solver->getElementValue(e1), solver->getElementValue(e2),
                                         solver->getElementValue(e3), solver->getBooleanValue(undef));
index e9bd773..3765759 100644 (file)
@@ -16,7 +16,7 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver * problem, SearchTuner *tuner) {
        CSolver * copy=problem->clone();
        copy->setTuner(tuner);
-       int result = copy->startEncoding();
+       int result = copy->solve();
        long long elapsedTime=copy->getElapsedTime();
        long long encodeTime=copy->getEncodeTime();
        long long solveTime=copy->getSolveTime();
index 0d6e352..29a9911 100644 (file)
@@ -366,7 +366,7 @@ Order *CSolver::createOrder(OrderType type, Set *set) {
        return order;
 }
 
-int CSolver::startEncoding() {
+int CSolver::solve() {
        bool deleteTuner = false;
        if (tuner == NULL) {
                tuner = new DefaultTuner();
index b937f71..bb9b1e1 100644 (file)
@@ -106,7 +106,7 @@ public:
        Boolean *orderConstraint(Order *order, uint64_t first, uint64_t second);
 
        /** When everything is done, the client calls this function and then csolver starts to encode*/
-       int startEncoding();
+       int solve();
 
        /** After getting the solution from the SAT solver, client can get the value of an element via this function*/
        uint64_t getElementValue(Element *element);