edits
authorbdemsky <bdemsky@uci.edu>
Sat, 21 Oct 2017 22:55:40 +0000 (15:55 -0700)
committerbdemsky <bdemsky@uci.edu>
Sat, 21 Oct 2017 22:55:40 +0000 (15:55 -0700)
src/ASTAnalyses/Order/orderanalysis.cc
src/ASTAnalyses/Order/orderanalysis.h
src/ASTAnalyses/Order/ordergraph.cc
src/ASTAnalyses/Order/ordergraph.h
src/ASTTransform/decomposeordertransform.cc
src/ASTTransform/decomposeordertransform.h
src/Collections/structs.cc
src/Collections/structs.h
src/Translator/decomposeorderresolver.cc
src/Translator/decomposeorderresolver.h
src/classlist.h

index 13e26c07eca66a0cfa32c20b115340e0bbf07085..abec0c05a34eefbe191827e72852a0a62445b3db 100644 (file)
 #include "mutableset.h"
 #include "tunable.h"
 
 #include "mutableset.h"
 #include "tunable.h"
 
-void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSNodeVisit(node, finishNodes, false, false, 0);
-                       node->status = FINISHED;
-                       finishNodes->push(node);
-               }
-       }
-       delete iterator;
-}
-
-void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       uint size = finishNodes->getSize();
-       uint sccNum = 1;
-       for (int i = size - 1; i >= 0; i--) {
-               OrderNode *node = finishNodes->get(i);
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSNodeVisit(node, NULL, true, false, sccNum);
-                       node->sccNum = sccNum;
-                       node->status = FINISHED;
-                       sccNum++;
-               }
-       }
-}
-
-void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
-       SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (mustvisit) {
-                       if (!edge->mustPos)
-                               continue;
-               } else
-               if (!edge->polPos && !edge->pseudoPos)          //Ignore edges that do not have positive polarity
-                       continue;
-
-               OrderNode *child = isReverse ? edge->source : edge->sink;
-               if (child->status == NOTVISITED) {
-                       child->status = VISITED;
-                       DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
-                       child->status = FINISHED;
-                       if (finishNodes != NULL) {
-                               finishNodes->push(child);
-                       }
-                       if (isReverse)
-                               child->sccNum = sccNum;
-               }
-       }
-       delete iterator;
-}
-
-void resetNodeInfoStatusSCC(OrderGraph *graph) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               iterator->next()->status = NOTVISITED;
-       }
-       delete iterator;
-}
-
-void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
-       Vector<OrderNode *> finishNodes;
-       DFS(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-       DFSReverse(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-}
-
-
-
-/** This function computes a source set for every nodes, the set of
-    nodes that can reach that node via pospolarity edges.  It then
-    looks for negative polarity edges from nodes in the the source set
-    to determine whether we need to generate pseudoPos edges. */
-
-void completePartialOrderGraph(OrderGraph *graph) {
-       Vector<OrderNode *> finishNodes;
-       DFS(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
-       HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
-
-       Vector<OrderNode *> sccNodes;
-
-       uint size = finishNodes.getSize();
-       uint sccNum = 1;
-       for (int i = size - 1; i >= 0; i--) {
-               OrderNode *node = finishNodes.get(i);
-               HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
-               table->put(node, sources);
-
-               if (node->status == NOTVISITED) {
-                       //Need to do reverse traversal here...
-                       node->status = VISITED;
-                       DFSNodeVisit(node, &sccNodes, true, false, sccNum);
-                       node->status = FINISHED;
-                       node->sccNum = sccNum;
-                       sccNum++;
-                       sccNodes.push(node);
-
-                       //Compute in set for entire SCC
-                       uint rSize = sccNodes.getSize();
-                       for (uint j = 0; j < rSize; j++) {
-                               OrderNode *rnode = sccNodes.get(j);
-                               //Compute source sets
-                               SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
-                               while (iterator->hasNext()) {
-                                       OrderEdge *edge = iterator->next();
-                                       OrderNode *parent = edge->source;
-                                       if (edge->polPos) {
-                                               sources->add(parent);
-                                               HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
-                                               sources->addAll(parent_srcs);
-                                       }
-                               }
-                               delete iterator;
-                       }
-                       for (uint j = 0; j < rSize; j++) {
-                               //Copy in set of entire SCC
-                               OrderNode *rnode = sccNodes.get(j);
-                               HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
-                               table->put(rnode, set);
-
-                               //Use source sets to compute pseudoPos edges
-                               SetIteratorOrderEdge *iterator = node->inEdges.iterator();
-                               while (iterator->hasNext()) {
-                                       OrderEdge *edge = iterator->next();
-                                       OrderNode *parent = edge->source;
-                                       ASSERT(parent != rnode);
-                                       if (edge->polNeg && parent->sccNum != rnode->sccNum &&
-                                                       sources->contains(parent)) {
-                                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
-                                               newedge->pseudoPos = true;
-                                       }
-                               }
-                               delete iterator;
-                       }
-
-                       sccNodes.clear();
-               }
-       }
-
-       table->resetAndDeleteVals();
-       delete table;
-       resetNodeInfoStatusSCC(graph);
-}
-
-void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSNodeVisit(node, finishNodes, false, true, 0);
-                       node->status = FINISHED;
-                       finishNodes->push(node);
-               }
-       }
-       delete iterator;
-}
-
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
        uint size = finishNodes->getSize();
        HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
        uint size = finishNodes->getSize();
        HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
