Adding python api for serilizing + performance improvement + making logs more readable
authorHamed Gorjiara <hgorjiar@uci.edu>
Wed, 18 Apr 2018 19:20:14 +0000 (12:20 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Wed, 18 Apr 2018 19:20:14 +0000 (12:20 -0700)
src/Backend/constraint.cc
src/Backend/satfuncopencoder.cc
src/Collections/cppvector.h
src/Test/deserializersolvetest.cc
src/Tuner/autotuner.cc
src/ccsolver.cc
src/ccsolver.h
src/csolver.cc
src/pycsolver.py

index 0988c31..535d058 100644 (file)
@@ -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;
 }
 
index 6210b99..79b1303 100644 (file)
@@ -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;
index 2d4cc19..b8497d9 100644 (file)
@@ -63,7 +63,7 @@ public:
                array[index] = item;
        }
 
-       uint getSize() const {
+       inline uint getSize() const {
                return size;
        }
 
index 2a2910f..b003226 100644 (file)
@@ -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();
index 5247d86..bdfeb61 100644 (file)
@@ -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;
 }
index 3d09bea..823b2f2 100644 (file)
@@ -136,4 +136,6 @@ void printConstraints(void* solver){
 
 
 
-
+void serialize(void* solver){
+       CCSOLVER(solver)->serialize();
+}
index e585855..d47e5ae 100644 (file)
@@ -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
index 9007467..2a440ac 100644 (file)
@@ -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;
index 32a8415..d78836e 100644 (file)
@@ -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