X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FAST%2Frewriter.cc;h=fef4dcbb17aaf40626791272a67db9d68cf0de11;hp=937a8b74cb442f2f6a0738fa039da845a0558eb8;hb=f2bb71e84525d9ebc1841d5c2867d8b48c070cd5;hpb=2ad5d121f791b7e2a8b904ba75f270e6372f1730

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 937a8b7..fef4dcb 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -2,77 +2,124 @@
 #include "boolean.h"
 #include "csolver.h"
 #include "polarityassignment.h"
+#include "element.h"
 
 void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
 	if (constraints.contains(bexpr.negate())) {
 		constraints.remove(bexpr.negate());
 		setUnSAT();
-	}	
+	}
 	if (constraints.contains(bexpr)) {
 		constraints.remove(bexpr);
 	}
 
 	replaceBooleanWithTrueNoRemove(bexpr);
 }
-	
+
+void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
+	replaceBooleanWithTrueNoRemove(bexpr.negate());
+}
+
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 	updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
-	
+
+	ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
+
 	uint size = bexpr->parents.getSize();
 	for (uint i = 0; i < size; i++) {
-		Boolean *parent = bexpr->parents.get(i);
-		ASSERT(parent->type == LOGICOP);
-		BooleanLogic *logicop = (BooleanLogic *) parent;
-		switch (logicop->op) {
-		case SATC_AND:
-			handleANDTrue(logicop, bexpr);
-			break;
-		case SATC_IFF:
-			handleIFFTrue(logicop, bexpr);
-			break;
-		case SATC_NOT:
-		case SATC_OR:
-		case SATC_XOR:
-		case SATC_IMPLIES:
-			ASSERT(0);
+		ASTNode *parent = bexpr->parents.get(i);
+		if (parent->type == ELEMFUNCRETURN) {
+			ElementFunction *ef = (ElementFunction *) parent;
+			handleFunction(ef, bexpr);
+		} else {
+			ASSERT(parent->type == LOGICOP);
+			BooleanLogic *logicop = (BooleanLogic *) parent;
+			switch (logicop->op) {
+			case SATC_AND:
+				handleANDTrue(logicop, bexpr);
+				break;
+			case SATC_IFF:
+				handleIFFTrue(logicop, bexpr);
+				break;
+			case SATC_NOT:
+			case SATC_OR:
+			case SATC_XOR:
+			case SATC_IMPLIES:
+				ASSERT(0);
+			}
 		}
 	}
 }
 
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
+	BooleanEdge childNegate = child.negate();
+	elemMap.remove(ef);
+	if (ef->overflowstatus == child) {
+		ef->overflowstatus = boolTrue;
+	} else if (ef->overflowstatus == childNegate) {
+		ef->overflowstatus = boolFalse;
+	}
+	elemMap.put(ef, ef);
+}
+
 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
 	//Canonicalize
 	if (oldb.isNegated()) {
-		oldb=oldb.negate();
-		newb=newb.negate();
+		oldb = oldb.negate();
+		newb = newb.negate();
+
 	}
 	if (constraints.contains(oldb)) {
 		constraints.remove(oldb);
 		constraints.add(newb);
+		if (newb->type == BOOLEANVAR)
+			replaceBooleanWithTrue(newb);
+		else
+			replaceBooleanWithTrueNoRemove(newb);
+		return;
 	}
 	if (constraints.contains(oldb.negate())) {
 		constraints.remove(oldb.negate());
 		constraints.add(newb.negate());
+		if (newb->type == BOOLEANVAR)
+			replaceBooleanWithTrue(newb.negate());
+		else
+			replaceBooleanWithTrueNoRemove(newb.negate());
+		return;
 	}
 
 	BooleanEdge oldbnegated = oldb.negate();
 	uint size = oldb->parents.getSize();
 	for (uint i = 0; i < size; i++) {
-		Boolean *parent = oldb->parents.get(i);
-		BooleanLogic *logicop = (BooleanLogic *) parent;
-		boolMap.remove(parent); //could change parent's hash
-		
-		uint parentsize = logicop->inputs.getSize();
-		for (uint j = 0; j < parentsize; j++) {
-			BooleanEdge b = logicop->inputs.get(j);
-			if (b == oldb) {
-				logicop->inputs.set(j, newb);
-				newb->parents.push(parent);
-			} else if (b == oldbnegated) {
-				logicop->inputs.set(j, newb.negate());
-				newb->parents.push(parent);
+		ASTNode *parent = oldb->parents.get(i);
+		if (parent->type == ELEMFUNCRETURN) {
+			ElementFunction *ef = (ElementFunction *) parent;
+			elemMap.remove(ef);
+			if (ef->overflowstatus == oldb) {
+				ef->overflowstatus = newb;
+				newb->parents.push(ef);
+			} else if (ef->overflowstatus == oldbnegated) {
+				ef->overflowstatus = newb.negate();
+				newb->parents.push(ef);
+			}
+			elemMap.put(ef, ef);
+		} else {
+			BooleanLogic *logicop = (BooleanLogic *) parent;
+			boolMap.remove(logicop);	//could change parent's hash
+
+			uint parentsize = logicop->inputs.getSize();
+			for (uint j = 0; j < parentsize; j++) {
+				BooleanEdge b = logicop->inputs.get(j);
+				if (b == oldb) {
+					logicop->inputs.set(j, newb);
+					newb->parents.push(logicop);
+				} else if (b == oldbnegated) {
+					logicop->inputs.set(j, newb.negate());
+					newb->parents.push(logicop);
+				}
 			}
+			boolMap.put(logicop, logicop);
 		}
-		boolMap.put(parent, parent);
 	}
 }
 
@@ -95,13 +142,13 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 }
 
 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
-	BooleanEdge childNegate=child.negate();
-	
+	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--;
@@ -111,7 +158,7 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
 		}
 	}
 
-	uint size=bexpr->inputs.getSize();
+	uint size = bexpr->inputs.getSize();
 	if (size == 0) {
 		bexpr->replaced = true;
 		replaceBooleanWithTrue(bexpr);
@@ -129,8 +176,8 @@ void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 }
 
 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
-	bool isNegated=bexpr.isNegated();
-	BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+	bool isNegated = bexpr.isNegated();
+	BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
 	BooleanEdge result;
 	if (b->op == SATC_IFF) {
 		if (isTrue(b->inputs.get(0))) {
@@ -142,7 +189,7 @@ BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
 		} else if (isFalse(b->inputs.get(1))) {
 			result = b->inputs.get(0).negate();
 		} else ASSERT(0);
-	} else if (b->op==SATC_AND) {
+	} else if (b->op == SATC_AND) {
 		uint size = b->inputs.getSize();
 		if (size == 0)
 			result = boolTrue;