@@ -257,8 +94,8 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
        Vector<OrderNode *> finishNodes;
        //Topologically sort the mustPos edge graph
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
        Vector<OrderNode *> finishNodes;
        //Topologically sort the mustPos edge graph
-       DFSMust(graph, &finishNodes);
-       resetNodeInfoStatusSCC(graph);
+       graph->DFSMust(&finishNodes);
+       graph->resetNodeInfoStatusSCC();
 
        //Find any backwards edges that complete cycles and force them to be mustNeg
        DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 
        //Find any backwards edges that complete cycles and force them to be mustNeg
        DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
index 89665a1fed0353bc4c01cfa8a77f287aa9978faf..24ec85c3e357766b411c4dac80f5834afb9f2103 100644 (file)
@@ -4,14 +4,6 @@
 #include "structs.h"
 #include "mymemory.h"
 
 #include "structs.h"
 #include "mymemory.h"
 
-void computeStronglyConnectedComponentGraph(OrderGraph *graph);
-void initializeNodeInfoSCC(OrderGraph *graph);
-void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
-void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
-void completePartialOrderGraph(OrderGraph *graph);
-void resetNodeInfoStatusSCC(OrderGraph *graph);
-void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
index 07d7f7fb432bd60537e41d8edddc153b5bb1ffff..a2e52f807d2db417b436eb9a1d728daf9d96f3f5 100644 (file)
@@ -6,8 +6,6 @@
 #include "order.h"
 
 OrderGraph::OrderGraph(Order *_order) :
 #include "order.h"
 
 OrderGraph::OrderGraph(Order *_order) :
-       nodes(new HashsetOrderNode()),
-       edges(new HashsetOrderEdge()),
        order(_order) {
 }
 
        order(_order) {
 }
 
@@ -110,43 +108,44 @@ void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrd
 
 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
        OrderNode *node = new OrderNode(id);
 
 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
        OrderNode *node = new OrderNode(id);
-       OrderNode *tmp = nodes->get(node);
+       OrderNode *tmp = nodes.get(node);
        if ( tmp != NULL) {
                delete node;
                node = tmp;
        } else {
        if ( tmp != NULL) {
                delete node;
                node = tmp;
        } else {
-               nodes->add(node);
+               nodes.add(node);
+               allNodes.push(node);
        }
        return node;
 }
 
 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
        OrderNode node(id);
        }
        return node;
 }
 
 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
        OrderNode node(id);
-       OrderNode *tmp = nodes->get(&node);
+       OrderNode *tmp = nodes.get(&node);
        return tmp;
 }
 
 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
        OrderEdge *edge = new OrderEdge(begin, end);
        return tmp;
 }
 
 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
        OrderEdge *edge = new OrderEdge(begin, end);
