From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Wed, 18 Apr 2018 19:20:14 +0000 (-0700)
Subject: Adding python api for serilizing + performance improvement + making logs more readable
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=c8fa49521562e3053876a003ebf3780f260d3dbf

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

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 0988c31..535d058 100644
--- 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 6210b99..79b1303 100644
--- 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 2d4cc19..b8497d9 100644
--- 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 2a2910f..b003226 100644
--- 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 5247d86..bdfeb61 100644
--- 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 3d09bea..823b2f2 100644
--- 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 e585855..d47e5ae 100644
--- 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 9007467..2a440ac 100644
--- 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 32a8415..d78836e 100644
--- 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