X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FAST%2Frewriter.cc;h=a53180e1ef972b87964c00dd04ed91ae2e107b77;hb=3c33c8ed7c4600da543b2a82bcffd5aca86f0eb9;hp=f32fc91b0e945d74ea94f4e8df5e250ce94e17fe;hpb=9b6f097f739d112bf3363f107064752cb8318c0b;p=satune.git

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index f32fc91..a53180e 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -1,164 +1,201 @@
 #include "rewriter.h"
 #include "boolean.h"
 #include "csolver.h"
+#include "polarityassignment.h"
+#include "element.h"
 
-void CSolver::replaceBooleanWithTrue(Boolean *bexpr) {
+void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
+	if (constraints.contains(bexpr.negate())) {
+		constraints.remove(bexpr.negate());
+		setUnSAT();
+	}
 	if (constraints.contains(bexpr)) {
 		constraints.remove(bexpr);
 	}
 
-	uint size = bexpr->parents.getSize();
-	for (uint i = 0; i < size; i++) {
-		Boolean *parent = bexpr->parents.get(i);
-		BooleanLogic *logicop = (BooleanLogic *) parent;
-		switch (logicop->op) {
-		case L_AND:
-			handleANDTrue(logicop, bexpr);
-			break;
-		case L_OR:
-			replaceBooleanWithTrue(parent);
-			break;
-		case L_NOT:
-			replaceBooleanWithFalse(parent);
-			break;
-		case L_XOR:
-			handleXORTrue(logicop, bexpr);
-			break;
-		case L_IMPLIES:
-			handleIMPLIESTrue(logicop, bexpr);
-			break;
-		}
-	}
+	replaceBooleanWithTrueNoRemove(bexpr);
 }
 
-void CSolver::replaceBooleanWithBoolean(Boolean *oldb, Boolean *newb) {
-	if (constraints.contains(oldb)) {
-		constraints.remove(oldb);
-		constraints.add(newb);
-	}
+void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
+	replaceBooleanWithTrueNoRemove(bexpr.negate());
+}
 
-	uint size = oldb->parents.getSize();
-	for (uint i = 0; i < size; i++) {
-		Boolean *parent = oldb->parents.get(i);
-		BooleanLogic *logicop = (BooleanLogic *) parent;
+void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
+	updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
-		uint parentsize = logicop->inputs.getSize();
+	ASSERT((bexpr->boolVal != BV_UNSAT) || unsat);
 
-		for (uint j = 0; j < parentsize; j++) {
-			Boolean *b = logicop->inputs.get(i);
-			if (b == oldb) {
-				logicop->inputs.set(i, newb);
-				newb->parents.push(parent);
+	uint size = bexpr->parents.getSize();
+	for (uint i = 0; i < size; i++) {
+		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 handleXORTrue(BooleanLogic *bexpr, Boolean *child) {
-	uint size = bexpr->inputs.getSize();
-	Boolean *b = bexpr->inputs.get(0);
-	uint childindex = (b == child) ? 0 : 1;
-	bexpr->inputs.remove(childindex);
-	bexpr->op = L_NOT;
+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::handleXORFalse(BooleanLogic *bexpr, Boolean *child) {
-	uint size = bexpr->inputs.getSize();
-	Boolean *b = bexpr->inputs.get(0);
-	uint otherindex = (b == child) ? 1 : 0;
-	replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(otherindex));
-}
+void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
+	//Canonicalize
+	if (oldb.isNegated()) {
+		oldb = oldb.negate();
+		newb = newb.negate();
 
-void CSolver::handleIMPLIESTrue(BooleanLogic *bexpr, Boolean *child) {
-	uint size = bexpr->inputs.getSize();
-	Boolean *b = bexpr->inputs.get(0);
-	if (b == child) {
-		//Replace with other term
-		replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(1));
-	} else {
-		//Statement is true...
-		replaceBooleanWithTrue(bexpr);
 	}
-}
-
-void CSolver::handleIMPLIESFalse(BooleanLogic *bexpr, Boolean *child) {
-	uint size = bexpr->inputs.getSize();
-	Boolean *b = bexpr->inputs.get(0);
-	if (b == child) {
-		//Statement is true...
-		replaceBooleanWithTrue(bexpr);
-	} else {
-		//Make into negation of first term
-		bexpr->inputs.get(1);
-		bexpr->op = L_NOT;
+	if (constraints.contains(oldb)) {
+		constraints.remove(oldb);
+		constraints.add(newb);
+		if (newb->type == BOOLEANVAR)
+			replaceBooleanWithTrue(newb);
+		else
+			replaceBooleanWithTrueNoRemove(newb);
+		return;
 	}
-}
-
-void CSolver::handleANDTrue(BooleanLogic *bexpr, Boolean *child) {
-	uint size = bexpr->inputs.getSize();
-
-	if (size == 1) {
-		replaceBooleanWithTrue(bexpr);
+	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 *b = bexpr->inputs.get(i);
-		if (b == child) {
-			bexpr->inputs.remove(i);
+		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);
 		}
 	}
-
-	if (size == 2) {
-		replaceBooleanWithBoolean(bexpr, bexpr->inputs.get(0));
-	}
 }
 
-void CSolver::handleORFalse(BooleanLogic *bexpr, Boolean *child) {
+void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 	uint size = bexpr->inputs.getSize();
+	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) {
+		replaceBooleanWithBoolean(BooleanEdge(bexpr), b1.negate());
+	} else if (b1 == child) {
+		replaceBooleanWithBoolean(BooleanEdge(bexpr), b0);
+	} else if (b1 == childnegate) {
+		replaceBooleanWithBoolean(BooleanEdge(bexpr), b0.negate());
+	} else
+		ASSERT(0);
+}
 
-	if (size == 1) {
-		replaceBooleanWithFalse(bexpr);
-	}
+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);
 
-	for (uint i = 0; i < size; i++) {
-		Boolean *b = bexpr->inputs.get(i);
 		if (b == child) {
 			bexpr->inputs.remove(i);
+			i--;
+		} else if (b == childNegate) {
+			replaceBooleanWithFalse(bexpr);
+			return;
 		}
 	}
 
-	if (size == 2) {
+	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(Boolean *bexpr) {
-	if (constraints.contains(bexpr)) {
-		setUnSAT();
-		constraints.remove(bexpr);
-	}
+void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
+	replaceBooleanWithTrue(bexpr.negate());
+}
 
-	uint size = bexpr->parents.getSize();
-	for (uint i = 0; i < size; i++) {
-		Boolean *parent = bexpr->parents.get(i);
-		BooleanLogic *logicop = (BooleanLogic *) parent;
-		switch (logicop->op) {
-		case L_AND:
-			replaceBooleanWithFalse(parent);
-			break;
-		case L_OR:
-			handleORFalse(logicop, bexpr);
-			break;
-		case L_NOT:
-			replaceBooleanWithTrue(parent);
-			break;
-		case L_XOR:
-			handleXORFalse(logicop, bexpr);
-			break;
-		case L_IMPLIES:
-			handleIMPLIESFalse(logicop, bexpr);
-			break;
-		}
+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;
 }