-       OrderEdge *tmp = edges->get(edge);
+       OrderEdge *tmp = edges.get(edge);
        if ( tmp != NULL ) {
                delete edge;
                edge = tmp;
        } else {
        if ( tmp != NULL ) {
                delete edge;
                edge = tmp;
        } else {
-               edges->add(edge);
+               edges.add(edge);
        }
        return edge;
 }
 
 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
        OrderEdge edge(begin, end);
        }
        return edge;
 }
 
 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
        OrderEdge edge(begin, end);
-       OrderEdge *tmp = edges->get(&edge);
+       OrderEdge *tmp = edges.get(&edge);
        return tmp;
 }
 
 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
        OrderEdge inverseedge(edge->sink, edge->source);
        return tmp;
 }
 
 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
        OrderEdge inverseedge(edge->sink, edge->source);
-       OrderEdge *tmp = edges->get(&inverseedge);
+       OrderEdge *tmp = edges.get(&inverseedge);
        return tmp;
 }
 
        return tmp;
 }
 
@@ -163,21 +162,16 @@ void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 }
 
 OrderGraph::~OrderGraph() {
 }
 
 OrderGraph::~OrderGraph() {
-       SetIteratorOrderNode *iterator = nodes->iterator();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               delete node;
-       }
-       delete iterator;
+       uint size=allNodes.getSize();
+       for(uint i=0;i<size;i++)
+               delete allNodes.get(i);
 
 
-       SetIteratorOrderEdge *eiterator = edges->iterator();
+       SetIteratorOrderEdge *eiterator = edges.iterator();
        while (eiterator->hasNext()) {
                OrderEdge *edge = eiterator->next();
                delete edge;
        }
        delete eiterator;
        while (eiterator->hasNext()) {
                OrderEdge *edge = eiterator->next();
                delete edge;
        }
        delete eiterator;
-       delete nodes;
-       delete edges;
 }
 
 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
 }
 
 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
@@ -227,3 +221,164 @@ bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current,
        delete iterator;
        return found;
 }
        delete iterator;
        return found;
 }
