tabbing

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

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index fd5fda8fed7fcb6fd46b18a7648b1fa564f9637f..1e0426c32a00d33eb284f059269b3fbad594c50a 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -36,21 +36,22 @@ void DecomposeOrderTransform::doTransform() {
                        continue;
                }
 
+               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
                        //makes sure we don't incorrectly optimize graphs with negative
                        //polarity edges
-                       completePartialOrderGraph(graph);
+                       graph->completePartialOrderGraph();
                }
 
                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) {
@@ -60,7 +61,6 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
-
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
                HashsetOrderEdge *edgesRemoved = NULL;
 
@@ -70,18 +70,18 @@ void DecomposeOrderTransform::doTransform() {
                }
 
                //This is needed for splitorder
-               computeStronglyConnectedComponentGraph(graph);
-               decomposeOrder(order, graph, edgesRemoved);
+               graph->computeStronglyConnectedComponentGraph();
+               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) {
-       Vector<Order *> ordervec;
+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++) {
@@ -92,9 +92,11 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
                if (edgesRemoved != NULL) {
                        if (edgesRemoved->contains(edge)) {
+                               dor->mustOrderEdge(from->getID(), to->getID());
                                solver->replaceBooleanWithTrue(orderconstraint);
                                continue;
                        } else if (edgesRemoved->contains(invedge)) {
+                               dor->mustOrderEdge(to->getID(), from->getID());
                                solver->replaceBooleanWithFalse(orderconstraint);
                                continue;
                        }
@@ -103,8 +105,11 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                if (from->sccNum != to->sccNum) {
                        if (edge != NULL) {
                                if (edge->polPos) {
+                                       dor->mustOrderEdge(from->getID(), to->getID());
                                        solver->replaceBooleanWithTrue(orderconstraint);
                                } else if (edge->polNeg) {
+                                       if (currOrder->type == SATC_TOTAL)
+                                               dor->mustOrderEdge(to->getID(), from->getID());
                                        solver->replaceBooleanWithFalse(orderconstraint);
                                } else {
                                        //This case should only be possible if constraint isn't in AST
@@ -114,6 +119,7 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                        } else {
                                if (invedge != NULL) {
                                        if (invedge->polPos) {
+                                               dor->mustOrderEdge(to->getID(), from->getID());
                                                solver->replaceBooleanWithFalse(orderconstraint);
                                        } else if (edge->polNeg) {
                                                //This case shouldn't happen...  If we have a partial order,
@@ -130,12 +136,11 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                } else {
                        //Build new order and change constraint's order
                        Order *neworder = NULL;
-                       if (ordervec.getSize() > from->sccNum)
-                               neworder = ordervec.get(from->sccNum);
+                       neworder = dor->getOrder(from->sccNum);
                        if (neworder == NULL) {
                                MutableSet *set = solver->createMutableSet(currOrder->set->getType());
                                neworder = solver->createOrder(currOrder->type, set);
-                               ordervec.setExpand(from->sccNum, neworder);
+                               dor->setOrder(from->sccNum, neworder);
                                if (currOrder->type == SATC_PARTIAL)
                                        partialcandidatevec.setExpand(from->sccNum, neworder);
                                else
@@ -154,10 +159,10 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
                        orderconstraint->order = neworder;
+                       dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
                        neworder->addOrderConstraint(orderconstraint);
                }
        }
-       currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
        solver->getActiveOrders()->remove(currOrder);
        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
@@ -191,18 +196,23 @@ bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
 }
 
 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+       node->removed = true;
        SetIteratorOrderEdge *iterin = node->inEdges.iterator();
        while (iterin->hasNext()) {
                OrderEdge *inEdge = iterin->next();
                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();