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

diff --git a/src/csolver.cc b/src/csolver.cc
index 81aeb8e..17e2378 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -39,6 +39,8 @@ CSolver::CSolver() :
 	boolFalse(boolTrue.negate()),
 	unsat(false),
 	booleanVarUsed(false),
+	incrementalMode(false),
+	optimizationsOff(false),
 	tuner(NULL),
 	elapsedTime(0),
 	satsolverTimeout(NOTIMEOUT),
@@ -139,6 +141,7 @@ void CSolver::resetSolver() {
 	allOrders.clear();
 	allFunctions.clear();
 	constraints.reset();
+	encodedConstraints.reset();
 	activeOrders.reset();
 	boolMap.reset();
 	elemMap.reset();
@@ -240,6 +243,17 @@ void CSolver::mustHaveValue(Element *element) {
 	element->anyValue = true;
 }
 
+void CSolver::freezeElementsVariables() {
+
+	for (uint i = 0; i < allElements.getSize(); i++) {
+		Element *e = allElements.get(i);
+		if (e->frozen) {
+			satEncoder->freezeElementVariables(&e->encoding);
+		}
+	}
+}
+
+
 Set *CSolver::getElementRange (Element *element) {
 	return element->getRange();
 }
@@ -395,6 +409,26 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 	return applyLogicalOperation(op, newarray, asize);
 }
 
+BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
+	BooleanEdge newarray[asize + 1];
+
+	newarray[asize] = applyLogicalOperation(SATC_OR, array, asize);
+	for (uint i = 0; i < asize; i++) {
+		BooleanEdge oprand1 = array[i];
+		BooleanEdge carray [asize - 1];
+		uint index = 0;
+		for ( uint j = 0; j < asize; j++) {
+			if (i != j) {
+				BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
+				carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
+			}
+		}
+		ASSERT(index == asize - 1);
+		newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
+	}
+	return applyLogicalOperation(SATC_AND, newarray, asize + 1);
+}
+
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 	if (!useInterpreter()) {
 		BooleanEdge newarray[asize];
@@ -533,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)) {
@@ -603,6 +637,75 @@ void CSolver::inferFixedOrders() {
 	}
 }
 
+int CSolver::solveIncremental() {
+	if (isUnSAT()) {
+		return IS_UNSAT;
+	}
+
+
+	long long startTime = getTimeNano();
+	bool deleteTuner = false;
+	if (tuner == NULL) {
+		tuner = new DefaultTuner();
+		deleteTuner = true;
+	}
+	int result = IS_INDETER;
+	ASSERT (!useInterpreter());
+	if(!optimizationsOff){
+		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);
+
+//	IntegerEncodingTransform iet(this);
+//	iet.doTransform();
+
+	//Doing element optimization on new constraints
+//	ElementOpt eop(this);
+//	eop.doTransform();
+
+	//Since no new element is added, we assuming adding new constraint
+	//has no impact on previous encoding decisions
+//	EncodingGraph eg(this);
+//	eg.encode();
+
+	naiveEncodingDecision(this);
+	//	eg.validate();
+	//Order of sat solver variables don't change!
+//	VarOrderingOpt bor(this, satEncoder);
+//	bor.doTransform();
+
+	long long time2 = getTimeNano();
+	//Encoding newly added constraints
+	satEncoder->encodeAllSATEncoder(this);
+	long long time1 = getTimeNano();
+
+	model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
+
+	model_print("Is problem UNSAT after encoding: %d\n", unsat);
+
+	result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
+	model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
+	time2 = getTimeNano();
+	elapsedTime = time2 - startTime;
+	model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+
+	if (deleteTuner) {
+		delete tuner;
+		tuner = NULL;
+	}
+	return result;
+}
+
 int CSolver::solve() {
 	if (isUnSAT()) {
 		return IS_UNSAT;
@@ -632,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();
@@ -736,6 +842,13 @@ uint64_t CSolver::getElementValue(Element *element) {
 	exit(-1);
 }
 
+void CSolver::freezeElement(Element *e) {
+	e->freezeElement();
+	if (!incrementalMode) {
+		incrementalMode = true;
+	}
+}
+
 bool CSolver::getBooleanValue(BooleanEdge bedge) {
 	Boolean *boolean = bedge.getBoolean();
 	switch (boolean->type) {