From 5f0500d87b5e837ac5d5864510a48ae7cf225791 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 5 Sep 2017 16:15:55 -0700
Subject: [PATCH] Don't do unnecessary work in polarity computation

---
 src/ASTAnalyses/polarityassignment.cc | 61 ++++++++++++---------------
 src/ASTAnalyses/polarityassignment.h  |  6 +--
 src/Collections/structs.h             |  1 +
 3 files changed, 30 insertions(+), 38 deletions(-)

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index f75c9ec..0be8066 100644
--- a/src/ASTAnalyses/polarityassignment.cc
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -7,50 +7,50 @@ void computePolarities(CSolver *This) {
 		BooleanEdge boolean = iterator->next();
 		Boolean *b = boolean.getBoolean();
 		bool isNegated = boolean.isNegated();
-		if (isNegated) {
-			updatePolarity(b, P_FALSE);
-		} else {
-			updatePolarity(b, P_TRUE);
-		}
-		computePolarity(b);
+		computePolarity(b, isNegated ? P_FALSE : P_TRUE);
 	}
 	delete iterator;
 }
 
-void updatePolarity(Boolean *This, Polarity polarity) {
-	This->polarity = (Polarity) (This->polarity | polarity);
+bool updatePolarity(Boolean *This, Polarity polarity) {
+	Polarity oldpolarity = This->polarity;
+	Polarity newpolarity = (Polarity) (This->polarity | polarity);
+	This->polarity = newpolarity;
+	return newpolarity != oldpolarity;
 }
 
 void updateMustValue(Boolean *This, BooleanValue value) {
 	This->boolVal = (BooleanValue) (This->boolVal | value);
 }
 
-void computePolarity(Boolean *This) {
-	switch (This->type) {
-	case BOOLEANVAR:
-	case ORDERCONST:
-		return;
-	case PREDICATEOP:
-		return computePredicatePolarity((BooleanPredicate *)This);
-	case LOGICOP:
-		return computeLogicOpPolarity((BooleanLogic *)This);
-	default:
-		ASSERT(0);
+void computePolarity(Boolean *This, Polarity polarity) {
+	if (updatePolarity(This, polarity)) {
+		switch (This->type) {
+		case BOOLEANVAR:
+		case ORDERCONST:
+			return;
+		case PREDICATEOP:
+			return computePredicatePolarity((BooleanPredicate *)This);
+		case LOGICOP:
+			return computeLogicOpPolarity((BooleanLogic *)This);
+		default:
+			ASSERT(0);
+		}
 	}
 }
 
 void computePredicatePolarity(BooleanPredicate *This) {
 	if (This->undefStatus) {
-		updatePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
-		computePolarity(This->undefStatus.getBoolean());
+		computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
 	}
 }
 
 void computeLogicOpPolarity(BooleanLogic *This) {
-	computeLogicOpPolarityChildren(This);
+	Polarity child=computeLogicOpPolarityChildren(This);
 	uint size = This->inputs.getSize();
 	for (uint i = 0; i < size; i++) {
-		computePolarity(This->inputs.get(i).getBoolean());
+		BooleanEdge b=This->inputs.get(i);
+		computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
 	}
 }
 
@@ -82,22 +82,13 @@ BooleanValue negateBooleanValue(BooleanValue This) {
 	}
 }
 
-void computeLogicOpPolarityChildren(BooleanLogic *This) {
-	Polarity parentpolarity = This->polarity;
+Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
 	switch (This->op) {
 	case SATC_AND: {
-		uint size = This->inputs.getSize();
-		for (uint i = 0; i < size; i++) {
-			BooleanEdge tmp = This->inputs.get(i);
-			Boolean *btmp = tmp.getBoolean();
-			updatePolarity(btmp, tmp.isNegated() ? negatePolarity(parentpolarity) : parentpolarity);
-		}
-		break;
+		return This->polarity;
 	}
 	case SATC_IFF: {
-		updatePolarity(This->inputs.get(0).getBoolean(), P_BOTHTRUEFALSE);
-		updatePolarity(This->inputs.get(1).getBoolean(), P_BOTHTRUEFALSE);
-		break;
+		return P_BOTHTRUEFALSE;
 	}
 	default:
 		ASSERT(0);
diff --git a/src/ASTAnalyses/polarityassignment.h b/src/ASTAnalyses/polarityassignment.h
index 6255875..8873ef2 100644
--- a/src/ASTAnalyses/polarityassignment.h
+++ b/src/ASTAnalyses/polarityassignment.h
@@ -14,13 +14,13 @@
 #include "boolean.h"
 
 void computePolarities(CSolver *This);
-void updatePolarity(Boolean *This, Polarity polarity);
+bool updatePolarity(Boolean *This, Polarity polarity);
 void updateMustValue(Boolean *This, BooleanValue value);
-void computePolarity(Boolean *boolean);
+void computePolarity(Boolean *boolean, Polarity polarity);
 void computePredicatePolarity(BooleanPredicate *This);
 void computeLogicOpPolarity(BooleanLogic *boolean);
 Polarity negatePolarity(Polarity This);
 BooleanValue negateBooleanValue(BooleanValue This);
-void computeLogicOpPolarityChildren(BooleanLogic *boolean);
+Polarity computeLogicOpPolarityChildren(BooleanLogic *boolean);
 
 #endif/* POLARITYASSIGNMENT_H */
diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index ea7fa1f..f52e895 100644
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -23,6 +23,7 @@ typedef Hashset<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_ent
 typedef Hashset<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashsetOrderNode;
 typedef Hashset<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
 typedef Hashset<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashsetOrderElement;
+typedef Hashset<Boolean *, uintptr_t, 4> HashsetBoolean;
 
 typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, 4> HashtableNodeToNodeSet;
 typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
-- 
2.34.1