More edits

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index f7d3e8822b1240d5bbd75f0f92de0aa88c67f686..dcc201d24c319ee324eb63a484e39239049c2633 100644 (file)
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -28,6 +28,9 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
        order(_order),
        first(_first),
        second(_second) {
+}
+
+void BooleanOrder::updateParents() {
        order->constraints.push(this);
 }
 

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 9864d9bb3d39ff7ffcebb8ac01df2e5d93a9db80..467ceb1a24608d49eac44c2620800be6b2dea1c9 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -56,7 +56,8 @@ public:
        Boolean *clone(CSolver *solver, CloneMap *map);
        void serialize(Serializer *serializer );
        virtual void print();
-
+       void updateParents();
+       
        Order *order;
        uint64_t first;
        uint64_t second;

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 1e0426c32a00d33eb284f059269b3fbad594c50a..d5bb5cf081dd02f91f5371c38e15246ec3490ac0 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -62,18 +62,20 @@ void DecomposeOrderTransform::doTransform() {
                }
 
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-               HashsetOrderEdge *edgesRemoved = NULL;
 
                if (mustReachPrune) {
-                       edgesRemoved = new HashsetOrderEdge();
-                       removeMustBeTrueNodes(graph, edgesRemoved);
+                       removeMustBeTrueNodes(graph, dor);
+               }
+
+               bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
+
+               if (pruneEdges) {
+                       mustEdgePrune(graph, dor);
                }
 
                //This is needed for splitorder
                graph->computeStronglyConnectedComponentGraph();
-               decomposeOrder(order, graph, edgesRemoved, dor);
-               if (edgesRemoved != NULL)
-                       delete edgesRemoved;
+               decomposeOrder(order, graph, dor);
                delete graph;
        }
        delete orderit;
@@ -81,7 +83,7 @@ void DecomposeOrderTransform::doTransform() {
 }
 
 
-void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
        Vector<Order *> partialcandidatevec;
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {
@@ -90,17 +92,8 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
                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)) {
-                               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;
-                       }
-               }
+               if (from->removed || to->removed)
+                       continue;
 
                if (from->sccNum != to->sccNum) {
                        if (edge != NULL) {
@@ -158,9 +151,10 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
                                if (edge->polNeg)
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
-                       orderconstraint->order = neworder;
+                       BooleanEdge neworderconstraint=solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
+                       solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
+                                                                                                                                                                                                                                
                        dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
-                       neworder->addOrderConstraint(orderconstraint);
                }
        }
        solver->getActiveOrders()->remove(currOrder);
@@ -195,14 +189,17 @@ bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
        return true;
 }
 
-void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
        node->removed = true;
+       model_print("Removing %llu\n", node->getID());
        SetIteratorOrderEdge *iterin = node->inEdges.iterator();
        while (iterin->hasNext()) {
                OrderEdge *inEdge = iterin->next();
                OrderNode *srcNode = inEdge->source;
                srcNode->outEdges.remove(inEdge);
-               edgesRemoved->add(inEdge);
+               dor->mustOrderEdge(srcNode->getID(), node->getID());
+               BooleanEdge be=solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
+               solver->replaceBooleanWithTrue(be);
                bool removeOutgoingEdges = !iterin->hasNext();
 
                SetIteratorOrderEdge *iterout = node->outEdges.iterator();
@@ -210,8 +207,10 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                        OrderEdge *outEdge = iterout->next();
                        OrderNode *sinkNode = outEdge->sink;
                        if (removeOutgoingEdges) {
+                               dor->mustOrderEdge(node->getID(), sinkNode->getID());
                                sinkNode->inEdges.remove(outEdge);
-                               edgesRemoved->add(outEdge);
+                               BooleanEdge be2=solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
+                               solver->replaceBooleanWithTrue(be2);
                        }
                        //Adding new edge to new sink and src nodes ...
                        if (srcNode == sinkNode) {
@@ -238,13 +237,115 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
        delete iterin;
 }
 
-void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
+void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
        SetIteratorOrderNode *iterator = graph->getNodes();
        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
+               if (node->removed)
+                       continue;
                if (isMustBeTrueNode(node)) {
-                       bypassMustBeTrueNode(graph, node, edgesRemoved);
+                       bypassMustBeTrueNode(graph, node, dor);
                }
        }
        delete iterator;
 }
