From a255c76241d54ef340c21c25a8c640e88988d204 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Wed, 30 Aug 2017 21:16:56 -0700 Subject: [PATCH] Rename startEncoding function --- src/Test/buildconstraintstest.cc | 2 +- src/Test/elemequalsattest.cc | 2 +- src/Test/elemequalunsattest.cc | 2 +- src/Test/funcencodingtest.cc | 2 +- src/Test/logicopstest.cc | 2 +- src/Test/ltelemconsttest.cc | 2 +- src/Test/ordergraphtest.cc | 2 +- src/Test/ordertest.cc | 2 +- src/Test/tablefuncencodetest.cc | 2 +- src/Test/tablepredicencodetest.cc | 2 +- src/Tuner/autotuner.cc | 2 +- src/csolver.cc | 2 +- src/csolver.h | 2 +- 13 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc index bbb2485..d3f4a24 100644 --- 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 53f8212..ff2f59b 100644 --- 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 5ec2bca..cd35ba7 100644 --- 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 d6a7962..87315f5 100644 --- 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 ece659e..a21e9c6 100644 --- 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 b110f29..b75bfb6 100644 --- 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 ccf1933..72ad021 100644 --- 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 893338d..1d90290 100644 --- 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 e998f3b..3252247 100644 --- 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 e0575e7..02195ea 100644 --- 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 e9bd773..3765759 100644 --- 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 0d6e352..29a9911 100644 --- 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 b937f71..bb9b1e1 100644 --- 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); -- 2.34.1