Adding python api for serilizing + performance improvement + making logs more readable

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 0988c314448ae43d280aac6200a7b5597d2973f5..535d058c39882ef2b53f0519746fe9596e48a01a 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -686,7 +686,7 @@ int solveCNF(CNF *cnf) {
        cnf->encodeTime = startSolve - startTime;
        model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
        cnf->solveTime = finishTime - startSolve;
-       model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
+       model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
        return result;
 }
 

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 6210b99940d4254905152458cb6c8b5fe4eb11b1..79b13033ebdc40f4ffd82963ac83885d936f3cdc 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -48,9 +48,8 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
        }
 
        bool notfinished = true;
+        Edge carray[numDomains];
        while (notfinished) {
-               Edge carray[numDomains];
-
                if (predicate->evalPredicateOperator(vals) != generateNegation) {
                        //Include this in the set of terms
                        for (uint i = 0; i < numDomains; i++) {
@@ -111,9 +110,8 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
        }
 
        bool notfinished = true;
+        Edge carray[numDomains + 1];
        while (notfinished) {
-               Edge carray[numDomains + 1];
-
                uint64_t result = function->applyFunctionOperator(numDomains, vals);
                bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
                bool needClause = isInRange;

diff --git a/src/Collections/cppvector.h b/src/Collections/cppvector.h
index 2d4cc1956df10579e362966c84371f4f34d5c63f..b8497d90857af941c12b24a74126a80714c99998 100644 (file)
--- a/src/Collections/cppvector.h
+++ b/src/Collections/cppvector.h
@@ -63,7 +63,7 @@ public:
                array[index] = item;
        }
 
-       uint getSize() const {
+       inline uint getSize() const {
                return size;
        }
 

diff --git a/src/Test/deserializersolvetest.cc b/src/Test/deserializersolvetest.cc
index 2a2910fa7de1b74f06bc4b3de85b52ec7c9f3e05..b003226f67b0ecba33619581519db70e32098aaa 100644 (file)
--- a/src/Test/deserializersolvetest.cc
+++ b/src/Test/deserializersolvetest.cc
@@ -1,12 +1,13 @@
 #include "csolver.h"
-//#include <unistd.h>
-//#include <sys/types.h>
+#include <unistd.h>
+#include <sys/types.h>
 
 int main(int argc, char **argv) {
        if (argc < 2) {
                printf("You should specify file names ...");
                exit(-1);
        }
+        usleep(20000000);
        for (int i = 1; i < argc; i++) {
                CSolver *solver = CSolver::deserialize(argv[i]);
                int value = solver->solve();

diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 5247d86b0fa1d9d576cb6887ead59f73a7b4745a..bdfeb614b0386fff6bef467d857f19670004b41b 100644 (file)
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -16,15 +16,16 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
        CSolver *copy = problem->clone();
        copy->setTuner(tuner);
+        model_print("**********************\n");
        int result = copy->solve();
-       model_print("SAT %d\n", result);
+       //model_print("SAT %d\n", result);
        long long elapsedTime = copy->getElapsedTime();
-       long long encodeTime = copy->getEncodeTime();
-       long long solveTime = copy->getSolveTime();
+//     long long encodeTime = copy->getEncodeTime();
+//     long long solveTime = copy->getSolveTime();
        long long metric = elapsedTime;
-       model_print("Elapsed Time: %llu\n", elapsedTime);
-       model_print("Encode Time: %llu\n", encodeTime);
-       model_print("Solve Time: %llu\n", solveTime);
+//     model_print("Elapsed Time: %llu\n", elapsedTime);
+//     model_print("Encode Time: %llu\n", encodeTime);
+//     model_print("Solve Time: %llu\n", solveTime);
        delete copy;
        return metric;
 }

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index 3d09bea1ab009c2d1904b624e648d566d3161ef2..823b2f20ac33cb0ed23cd667c2169c627776c847 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -136,4 +136,6 @@ void printConstraints(void* solver){
 
 
 
-
+void serialize(void* solver){
+       CCSOLVER(solver)->serialize();
+}

diff --git a/src/ccsolver.h b/src/ccsolver.h
index e5858554b6139ab10817cd622c2986ac6ba42557..d47e5ae29710223ef9063b58c818c10557424c9f 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -39,6 +39,7 @@ long getElementValue(void* solver,void *element);
 int getBooleanValue(void* solver,void* boolean);
 int getOrderConstraintValue(void* solver,void *order, long first, long second);
 void printConstraints(void* solver);
+void serialize(void* solver);
 #ifdef __cplusplus
 }
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index 900746773e9e3217f967d345a09929be64acd2b6..2a440ac3c4689b547662bb839ceebf2a02b133ce 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -616,7 +616,7 @@ int CSolver::solve() {
 
        model_print("Is problem UNSAT after encoding: %d\n", unsat);
        int result = unsat ? IS_UNSAT : satEncoder->solve();
-       model_print("Result Computed in CSolver: %d\n", result);
+       model_print("Result Computed in SAT solver: %d\n", result);
 
        if (deleteTuner) {
                delete tuner;

diff --git a/src/pycsolver.py b/src/pycsolver.py
index 32a8415b9da431b24a941c4c48b0154d6a527d4e..d78836e023e1e6188880d6187ee198d0ec978d09 100644 (file)
--- a/src/pycsolver.py
+++ b/src/pycsolver.py
@@ -94,5 +94,7 @@ def loadCSolver():
        csolverlb.getOrderConstraintValue.restype = c_int
        csolverlb.printConstraints.argtypes = [c_void_p]
        csolverlb.printConstraints.restype = None
+       csolverlb.serialize.argtypes = [c_void_p]
+       csolverlb.serialize.restype = None
        return csolverlb