+
+void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
+       SetIteratorOrderNode *iterator = getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (node->status == NOTVISITED) {
+                       node->status = VISITED;
+                       DFSNodeVisit(node, finishNodes, false, false, 0);
+                       node->status = FINISHED;
+                       finishNodes->push(node);
+               }
+       }
+       delete iterator;
+}
+
+void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
+       SetIteratorOrderNode *iterator = getNodes();
+       while (iterator->hasNext()) {
+               OrderNode *node = iterator->next();
+               if (node->status == NOTVISITED) {
+                       node->status = VISITED;
+                       DFSNodeVisit(node, finishNodes, false, true, 0);
+                       node->status = FINISHED;
+                       finishNodes->push(node);
+               }
+       }
+       delete iterator;
+}
+
+void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
+       uint size = finishNodes->getSize();
+       uint sccNum = 1;
+       for (int i = size - 1; i >= 0; i--) {
+               OrderNode *node = finishNodes->get(i);
+               if (node->status == NOTVISITED) {
+                       node->status = VISITED;
+                       DFSNodeVisit(node, NULL, true, false, sccNum);
+                       node->sccNum = sccNum;
+                       node->status = FINISHED;
+                       sccNum++;
+               }
+       }
+}
+
+void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
+       SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
+       while (iterator->hasNext()) {
+               OrderEdge *edge = iterator->next();
+               if (mustvisit) {
+                       if (!edge->mustPos)
+                               continue;
+               } else
+               if (!edge->polPos && !edge->pseudoPos)          //Ignore edges that do not have positive polarity
+                       continue;
+
+               OrderNode *child = isReverse ? edge->source : edge->sink;
+               if (child->status == NOTVISITED) {
+                       child->status = VISITED;
+                       DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
+                       child->status = FINISHED;
+                       if (finishNodes != NULL) {
+                               finishNodes->push(child);
+                       }
+                       if (isReverse)
+                               child->sccNum = sccNum;
+               }
+       }
+       delete iterator;
+}
+
+void OrderGraph::resetNodeInfoStatusSCC() {
+       SetIteratorOrderNode *iterator = getNodes();
+       while (iterator->hasNext()) {
+               iterator->next()->status = NOTVISITED;
+       }
+       delete iterator;
+}
+
+void OrderGraph::computeStronglyConnectedComponentGraph() {
+       Vector<OrderNode *> finishNodes;
+       DFS(&finishNodes);
+       resetNodeInfoStatusSCC();
+       DFSReverse(&finishNodes);
+       resetNodeInfoStatusSCC();
+}
+
+/** This function computes a source set for every nodes, the set of
+    nodes that can reach that node via pospolarity edges.  It then
+    looks for negative polarity edges from nodes in the the source set
+    to determine whether we need to generate pseudoPos edges. */
+
+void OrderGraph::completePartialOrderGraph() {
+       Vector<OrderNode *> finishNodes;
+       DFS(&finishNodes);
+       resetNodeInfoStatusSCC();
+       HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
+
+       Vector<OrderNode *> sccNodes;
+
+       uint size = finishNodes.getSize();
+       uint sccNum = 1;
+       for (int i = size - 1; i >= 0; i--) {
+               OrderNode *node = finishNodes.get(i);
+               HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
+               table->put(node, sources);
+
+               if (node->status == NOTVISITED) {
+                       //Need to do reverse traversal here...
+                       node->status = VISITED;
+                       DFSNodeVisit(node, &sccNodes, true, false, sccNum);
+                       node->status = FINISHED;
+                       node->sccNum = sccNum;
+                       sccNum++;
+                       sccNodes.push(node);
+
+                       //Compute in set for entire SCC
+                       uint rSize = sccNodes.getSize();
+                       for (uint j = 0; j < rSize; j++) {
+                               OrderNode *rnode = sccNodes.get(j);
+                               //Compute source sets
+                               SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
+                               while (iterator->hasNext()) {
+                                       OrderEdge *edge = iterator->next();
+                                       OrderNode *parent = edge->source;
+                                       if (edge->polPos) {
+                                               sources->add(parent);
+                                               HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
+                                               sources->addAll(parent_srcs);
+                                       }
+                               }
+                               delete iterator;
+                       }
+                       for (uint j = 0; j < rSize; j++) {
+                               //Copy in set of entire SCC
+                               OrderNode *rnode = sccNodes.get(j);
+                               HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
+                               table->put(rnode, set);
+
+                               //Use source sets to compute pseudoPos edges
+                               SetIteratorOrderEdge *iterator = node->inEdges.iterator();
+                               while (iterator->hasNext()) {
+                                       OrderEdge *edge = iterator->next();
+                                       OrderNode *parent = edge->source;
+                                       ASSERT(parent != rnode);
+                                       if (edge->polNeg && parent->sccNum != rnode->sccNum &&
+                                                       sources->contains(parent)) {
+                                               OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
+                                               newedge->pseudoPos = true;
+                                       }
+                               }
+                               delete iterator;
+                       }
+
+                       sccNodes.clear();
+               }
+       }
+
+       table->resetAndDeleteVals();
+       delete table;
+       resetNodeInfoStatusSCC();
+}
index 2bb8812351e695bebb2d7ef2490cb61b3da5164c..7460b20ebaf15070275635ffb220a16a6a91d3de 100644 (file)
@@ -27,14 +27,23 @@ public:
        Order *getOrder() {return order;}
        bool isTherePath(OrderNode *source, OrderNode *destination);
        bool isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination);
        Order *getOrder() {return order;}
        bool isTherePath(OrderNode *source, OrderNode *destination);
        bool isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination);
