From: bdemsky <bdemsky@uci.edu>
Date: Sun, 3 Sep 2017 03:57:42 +0000 (-0700)
Subject: Handle optimizations for mustbetrue/mustbefalse automatically
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=b7c60513c6e98582529ec3f3a175119781805a4a;p=satune.git

Handle optimizations for mustbetrue/mustbefalse automatically
---

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 218fc50..c943b0f 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -16,8 +16,8 @@ public:
 	Boolean(ASTNodeType _type);
 	virtual ~Boolean() {}
 	virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
-	virtual bool isTrue() {return false;}
-	virtual bool isFalse() {return false;}
+	virtual bool isTrue() {return boolVal == BV_MUSTBETRUE;}
+	virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
 	Polarity polarity;
 	BooleanValue boolVal;
 	Vector<Boolean *> parents;
diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 80e1f1a..cfa41d5 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -11,6 +11,10 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
 		constraints.remove(bexpr);
 	}
 
+	replaceBooleanWithTrueNoRemove(bexpr);
+}
+	
+void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 	uint size = bexpr->parents.getSize();
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = bexpr->parents.get(i);
diff --git a/src/csolver.cc b/src/csolver.cc
index ecc237e..956b6bf 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -348,6 +348,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 			updateMustValue(ptr, BV_MUSTBEFALSE);
 		else
 			updateMustValue(ptr, BV_MUSTBETRUE);
+		
+		if (ptr->boolVal == BV_UNSAT)
+			setUnSAT();
+		
+		replaceBooleanWithTrueNoRemove(constraint);
+		constraint->parents.clear();
 	}
 }
 
diff --git a/src/csolver.h b/src/csolver.h
index 2875a9c..3ff8509 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -134,6 +134,7 @@ public:
 	SATEncoder *getSATEncoder() {return satEncoder;}
 
 	void replaceBooleanWithTrue(BooleanEdge bexpr);
+	void replaceBooleanWithTrueNoRemove(BooleanEdge bexpr);
 	void replaceBooleanWithFalse(BooleanEdge bexpr);
 	void replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb);
 	CSolver *clone();