From a66aabb1f6034db3920885d3a1a7519a9cbbd637 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Sat, 2 Sep 2017 20:46:12 -0700
Subject: [PATCH] Compute Must Values Automatically

---
 src/ASTAnalyses/polarityassignment.cc | 43 +++++++--------------------
 src/ASTAnalyses/polarityassignment.h  |  9 +++---
 src/csolver.cc                        |  6 +++-
 3 files changed, 19 insertions(+), 39 deletions(-)

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index 6b63436..f75c9ec 100644
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -9,12 +9,10 @@ void computePolarities(CSolver *This) {
 		bool isNegated = boolean.isNegated();
 		if (isNegated) {
 			updatePolarity(b, P_FALSE);
-			updateMustValue(b, BV_MUSTBEFALSE);
 		} else {
 			updatePolarity(b, P_TRUE);
-			updateMustValue(b, BV_MUSTBETRUE);
 		}
-		computePolarityAndBooleanValue(b);
+		computePolarity(b);
 	}
 	delete iterator;
 }
@@ -27,33 +25,32 @@ void updateMustValue(Boolean *This, BooleanValue value) {
 	This->boolVal = (BooleanValue) (This->boolVal | value);
 }
 
-void computePolarityAndBooleanValue(Boolean *This) {
+void computePolarity(Boolean *This) {
 	switch (This->type) {
 	case BOOLEANVAR:
 	case ORDERCONST:
 		return;
 	case PREDICATEOP:
-		return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
+		return computePredicatePolarity((BooleanPredicate *)This);
 	case LOGICOP:
-		return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
+		return computeLogicOpPolarity((BooleanLogic *)This);
 	default:
 		ASSERT(0);
 	}
 }
 
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
+void computePredicatePolarity(BooleanPredicate *This) {
 	if (This->undefStatus) {
 		updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
-		computePolarityAndBooleanValue(This->undefStatus.getBoolean());
+		computePolarity(This->undefStatus.getBoolean());
 	}
 }
 
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
-	computeLogicOpBooleanValue(This);
-	computeLogicOpPolarity(This);
+void computeLogicOpPolarity(BooleanLogic *This) {
+	computeLogicOpPolarityChildren(This);
 	uint size = This->inputs.getSize();
 	for (uint i = 0; i < size; i++) {
-		computePolarityAndBooleanValue(This->inputs.get(i).getBoolean());
+		computePolarity(This->inputs.get(i).getBoolean());
 	}
 }
 
@@ -85,7 +82,7 @@ BooleanValue negateBooleanValue(BooleanValue This) {
 	}
 }
 
-void computeLogicOpPolarity(BooleanLogic *This) {
+void computeLogicOpPolarityChildren(BooleanLogic *This) {
 	Polarity parentpolarity = This->polarity;
 	switch (This->op) {
 	case SATC_AND: {
@@ -106,23 +103,3 @@ void computeLogicOpPolarity(BooleanLogic *This) {
 		ASSERT(0);
 	}
 }
-
-void computeLogicOpBooleanValue(BooleanLogic *This) {
-	BooleanValue parentbv = This->boolVal;
-	switch (This->op) {
-	case SATC_AND: {
-		if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
-			uint size = This->inputs.getSize();
-			for (uint i = 0; i < size; i++) {
-				BooleanEdge be=This->inputs.get(i);
-				updateMustValue(be.getBoolean(), be.isNegated()?negateBooleanValue(parentbv):parentbv);
-			}
-		}
-		return;
-	}
-	case SATC_IFF:
-		return;
-	default:
-		ASSERT(0);
-	}
-}
diff --git a/src/ASTAnalyses/polarityassignment.h b/src/ASTAnalyses/polarityassignment.h
index 6621d77..6255875 100644
--- a/src/ASTAnalyses/polarityassignment.h
+++ b/src/ASTAnalyses/polarityassignment.h
@@ -16,12 +16,11 @@
 void computePolarities(CSolver *This);
 void updatePolarity(Boolean *This, Polarity polarity);
 void updateMustValue(Boolean *This, BooleanValue value);
-void computePolarityAndBooleanValue(Boolean *boolean);
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This);
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *boolean);
+void computePolarity(Boolean *boolean);
+void computePredicatePolarity(BooleanPredicate *This);
+void computeLogicOpPolarity(BooleanLogic *boolean);
 Polarity negatePolarity(Polarity This);
 BooleanValue negateBooleanValue(BooleanValue This);
-void computeLogicOpPolarity(BooleanLogic *boolean);
-void computeLogicOpBooleanValue(BooleanLogic *boolean);
+void computeLogicOpPolarityChildren(BooleanLogic *boolean);
 
 #endif/* POLARITYASSIGNMENT_H */
diff --git a/src/csolver.cc b/src/csolver.cc
index 3e240a4..ecc237e 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -342,8 +342,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 				return;
 			}
 		}
-
 		constraints.add(constraint);
+		Boolean *ptr=constraint.getBoolean();
+		if (constraint.isNegated())
+			updateMustValue(ptr, BV_MUSTBEFALSE);
+		else
+			updateMustValue(ptr, BV_MUSTBETRUE);
 	}
 }
 
-- 
2.34.1