Don't do unnecessary work in polarity computation

diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
index f75c9ece2b11f5178c39e3ac4dbfc2c79a145824..0be806623602a3ae1d59fbce9e073d2a24c91a80 100644 (file)
--- 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 625587543b2e86131320baab2b4da189c365fec0..8873ef247f6ae1238c745ab7fb8b070c77effbad 100644 (file)
--- 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 ea7fa1f138dce7fe0fffeab80239f51eaf3460c7..f52e895830c1c7e503f5e4411fd0bae49fb070a1 100644 (file)
--- 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;