bug fix
[satune.git] / src / ASTTransform / decomposeordertransform.cc
index f629a76b5815a3b8b071e2fcd7162c46295b6e17..6da5e4aa5eb3765c87fe921bc48f749c033e69f0 100644 (file)
@@ -16,6 +16,7 @@
 #include "decomposeorderresolver.h"
 #include "tunable.h"
 #include "orderanalysis.h"
+#include "polarityassignment.h"
 
 
 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
@@ -153,7 +154,7 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
                        }
                        BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
                        solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
-
+                       updateEdgePolarity(neworderconstraint, orderconstraint);
                        dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
                }
        }
@@ -213,6 +214,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                        }
                        //Add new order constraint
                        BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+                       updateEdgePolarity(orderconstraint, P_TRUE);
                        solver->addConstraint(orderconstraint);
 
                        //Add new edge
@@ -244,7 +246,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->removed)
                        continue;
                if (isMustBeTrueNode(node)) {
@@ -257,7 +259,7 @@ void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, Decompose
 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
+               OrderNode *node = (OrderNode *)iterator->next();
                if (node->removed)
                        continue;
                attemptNodeMerge(graph, node, dor);
@@ -325,7 +327,13 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 
                BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
-               solver->replaceBooleanWithBoolean(be, benew);
+               updateEdgePolarity(benew, be);
+               if (solver->isTrue(benew))
+                 solver->replaceBooleanWithTrue(be);
+               else if (solver->isFalse(benew))
+                 solver->replaceBooleanWithFalse(be);
+               else
+                 solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->inEdges.reset();
        delete inedgeit;
@@ -339,6 +347,7 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                sink->inEdges.remove(outedge);
                //save the remapping that we did
                dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
+
                //create the new edge
                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
                //update the flags
@@ -353,7 +362,13 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 
                BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
-               solver->replaceBooleanWithBoolean(be, benew);
+               updateEdgePolarity(benew, be);
+               if (solver->isTrue(benew))
+                 solver->replaceBooleanWithTrue(be);
+               else if (solver->isFalse(benew))
+                 solver->replaceBooleanWithFalse(be);
+               else
+                 solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->outEdges.reset();
        delete outedgeit;