-       SetIteratorOrderNode *getNodes() {return nodes->iterator();}
-       SetIteratorOrderEdge *getEdges() {return edges->iterator();}
-
+       SetIteratorOrderNode *getNodes() {return nodes.iterator();}
+       SetIteratorOrderEdge *getEdges() {return edges.iterator();}
+       void DFS(Vector<OrderNode *> *finishNodes);
+       void DFSMust(Vector<OrderNode *> *finishNodes);
+       void computeStronglyConnectedComponentGraph();
+       void resetNodeInfoStatusSCC();
+       void completePartialOrderGraph();
+       void removeNode(OrderNode *node) {nodes.remove(node);}
+       
        CMEMALLOC;
 private:
        CMEMALLOC;
 private:
-       HashsetOrderNode *nodes;
-       HashsetOrderEdge *edges;
+       HashsetOrderNode nodes;
+       Vector<OrderNode *> allNodes;
+       HashsetOrderEdge edges;
        Order *order;
        Order *order;
+       void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
+       void DFSReverse(Vector<OrderNode *> *finishNodes);
 };
 
 OrderGraph *buildOrderGraph(Order *order);
 };
 
 OrderGraph *buildOrderGraph(Order *order);
index 51d6a51b1f0d14401638c45b963b8f48827982f4..d4a2d5faf9a6d3836b398a5d8f4ae750f0895cbf 100644 (file)
@@ -36,12 +36,15 @@ void DecomposeOrderTransform::doTransform() {
                        continue;
                }
 
                        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
                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);
                }
 
                bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
@@ -60,7 +63,6 @@ void DecomposeOrderTransform::doTransform() {
                        }
                }
 
                        }
                }
 
-
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
                HashsetOrderEdge *edgesRemoved = NULL;
 
                bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
                HashsetOrderEdge *edgesRemoved = NULL;
 
@@ -70,8 +72,8 @@ void DecomposeOrderTransform::doTransform() {
                }
 
                //This is needed for splitorder
                }
 
                //This is needed for splitorder
-               computeStronglyConnectedComponentGraph(graph);
-               decomposeOrder(order, graph, edgesRemoved);
+               graph->computeStronglyConnectedComponentGraph();
+               decomposeOrder(order, graph, edgesRemoved, dor);
                if (edgesRemoved != NULL)
                        delete edgesRemoved;
        }
                if (edgesRemoved != NULL)
                        delete edgesRemoved;
        }
@@ -80,8 +82,7 @@ void DecomposeOrderTransform::doTransform() {
 }
 
 
 }
 
 
-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++) {
        Vector<Order *> partialcandidatevec;
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {
@@ -92,9 +93,11 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
                if (edgesRemoved != NULL) {
                        if (edgesRemoved->contains(edge)) {
                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)) {
                                solver->replaceBooleanWithTrue(orderconstraint);
                                continue;
                        } else if (edgesRemoved->contains(invedge)) {
+                               dor->mustOrderEdge(to->getID(), from->getID());
                                solver->replaceBooleanWithFalse(orderconstraint);
                                continue;
                        }
                                solver->replaceBooleanWithFalse(orderconstraint);
                                continue;
                        }
@@ -103,8 +106,11 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                if (from->sccNum != to->sccNum) {
                        if (edge != NULL) {
                                if (edge->polPos) {
                if (from->sccNum != to->sccNum) {
                        if (edge != NULL) {
                                if (edge->polPos) {
+                                       dor->mustOrderEdge(from->getID(), to->getID());
                                        solver->replaceBooleanWithTrue(orderconstraint);
                                } else if (edge->polNeg) {
                                        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
                                        solver->replaceBooleanWithFalse(orderconstraint);
                                } else {
                                        //This case should only be possible if constraint isn't in AST
@@ -114,6 +120,7 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                        } else {
                                if (invedge != NULL) {
                                        if (invedge->polPos) {
                        } 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,
                                                solver->replaceBooleanWithFalse(orderconstraint);
                                        } else if (edge->polNeg) {
                                                //This case shouldn't happen...  If we have a partial order,
@@ -130,12 +137,11 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                } else {
                        //Build new order and change constraint's order
                        Order *neworder = NULL;
                } 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);
                        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
                                if (currOrder->type == SATC_PARTIAL)
                                        partialcandidatevec.setExpand(from->sccNum, neworder);
                                else
@@ -154,10 +160,10 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
                        orderconstraint->order = neworder;
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
                        orderconstraint->order = neworder;
+                       dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
                        neworder->addOrderConstraint(orderconstraint);
                }
        }
                        neworder->addOrderConstraint(orderconstraint);
                }
        }
-       currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
        solver->getActiveOrders()->remove(currOrder);
        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
        solver->getActiveOrders()->remove(currOrder);
        uint pcvsize = partialcandidatevec.getSize();
        for (uint i = 0; i < pcvsize; i++) {
@@ -209,6 +215,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                                solver->setUnSAT();
                                delete iterout;
                                delete iterin;
                                solver->setUnSAT();
                                delete iterout;
                                delete iterin;
+                               graph->removeNode(node);
                                return;
                        }
                        //Add new order constraint
                                return;
                        }
                        //Add new order constraint
@@ -227,6 +234,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                delete iterout;
        }
        delete iterin;
                delete iterout;
        }
        delete iterin;
