X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FAST%2Frewriter.cc;h=c49fcf5d2d5d0c2fcbe0acf1846737527330e07a;hb=da9bf180de81b31c95fb4987b84412e11ce3f6eb;hp=80e1f1a90d4b34085527de89e2fdd678949ac2fc;hpb=6b81425e00f5a8e1e563ff268cca3c9bce355bcb;p=satune.git

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 80e1f1a..c49fcf5 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -1,6 +1,7 @@
 #include "rewriter.h"
 #include "boolean.h"
 #include "csolver.h"
+#include "polarityassignment.h"
 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
 	if (constraints.contains(bexpr.negate())) {
@@ -11,6 +12,12 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
 		constraints.remove(bexpr);
 	}
 
+	replaceBooleanWithTrueNoRemove(bexpr);
+}
+	
+void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
+	updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
+	
 	uint size = bexpr->parents.getSize();
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = bexpr->parents.get(i);
@@ -72,6 +79,7 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 	BooleanEdge b0 = bexpr->inputs.get(0);
 	BooleanEdge b1 = bexpr->inputs.get(1);
 	BooleanEdge childnegate = child.negate();
+	bexpr->replaced = true;
 	if (b0 == child) {
 		replaceBooleanWithBoolean(BooleanEdge(bexpr), b1);
 	} else if (b0 == childnegate) {
@@ -87,15 +95,15 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
 	BooleanEdge childNegate=child.negate();
 	
+	boolMap.remove(bexpr);
+	
 	for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
 		BooleanEdge b = bexpr->inputs.get(i);
 		
 		if (b == child) {
 			bexpr->inputs.remove(i);
 			i--;
-		}
-		
-		if (b == childNegate) {
+		} else if (b == childNegate) {
 			replaceBooleanWithFalse(bexpr);
 			return;
 		}
@@ -103,12 +111,42 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
 
 	uint size=bexpr->inputs.getSize();
 	if (size == 0) {
+		bexpr->replaced = true;
 		replaceBooleanWithTrue(bexpr);
 	} else if (size == 1) {
+		bexpr->replaced = true;
 		replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
+	} else {
+		//Won't build any of these in future cases...
+		boolMap.put(bexpr, bexpr);
 	}
 }
 
 void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 	replaceBooleanWithTrue(bexpr.negate());
 }
+
+BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
+	bool isNegated=bexpr.isNegated();
+	BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+	BooleanEdge result;
+	if (b->op == SATC_IFF) {
+		if (isTrue(b->inputs.get(0))) {
+			result = b->inputs.get(1);
+		} else if (isFalse(b->inputs.get(0))) {
+			result = b->inputs.get(1).negate();
+		} else if (isTrue(b->inputs.get(1))) {
+			result = b->inputs.get(0);
+		} else if (isFalse(b->inputs.get(1))) {
+			result = b->inputs.get(0).negate();
+		} else ASSERT(0);
+	} else if (b->op==SATC_AND) {
+		uint size = b->inputs.getSize();
+		if (size == 0)
+			result = boolTrue;
+		else if (size == 1)
+			result = b->inputs.get(0);
+		else ASSERT(0);
+	}
+	return isNegated ? result.negate() : result;
+}