From: bdemsky <bdemsky@uci.edu>
Date: Tue, 24 Oct 2017 22:07:19 +0000 (-0700)
Subject: Add timing statements
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=57efcd4a2e42b97ab5f564b7b1229612d2c0a793

Add timing statements
---

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index b7cb320..0fe3d45 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -352,6 +352,7 @@ int solveCNF(CNF *cnf) {
 	long long finishTime = getTimeNano();
 	cnf->encodeTime = startSolve - startTime;
 	cnf->solveTime = finishTime - startSolve;
+	model_print("CNF Encode time: %f\n Solve time: %f\n", cnf->encodeTime/1000000000.0, cnf->solveTime/ 1000000000.0);
 	return result;
 }
 
diff --git a/src/config.h b/src/config.h
index 2e48668..e34b828 100644
--- a/src/config.h
+++ b/src/config.h
@@ -19,7 +19,7 @@
 //#define CONFIG_DEBUG
 #endif
 
-//#define SATCHECK_CONFIG
+#define SATCHECK_CONFIG
 
 #ifndef CONFIG_ASSERT
 #define CONFIG_ASSERT
diff --git a/src/csolver.cc b/src/csolver.cc
index fb29cff..160e686 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -100,10 +100,7 @@ CSolver* CSolver::deserialize(const char * file){
 void CSolver::serialize() {
 	model_print("serializing ...\n");
 	char buffer[255];
-	struct timespec t;
-	clock_gettime(CLOCK_REALTIME, &t);
-
-	unsigned long long nanotime=t.tv_sec*1000000000+t.tv_nsec;
+	long long nanotime=getTimeNano();
 	int numchars=sprintf(buffer, "DUMP%llu", nanotime);
 	Serializer serializer(buffer);
 	SetIteratorBooleanEdge *it = getConstraints();
@@ -501,7 +498,9 @@ void CSolver::inferFixedOrders() {
 	}
 }
 
+#define NANOSEC 1000000000.0
 int CSolver::solve() {
+	long long starttime = getTimeNano();	
 	bool deleteTuner = false;
 	if (tuner == NULL) {
 		tuner = new DefaultTuner();
@@ -520,14 +519,19 @@ int CSolver::solve() {
 		}
 		delete orderit;
 	}
-	
-	computePolarities(this);
 
+	computePolarities(this);
+	long long time2 = getTimeNano();
+	model_print("Polarity time: %f\n", (time2-starttime)/NANOSEC);
 	Preprocess pp(this);
 	pp.doTransform();
-
+	long long time3 = getTimeNano();
+	model_print("Preprocess time: %f\n", (time3-time2)/NANOSEC);
+	
 	DecomposeOrderTransform dot(this);
 	dot.doTransform();
+	long long time4 = getTimeNano();
+	model_print("Decompose Order: %f\n", (time4-time3)/NANOSEC);
 
 	IntegerEncodingTransform iet(this);
 	iet.doTransform();
@@ -537,14 +541,20 @@ int CSolver::solve() {
 	eg.encode();
 
 	naiveEncodingDecision(this);
-
+	long long time5 = getTimeNano();
+	model_print("Encoding Graph Time: %f\n", (time5-time4)/NANOSEC);
+	
 	long long startTime = getTimeNano();
 	satEncoder->encodeAllSATEncoder(this);
+	long long endTime = getTimeNano();
+
+	elapsedTime = endTime - startTime;
+	model_print("Elapse Encode time: %f\n", elapsedTime/NANOSEC);
+	
 	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);
-	long long finishTime = getTimeNano();
-	elapsedTime = finishTime - startTime;
+	
 	if (deleteTuner) {
 		delete tuner;
 		tuner = NULL;
diff --git a/src/mymemory.h b/src/mymemory.h
index 0798860..766e6f6 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -19,7 +19,7 @@
 
 #include "config.h"
 
-//#define SATCHECK_CONFIG
+#define SATCHECK_CONFIG
 
 /*
    void * ourmalloc(size_t size);