X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FASTAnalyses%2Fpolarityassignment.cc;h=2aa9e5d8e491ac24cf03690243cbb0147339e633;hp=14789304b49a797d74a14e4da5af02b6008dcd76;hb=f9546315ab6ece42f48fa8b2e2e53abcd1f00b74;hpb=13a2b4ac7c072f1896f23b30d23233eb67c05061

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 1478930..2aa9e5d 100644
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -81,8 +81,7 @@ BooleanValue negateBooleanValue(BooleanValue This) {
 void computeLogicOpPolarity(BooleanLogic *This) {
 	Polarity parentpolarity = This->polarity;
 	switch (This->op) {
-	case SATC_AND:
-	case SATC_OR: {
+	case SATC_AND: {
 		uint size = This->inputs.getSize();
 		for (uint i = 0; i < size; i++) {
 			Boolean *tmp = This->inputs.get(i);
@@ -95,19 +94,11 @@ void computeLogicOpPolarity(BooleanLogic *This) {
 		updatePolarity(tmp, negatePolarity(parentpolarity));
 		break;
 	}
-	case SATC_IFF:
-	case SATC_XOR: {
+	case SATC_IFF: {
 		updatePolarity(This->inputs.get(0), P_BOTHTRUEFALSE);
 		updatePolarity(This->inputs.get(1), P_BOTHTRUEFALSE);
 		break;
 	}
-	case SATC_IMPLIES: {
-		Boolean *left = This->inputs.get(0);
-		updatePolarity(left, negatePolarity( parentpolarity));
-		Boolean *right = This->inputs.get(1);
-		updatePolarity(right, parentpolarity);
-		break;
-	}
 	default:
 		ASSERT(0);
 	}
@@ -125,28 +116,10 @@ void computeLogicOpBooleanValue(BooleanLogic *This) {
 		}
 		return;
 	}
-	case SATC_OR: {
-		if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-			uint size = This->inputs.getSize();
-			for (uint i = 0; i < size; i++) {
-				updateMustValue(This->inputs.get(i), parentbv);
-			}
-		}
-		return;
-	}
 	case SATC_NOT:
 		updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
 		return;
-	case SATC_IMPLIES:
-		//implies is really an or with the first term negated
-		if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-			uint size = This->inputs.getSize();
-			updateMustValue(This->inputs.get(0), negateBooleanValue(parentbv));
-			updateMustValue(This->inputs.get(1), parentbv);
-		}
-		return;
 	case SATC_IFF:
-	case SATC_XOR:
 		return;
 	default:
 		ASSERT(0);