Rename startEncoding function

diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
index bbb2485bc3245fa82b55826a69e37de1736e5f35..d3f4a2407f51a72199ddceb5500adbce4be633fe 100644 (file)
--- a/src/Test/buildconstraintstest.cc
+++ b/src/Test/buildconstraintstest.cc
@@ -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");

diff --git a/src/Test/elemequalsattest.cc b/src/Test/elemequalsattest.cc
index 53f82127939f5316072b4c01916d501e3403a322..ff2f59bd2646efa6f64fbab2d11b14ef833c7218 100644 (file)
--- a/src/Test/elemequalsattest.cc
+++ b/src/Test/elemequalsattest.cc
@@ -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");

diff --git a/src/Test/elemequalunsattest.cc b/src/Test/elemequalunsattest.cc
index 5ec2bcafcd9002234d83fba9f867edcb90efa386..cd35ba7d42c1ca84011bb65bc8f86fc9cd521e83 100644 (file)
--- a/src/Test/elemequalunsattest.cc
+++ b/src/Test/elemequalunsattest.cc
@@ -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");

diff --git a/src/Test/funcencodingtest.cc b/src/Test/funcencodingtest.cc
index d6a796200d7dc30fee4e8eeafa4d231ac902a3a1..87315f509faa9f4d30e7ee61bea47bf1c9e43c45 100644 (file)
--- a/src/Test/funcencodingtest.cc
+++ b/src/Test/funcencodingtest.cc
@@ -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

diff --git a/src/Test/logicopstest.cc b/src/Test/logicopstest.cc
index ece659e4699aafa14fc8861ac2d31a871677d118..a21e9c6fbe1d27ff6aa5fa53ce6864784eb9d793 100644 (file)
--- a/src/Test/logicopstest.cc
+++ b/src/Test/logicopstest.cc
@@ -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));

diff --git a/src/Test/ltelemconsttest.cc b/src/Test/ltelemconsttest.cc
index b110f29b8698b06d0e6cd19de9abc863afc7d484..b75bfb64843d9933293b478b6592619e4e74d705 100644 (file)
--- a/src/Test/ltelemconsttest.cc
+++ b/src/Test/ltelemconsttest.cc
@@ -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");

diff --git a/src/Test/ordergraphtest.cc b/src/Test/ordergraphtest.cc
index ccf1933a5e9110dbc99bc81e97410ac602f6a57b..72ad021e7eac2e5d9711871e4f759338c0884f98 100644 (file)
--- a/src/Test/ordergraphtest.cc
+++ b/src/Test/ordergraphtest.cc
@@ -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");*/

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 893338dd5419da5e9e0617ec1e079019054f9792..1d9029098823bf6dcc4fae7ad9f7c923032e2ef4 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -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");

diff --git a/src/Test/tablefuncencodetest.cc b/src/Test/tablefuncencodetest.cc
index e998f3bb6dbf42588c1b1f61ed948e6351c967d2..32522476c9d2ddf462019a1378933b858a877dd6 100644 (file)
--- a/src/Test/tablefuncencodetest.cc
+++ b/src/Test/tablefuncencodetest.cc
@@ -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));

diff --git a/src/Test/tablepredicencodetest.cc b/src/Test/tablepredicencodetest.cc
index e0575e77450f42051020ed085142a05b9a7b406d..02195ea705e57f3513693ab7b40d3b9d5a2171f0 100644 (file)
--- a/src/Test/tablepredicencodetest.cc
+++ b/src/Test/tablepredicencodetest.cc
@@ -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));

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index e9bd7731e1b5030e97eb3c786c5312d322558bd8..37657590a9b0698fc3ea536d794baf9ae1745315 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -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();

diff --git a/src/csolver.cc b/src/csolver.cc
index 0d6e352b50bcad23f6b6210bb80d04eddb25bd28..29a99118eda43b1e26b6553afb11164d9ca2ea08 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -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();

diff --git a/src/csolver.h b/src/csolver.h
index b937f7136486fa72242ea53aaf9014058688d1c8..bb9b1e1f52267d02f36cccb3885d74a59f761a98 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -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);