+
+void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
+       SetIteratorOrderNode *iterator = graph->getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (node->removed)
+                       continue;
+               attemptNodeMerge(graph, node, dor);
+       }
+       delete iterator;
+}
+
+void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
+       SetIteratorOrderEdge * edgeit = node->outEdges.iterator();
+       while(edgeit->hasNext()) {
+               OrderEdge *outedge=edgeit->next();
+               OrderNode *dstnode=outedge->sink;
+               uint numOutEdges=node->outEdges.getSize();
+               uint numInEdges=dstnode->inEdges.getSize();
+               /*
+                       Need to avoid a situation where we create new reachability by
+                       the merge.  This can only happen if there is an extra in edge to
+                       the dstnode and an extra out edge to our node.
+               */
+               
+               if (numOutEdges == 1 || numInEdges == 1) {
+                       /* Safe to do the Merge */
+                       mergeNodes(graph, node, outedge, dstnode, dor);
+                       
+                       //Throw away the iterator and start over
+                       delete edgeit;
+                       edgeit=node->outEdges.iterator();
+               }
+       }
+       delete edgeit;
+}
+
+void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
+       /* Fix up must edge between the two nodes */
+       node->outEdges.remove(edge);
+       dstnode->inEdges.remove(edge);
+       dor->mustOrderEdge(node->getID(), dstnode->getID());
+
+       /* Go through the incoming edges to the new node */
+       SetIteratorOrderEdge *inedgeit=dstnode->inEdges.iterator();
+       while(inedgeit->hasNext()) {
+               OrderEdge *inedge=inedgeit->next();
+               OrderNode *source=inedge->source;
+               //remove it from the source node
+               source->outEdges.remove(inedge);
+               //save the remapping that we did
+               dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
+               //create the new edge
+               OrderEdge *newedge=graph->getOrderEdgeFromOrderGraph(source, node);
+               //update the flags
+               newedge->polPos |= inedge->polPos;
+               newedge->polNeg |= inedge->polNeg;
+               newedge->mustPos |= inedge->mustPos;
+               newedge->mustNeg |= inedge->mustNeg;
+               newedge->pseudoPos |= inedge->pseudoPos;
+               //add new edge to both
+               source->outEdges.add(newedge);
+               node->inEdges.add(newedge);
+
+               BooleanEdge be=solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
+               BooleanEdge benew=solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
+               solver->replaceBooleanWithBoolean(be, benew);
+               
+       }
+       dstnode->inEdges.reset();
+       delete inedgeit;
+
+               /* Go through the outgoing edges from the new node */
+       SetIteratorOrderEdge *outedgeit=dstnode->outEdges.iterator();
+       while(outedgeit->hasNext()) {
+               OrderEdge *outedge=outedgeit->next();
+               OrderNode *sink=outedge->sink;
+               //remove it from the sink node
+               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
+               newedge->polPos |= outedge->polPos;
+               newedge->polNeg |= outedge->polNeg;
+               newedge->mustPos |= outedge->mustPos;
+               newedge->mustNeg |= outedge->mustNeg;
+               newedge->pseudoPos |= outedge->pseudoPos;
+               //add new edge to both
+               sink->inEdges.add(newedge);
+               node->outEdges.add(newedge);
+               //add it to the remove set
+       }
+       dstnode->outEdges.reset();
+       delete outedgeit;
+
+       /* Mark destination as removed */
+       dstnode->removed = true;
+}

diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h
index 3f8092fb890bf418624022c98b7ebde3adec00de..9020e1cd3938ff90e1d184ab4503e4579556b406 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.h
+++ b/src/ASTTransform/decomposeordertransform.h
@@ -20,9 +20,12 @@ public:
        CMEMALLOC;
 private:
        bool isMustBeTrueNode(OrderNode *node);
-       void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved);
-       void decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor);
-       void removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved);
+       void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor);
+       void decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor);
+       void removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor);
+       void mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor);
+       void attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor);
+       void mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor);
 };
 
 

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 012f420d7725bb2feb43c731d57a103b12bf8938..9edcd3c828a53cacf54deeea49bbea0e4ceae10d 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -39,6 +39,6 @@ public:
 static TunableDesc onoff(0, 1, 1);
 static TunableDesc offon(0, 1, 0);
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE};
 typedef enum Tunables Tunables;
 #endif

diff --git a/src/csolver.cc b/src/csolver.cc
index 311ad0f5052ac00ac29ff03cbdbc1082912fcd94..7fa33f2459c2d18df7dfc43683f667c4e75b3f81 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -387,9 +387,29 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 
 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
        ASSERT(first != second);
+       bool negate = false;
+       if (order->type == SATC_TOTAL) {
+               if (first > second) {
+                       uint64_t tmp = first;
+                       first = second;
+                       second = tmp;
+                       negate = true;
+               }
+       }
        Boolean *constraint = new BooleanOrder(order, first, second);
-       allBooleans.push(constraint);
-       return BooleanEdge(constraint);
+       Boolean *b = boolMap.get(constraint);
+
+       if (b == NULL) {
+               allBooleans.push(constraint);
+               boolMap.put(constraint, constraint);
+               constraint->updateParents();
+       } else {
+               delete constraint;
+               constraint = b;
+       }
+
+       BooleanEdge be=BooleanEdge(constraint);
+       return negate ? be.negate() : be;
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {