tabbing

[satune.git] / src / ASTTransform / decomposeordertransform.cc

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index d4a2d5faf9a6d3836b398a5d8f4ae750f0895cbf..1e0426c32a00d33eb284f059269b3fbad594c50a 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -36,9 +36,9 @@ void DecomposeOrderTransform::doTransform() {
                        continue;
                }
 
-               DecomposeOrderResolver *dor=new DecomposeOrderResolver(order);
+               DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
                order->setOrderResolver(dor);
-               
+
                OrderGraph *graph = buildOrderGraph(order);
                if (order->type == SATC_PARTIAL) {
                        //Required to do SCC analysis for partial order graphs.  It
@@ -48,12 +48,10 @@ void DecomposeOrderTransform::doTransform() {
                }
 
                bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
-
                if (mustReachGlobal)
                        reachMustAnalysis(solver, graph, false);
 
                bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-
                if (mustReachLocal) {
                        //This pair of analysis is also optional
                        if (order->type == SATC_PARTIAL) {
@@ -76,13 +74,14 @@ void DecomposeOrderTransform::doTransform() {
                decomposeOrder(order, graph, edgesRemoved, dor);
                if (edgesRemoved != NULL)
                        delete edgesRemoved;
+               delete graph;
        }
        delete orderit;
        delete orders;
 }
 
 
-void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
        Vector<Order *> partialcandidatevec;
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {
@@ -109,7 +108,7 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                                        dor->mustOrderEdge(from->getID(), to->getID());
                                        solver->replaceBooleanWithTrue(orderconstraint);
                                } else if (edge->polNeg) {
-                                       if (currOrder->type == SATC_TOTAL)                                      
+                                       if (currOrder->type == SATC_TOTAL)
                                                dor->mustOrderEdge(to->getID(), from->getID());
                                        solver->replaceBooleanWithFalse(orderconstraint);
                                } else {
@@ -204,18 +203,21 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                OrderNode *srcNode = inEdge->source;
                srcNode->outEdges.remove(inEdge);
                edgesRemoved->add(inEdge);
+               bool removeOutgoingEdges = !iterin->hasNext();
+
                SetIteratorOrderEdge *iterout = node->outEdges.iterator();
                while (iterout->hasNext()) {
                        OrderEdge *outEdge = iterout->next();
                        OrderNode *sinkNode = outEdge->sink;
-                       sinkNode->inEdges.remove(outEdge);
-                       edgesRemoved->add(outEdge);
+                       if (removeOutgoingEdges) {
+                               sinkNode->inEdges.remove(outEdge);
+                               edgesRemoved->add(outEdge);
+                       }
                        //Adding new edge to new sink and src nodes ...
                        if (srcNode == sinkNode) {
                                solver->setUnSAT();
                                delete iterout;
                                delete iterin;
-                               graph->removeNode(node);
                                return;
                        }
                        //Add new order constraint
@@ -234,7 +236,6 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                delete iterout;
        }
        delete iterin;
-       graph->removeNode(node);
 }
 
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {