Bug fix for removing must edges...They also need to update constraints

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

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 3b8571d4fd3f37e5aea1b30908d9f5d3d1103b74..fd5fda8fed7fcb6fd46b18a7648b1fa564f9637f 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -62,20 +62,25 @@ void DecomposeOrderTransform::doTransform() {
 
 
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+               HashsetOrderEdge *edgesRemoved = NULL;
 
-               if (mustReachPrune)
-                       removeMustBeTrueNodes(solver, graph);
+               if (mustReachPrune) {
+                       edgesRemoved = new HashsetOrderEdge();
+                       removeMustBeTrueNodes(graph, edgesRemoved);
+               }
 
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
-               decomposeOrder(order, graph);
+               decomposeOrder(order, graph, edgesRemoved);
+               if (edgesRemoved != NULL)
+                       delete edgesRemoved;
        }
        delete orderit;
        delete orders;
 }
 
 
-void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
+void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved) {
        Vector<Order *> ordervec;
        Vector<Order *> partialcandidatevec;
        uint size = currOrder->constraints.getSize();
@@ -83,8 +88,19 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                BooleanOrder *orderconstraint = currOrder->constraints.get(i);
                OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
                OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
+               OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
+               OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
+               if (edgesRemoved != NULL) {
+                       if (edgesRemoved->contains(edge)) {
+                               solver->replaceBooleanWithTrue(orderconstraint);
+                               continue;
+                       } else if (edgesRemoved->contains(invedge)) {
+                               solver->replaceBooleanWithFalse(orderconstraint);
+                               continue;
+                       }
+               }
+
                if (from->sccNum != to->sccNum) {
-                       OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
                        if (edge != NULL) {
                                if (edge->polPos) {
                                        solver->replaceBooleanWithTrue(orderconstraint);
@@ -96,7 +112,6 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                                        ;
                                }
                        } else {
-                               OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
                                if (invedge != NULL) {
                                        if (invedge->polPos) {
                                                solver->replaceBooleanWithFalse(orderconstraint);
@@ -135,7 +150,6 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                                ((MutableSet *)neworder->set)->addElementMSet(to->id);
                        }
                        if (currOrder->type == SATC_PARTIAL) {
-                               OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
                                if (edge->polNeg)
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
@@ -153,3 +167,74 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                }
        }
 }
+
+bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
+       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (!edge->mustPos) {
+                       delete iterator;
+                       return false;
+               }
+       }
+       delete iterator;
+       iterator = node->outEdges.iterator();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (!edge->mustPos) {
+                       delete iterator;
+                       return false;
+               }
+       }
+       delete iterator;
+       return true;
+}
+
+void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+       SetIteratorOrderEdge *iterin = node->inEdges.iterator();
+       while (iterin->hasNext()) {
+               OrderEdge *inEdge = iterin->next();
+               OrderNode *srcNode = inEdge->source;
+               srcNode->outEdges.remove(inEdge);
+               edgesRemoved->add(inEdge);
+               SetIteratorOrderEdge *iterout = node->outEdges.iterator();
+               while (iterout->hasNext()) {
+                       OrderEdge *outEdge = iterout->next();
+                       OrderNode *sinkNode = outEdge->sink;
+                       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;
+                               return;
+                       }
+                       //Add new order constraint
+                       BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+                       solver->addConstraint(orderconstraint);
+
+                       //Add new edge
+                       OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
+                       newEdge->mustPos = true;
+                       newEdge->polPos = true;
+                       if (newEdge->mustNeg)
+                               solver->setUnSAT();
+                       srcNode->outEdges.add(newEdge);
+                       sinkNode->inEdges.add(newEdge);
+               }
+               delete iterout;
+       }
+       delete iterin;
+}
+
+void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
+       SetIteratorOrderNode *iterator = graph->getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (isMustBeTrueNode(node)) {
+                       bypassMustBeTrueNode(graph, node, edgesRemoved);
+               }
+       }
+       delete iterator;
+}