+       graph->removeNode(node);
 }
 
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
 }
 
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
index 8351ae0f632af276b3338913370665e06993225d..3f8092fb890bf418624022c98b7ebde3adec00de 100644 (file)
@@ -21,7 +21,7 @@ public:
 private:
        bool isMustBeTrueNode(OrderNode *node);
        void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved);
 private:
        bool isMustBeTrueNode(OrderNode *node);
        void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved);
-       void decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved);
+       void decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor);
        void removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved);
 };
 
        void removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved);
 };
 
index 96b85e7dc1aedb6fd9ae8228ed63f31582777af4..09dc41922a2f9d6511b4288b1bdeaeaf7acac519 100644 (file)
@@ -6,6 +6,7 @@
 #include "ordergraph.h"
 #include "orderelement.h"
 #include "structs.h"
 #include "ordergraph.h"
 #include "orderelement.h"
 #include "structs.h"
+#include "decomposeorderresolver.h"
 
 unsigned int table_entry_hash_function(TableEntry *This) {
        unsigned int h = 0;
 
 unsigned int table_entry_hash_function(TableEntry *This) {
        unsigned int h = 0;
@@ -56,3 +57,12 @@ unsigned int order_pair_hash_function(OrderPair *This) {
 bool order_pair_equals(OrderPair *key1, OrderPair *key2) {
        return key1->first == key2->first && key1->second == key2->second;
 }
 bool order_pair_equals(OrderPair *key1, OrderPair *key2) {
        return key1->first == key2->first && key1->second == key2->second;
 }
+
+unsigned int doredge_hash_function(DOREdge *key) {
+       return (uint) (key->newfirst << 2) ^ key->newsecond;
+}
+
+bool doredge_equals(DOREdge *key1, DOREdge *key2) {
+       return key1->newfirst == key2->newfirst &&
+               key1->newsecond == key2->newsecond;
+}
index 6d06f549d616b3b869d0022b5b6938ced17a12fa..2515f8f09969907fd7411004bbad782fdd4a8002 100644 (file)
@@ -19,11 +19,15 @@ bool order_element_equals(OrderElement *key1, OrderElement *key2);
 unsigned int order_pair_hash_function(OrderPair *This);
 bool order_pair_equals(OrderPair *key1, OrderPair *key2);
 
 unsigned int order_pair_hash_function(OrderPair *This);
 bool order_pair_equals(OrderPair *key1, OrderPair *key2);
 
+unsigned int doredge_hash_function(DOREdge *key);
+bool doredge_equals(DOREdge *key1, DOREdge *key2);
+
 
 typedef Hashset<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
 typedef Hashset<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> HashsetOrderNode;
 typedef Hashset<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
 typedef Hashset<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> HashsetOrderElement;
 
 typedef Hashset<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
 typedef Hashset<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> HashsetOrderNode;
 typedef Hashset<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
 typedef Hashset<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> HashsetOrderElement;
+typedef Hashset<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> HashsetDOREdge;
 typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
 typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
 typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
 typedef Hashset<Boolean *, uintptr_t, PTRSHIFT> HashsetBoolean;
 typedef Hashset<Element *, uintptr_t, PTRSHIFT> HashsetElement;
 typedef SetIterator<Boolean *, uintptr_t, PTRSHIFT> SetIteratorBoolean;
@@ -43,5 +47,5 @@ typedef SetIterator<TableEntry *, uintptr_t, PTRSHIFT, table_entry_hash_function
 typedef SetIterator<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
 typedef SetIterator<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
 typedef SetIterator<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
 typedef SetIterator<OrderEdge *, uintptr_t, PTRSHIFT, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
 typedef SetIterator<OrderNode *, uintptr_t, PTRSHIFT, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
 typedef SetIterator<OrderElement *, uintptr_t, PTRSHIFT, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
-
+typedef SetIterator<DOREdge *, uintptr_t, PTRSHIFT, doredge_hash_function, doredge_equals> SetIteratorDOREdge;
 #endif
 #endif
index 1e5fdf0cca7dc43cee7fc532e938aaed665e5bae..f0d3e2aa738812e6af2c24ef0c32edbeda41d750 100644 (file)
 #include "ordernode.h"
 #include "ordergraph.h"
 
 #include "ordernode.h"
 #include "ordergraph.h"
 
-DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order *> &_orders) :
-       graph(_graph),
-       orders(_orders.getSize(), _orders.expose())
+DecomposeOrderResolver::DecomposeOrderResolver(Order * _order) :
+       graph(NULL),
+       order(_order)
 {
 }
 
 DecomposeOrderResolver::~DecomposeOrderResolver() {
 {
 }
 
 DecomposeOrderResolver::~DecomposeOrderResolver() {
+       if (graph != NULL)
+               delete graph;
+       uint size=edges.getSize();
+       edges.resetAndDelete();
 }
 
 }
 
-void processNode(HashsetOrderNode * set, OrderNode *node, bool outedges) {
-       if (node->removed) {
-               Vector<OrderNode *> toprocess;
-               HashsetOrderNode visited;
-               toprocess.push(node);
-               while(toprocess.getSize()!=0) {
-                       OrderNode *newnode=toprocess.last();toprocess.pop();
-                       SetIteratorOrderEdge *iterator=outedges ? newnode->outEdges.iterator() : newnode->inEdges.iterator();
-                       while(iterator->hasNext()) {
-                               OrderEdge *edge=iterator->next();
-                               OrderNode *tmpnode=outedges ? edge->sink : edge->source;
-                               if (tmpnode->removed) {
-                                       if (visited.add(tmpnode)) {
-                                               toprocess.push(tmpnode);
-                                       }
-                               } else {
-                                       set->add(tmpnode);
-                               }
-                       }
-                       delete iterator;
-               }
-       } else
-               set->add(node);
+void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
+       DOREdge edge(first, second, 0, first, second);
+       if (!edges.contains(&edge)) {
+               DOREdge *newedge=new DOREdge(first, second, 0, first, second);
+               edges.add(newedge);
+       }
+}
+
+void DecomposeOrderResolver::remapEdge(uint64_t first, uint64_t second, uint64_t newfirst, uint64_t newsecond) {
+       DOREdge edge(first, second, 0, first, second);
+       DOREdge *oldedge=edges.get(&edge);
+       if (oldedge != NULL) {
+               edges.remove(oldedge);
+               oldedge->newfirst=newfirst;
+               oldedge->newsecond=newsecond;
+               edges.add(oldedge);
+       } else {
+               DOREdge *newedge=new DOREdge(first, second, 0, newfirst, newsecond);
+               edges.add(newedge);
+       }
+}
+
+void DecomposeOrderResolver::setEdgeOrder(uint64_t first, uint64_t second, uint sccNum) {
+       DOREdge edge(first, second, 0, first, second);
+       DOREdge *oldedge=edges.get(&edge);
+       if (oldedge != NULL) {
+               oldedge->orderindex=sccNum;
+       } else {
+               DOREdge *newedge=new DOREdge(first, second, sccNum, first, second);
+               edges.add(newedge);
+       }
+}
+
+void DecomposeOrderResolver::setOrder(uint sccNum, Order *neworder) {
+       orders.setExpand(sccNum, neworder);
+}
+
+Order * DecomposeOrderResolver::getOrder(uint sccNum) {
+       Order *neworder = NULL;
+       if (orders.getSize() > sccNum)
+               neworder = orders.get(sccNum);
+       return neworder;
 }
 
 bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
 }
 
 bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
@@ -52,8 +75,8 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
        ASSERT(to != NULL);
        if (from->removed || to->removed) {
                HashsetOrderNode fromset, toset;
        ASSERT(to != NULL);
        if (from->removed || to->removed) {
                HashsetOrderNode fromset, toset;
-               processNode(&fromset, from, true);
-               processNode(&toset, to, false);
+               //              processNode(&fromset, from, true);
+               //              processNode(&toset, to, false);
                SetIteratorOrderNode *fromit=fromset.iterator();
                while(fromit->hasNext()) {
                        OrderNode * nodefrom=fromit->next();
                SetIteratorOrderNode *fromit=fromset.iterator();
                while(fromit->hasNext()) {
                        OrderNode * nodefrom=fromit->next();
index 1f3b266f1474c8639178413f51bd451a03bd505b..5948e14b9b26d12f87a35ac2455b13ac2a0c2536 100644 (file)
 #include "structs.h"
 #include "orderresolver.h"
 
 #include "structs.h"
 #include "orderresolver.h"
 
+class DOREdge {
+ public:
+ DOREdge(uint64_t _origfirst, uint64_t _origsecond, uint _orderindex, uint64_t _newfirst, uint64_t _newsecond) :
+         origfirst(_origfirst),
+               origsecond(_origsecond),
+               orderindex(_orderindex),
+               newfirst(_newfirst),
+               newsecond(_newsecond) {
+       }               
+       uint64_t origfirst;
+       uint64_t origsecond;
+       uint orderindex;
+       uint64_t newfirst;
+       uint64_t newsecond;
+       CMEMALLOC;
+};
+
 class DecomposeOrderResolver : public OrderResolver {
 public:
 class DecomposeOrderResolver : public OrderResolver {
 public:
-       DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
-       bool resolveOrder(uint64_t first, uint64_t second);
-       bool resolvePartialOrder(OrderNode *first, OrderNode *second);
+       DecomposeOrderResolver(Order *_order);
+       virtual bool resolveOrder(uint64_t first, uint64_t second);
        virtual ~DecomposeOrderResolver();
        virtual ~DecomposeOrderResolver();
-private:
+       void mustOrderEdge(uint64_t first, uint64_t second);
+       void remapEdge(uint64_t oldfirst, uint64_t oldsecond, uint64_t newfirst, uint64_t newsecond);
+       void setEdgeOrder(uint64_t first, uint64_t second, uint sccNum);
+       void setOrder(uint sccNum, Order *order);
+       Order * getOrder(uint sccNum);
+       CMEMALLOC;
+       
+ private:
+       bool resolvePartialOrder(OrderNode *first, OrderNode *second);
        OrderGraph *graph;
        OrderGraph *graph;
+       Order *order;
        Vector<Order *> orders;
        Vector<Order *> orders;
+       HashsetDOREdge edges;
 };
 
 #endif/* DECOMPOSEORDERRESOLVER_H */
 };
 
 #endif/* DECOMPOSEORDERRESOLVER_H */
index 69c710ef3f927232ac5275f5ffaede8a07d151be..bb102ad8c4c6eaca9b07a65571836fb4c828b950 100644 (file)
@@ -53,6 +53,7 @@ class OrderEncoding;
 class OrderGraph;
 class OrderNode;
 class OrderEdge;
 class OrderGraph;
 class OrderNode;
 class OrderEdge;
+class DOREdge;
 
 class AutoTuner;
 class SearchTuner;
 
 class AutoTuner;
 class SearchTuner;