Edits
[satune.git] / src / ASTAnalyses / Polarity / polarityassignment.cc
index 6254832477b7abd72102e544e2d75012a026f671..ef988dd3fb0fc5b10a265d4e90e26659da9c3f00 100644 (file)
@@ -12,6 +12,22 @@ void computePolarities(CSolver *This) {
        delete iterator;
 }
 
+void updateEdgePolarity(BooleanEdge dst, BooleanEdge src) {
+       Boolean *bdst = dst.getBoolean();
+       Boolean *bsrc = src.getBoolean();
+       bool isNegated = dst.isNegated() ^ src.isNegated();
+       Polarity p = isNegated ? negatePolarity(bsrc->polarity) : bsrc->polarity;
+       updatePolarity(bdst, p);
+}
+
+void updateEdgePolarity(BooleanEdge dst, Polarity p) {
+       Boolean *bdst = dst.getBoolean();
+       bool isNegated = dst.isNegated();
+       if (isNegated)
+               p=negatePolarity(p);
+       updatePolarity(bdst, p);
+}
+
 bool updatePolarity(Boolean *This, Polarity polarity) {
        Polarity oldpolarity = This->polarity;
        Polarity newpolarity = (Polarity) (This->polarity | polarity);
@@ -54,20 +70,6 @@ void computeLogicOpPolarity(BooleanLogic *This) {
        }
 }
 
-Polarity negatePolarity(Polarity This) {
-       switch (This) {
-       case P_UNDEFINED:
-       case P_BOTHTRUEFALSE:
-               return This;
-       case P_TRUE:
-               return P_FALSE;
-       case P_FALSE:
-               return P_TRUE;
-       default:
-               ASSERT(0);
-       }
-}
-
 BooleanValue negateBooleanValue(BooleanValue This) {
        switch (This) {
        case BV_UNDEFINED:
@@ -94,3 +96,17 @@ Polarity computeLogicOpPolarityChildren(BooleanLogic *This) {
                ASSERT(0);
        }
 }
+
+Polarity negatePolarity(Polarity This) {
+       switch (This) {
+       case P_UNDEFINED:
+       case P_BOTHTRUEFALSE:
+               return This;
+       case P_TRUE:
+               return P_FALSE;
+       case P_FALSE:
+               return P_TRUE;
+       default:
+               ASSERT(0);
+       }
+}