X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=17e237888caa78445af6b5cb91b1b9c4ebcfcd39;hp=17b3dc31b565db26711b89aebba6f4b31aa420c0;hb=85d422935f1a6ebdb689f4108185521b022a51d9;hpb=50d8f27a7eb47d7398e14252895a656dbeed5c6a

diff --git a/src/csolver.cc b/src/csolver.cc
index 17b3dc3..17e2378 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -40,6 +40,7 @@ CSolver::CSolver() :
 	unsat(false),
 	booleanVarUsed(false),
 	incrementalMode(false),
+	optimizationsOff(false),
 	tuner(NULL),
 	elapsedTime(0),
 	satsolverTimeout(NOTIMEOUT),
@@ -566,7 +567,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-	if (!useInterpreter()) {
+	if (!useInterpreter() && !optimizationsOff) {
 		if (isTrue(constraint))
 			return;
 		else if (isFalse(constraint)) {
@@ -650,8 +651,9 @@ int CSolver::solveIncremental() {
 	}
 	int result = IS_INDETER;
 	ASSERT (!useInterpreter());
-
-	computePolarities(this);
+	if(!optimizationsOff){
+		computePolarities(this);
+	}
 //	long long time1 = getTimeNano();
 //	model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 //	Preprocess pp(this);
@@ -733,36 +735,39 @@ int CSolver::solve() {
 			}
 			delete orderit;
 		}
+		long long time1, time2;
+		
 		computePolarities(this);
-		long long time1 = getTimeNano();
-		model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
-		Preprocess pp(this);
-		pp.doTransform();
-		long long time2 = getTimeNano();
-		model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
-
-		DecomposeOrderTransform dot(this);
-		dot.doTransform();
 		time1 = getTimeNano();
-		model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+		model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+		if(!optimizationsOff){
+			Preprocess pp(this);
+			pp.doTransform();
+			time2 = getTimeNano();
+			model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 
-		IntegerEncodingTransform iet(this);
-		iet.doTransform();
+			DecomposeOrderTransform dot(this);
+			dot.doTransform();
+			time1 = getTimeNano();
+			model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 
-		ElementOpt eop(this);
-		eop.doTransform();
+			IntegerEncodingTransform iet(this);
+			iet.doTransform();
 
-		EncodingGraph eg(this);
-		eg.encode();
+			ElementOpt eop(this);
+			eop.doTransform();
 
+			EncodingGraph eg(this);
+			eg.encode();
+		}
 		naiveEncodingDecision(this);
 		//	eg.validate();
-
-		VarOrderingOpt bor(this, satEncoder);
-		bor.doTransform();
-
-		time2 = getTimeNano();
-		model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+		if(!optimizationsOff){
+			VarOrderingOpt bor(this, satEncoder);
+			bor.doTransform();
+			time2 = getTimeNano();
+			model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+		}
 
 		satEncoder->encodeAllSATEncoder(this);
 		time1 = getTimeNano();