tabbing

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

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 01a667d9eb0c32c83432e9eae083c4a275911698..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
@@ -81,7 +81,7 @@ void DecomposeOrderTransform::doTransform() {
 }
 
 
-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++) {
@@ -108,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 {
@@ -203,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
@@ -233,7 +236,6 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                delete iterout;
        }
        delete iterin;
-       graph->removeNode(node);
 }
 
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {