New Resolver Strategy

diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index a2e52f807d2db417b436eb9a1d728daf9d96f3f5..d518b1ba12cb9d1c183091d0432d49a4f67d1005 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -71,6 +71,16 @@ void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *
        }
 }
 
+void OrderGraph::addEdge(uint64_t first, uint64_t second) {
+       OrderNode *node1 = getOrderNodeFromOrderGraph(first);
+       OrderNode *node2 = getOrderNodeFromOrderGraph(second);
+       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
+       _1to2->polPos = true;
+       _1to2->mustPos = true;
+       node1->addNewOutgoingEdge(_1to2);
+       node2->addNewIncomingEdge(_1to2);
+}
+
 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
        BooleanValue mustval = constr->boolVal;
        switch (mustval) {

diff --git a/src/ASTAnalyses/Order/ordergraph.h b/src/ASTAnalyses/Order/ordergraph.h
index 7460b20ebaf15070275635ffb220a16a6a91d3de..fc829668787cd5e94a89f05bf9b79cc8484eb281 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.h
+++ b/src/ASTAnalyses/Order/ordergraph.h
@@ -23,6 +23,7 @@ public:
        OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
        void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
        void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+       void addEdge(uint64_t first, uint64_t second);
        OrderEdge *getInverseOrderEdge(OrderEdge *edge);
        Order *getOrder() {return order;}
        bool isTherePath(OrderNode *source, OrderNode *destination);

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index d4a2d5faf9a6d3836b398a5d8f4ae750f0895cbf..01a667d9eb0c32c83432e9eae083c4a275911698 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -48,12 +48,10 @@ void DecomposeOrderTransform::doTransform() {
                }
 
                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) {
@@ -76,6 +74,7 @@ void DecomposeOrderTransform::doTransform() {
                decomposeOrder(order, graph, edgesRemoved, dor);
                if (edgesRemoved != NULL)
                        delete edgesRemoved;
+               delete graph;
        }
        delete orderit;
        delete orders;

diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index f0d3e2aa738812e6af2c24ef0c32edbeda41d750..0e652d8d6e813169979e2a10fdb7a6479e754f7e 100644 (file)
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -20,7 +20,6 @@ DecomposeOrderResolver::DecomposeOrderResolver(Order * _order) :
 DecomposeOrderResolver::~DecomposeOrderResolver() {
        if (graph != NULL)
                delete graph;
-       uint size=edges.getSize();
        edges.resetAndDelete();
 }
 
@@ -68,47 +67,41 @@ Order * DecomposeOrderResolver::getOrder(uint sccNum) {
        return neworder;
 }
 
+void DecomposeOrderResolver::buildGraph() {
+       graph = new OrderGraph(order);
+       SetIteratorDOREdge *iterator = edges.iterator();
+       while(iterator->hasNext()) {
+               DOREdge * doredge = iterator->next();
+               if (doredge->orderindex == 0) {
+                       graph->addEdge(doredge->origfirst, doredge->origsecond);
+               } else {
+                       Order * suborder = orders.get(doredge->orderindex);
+                       bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
+                       if (isEdge)
+                               graph->addEdge(doredge->origfirst, doredge->origsecond);
+               }
+       }
+       delete iterator;
+       if (order->type == SATC_TOTAL) {
+               graph->computeStronglyConnectedComponentGraph();
+       }
+}
+
 bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
+       if (graph == NULL)
+               buildGraph();
+
        OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
        ASSERT(from != NULL);
        OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
        ASSERT(to != NULL);
-       if (from->removed || to->removed) {
-               HashsetOrderNode fromset, toset;
-               //              processNode(&fromset, from, true);
-               //              processNode(&toset, to, false);
-               SetIteratorOrderNode *fromit=fromset.iterator();
-               while(fromit->hasNext()) {
-                       OrderNode * nodefrom=fromit->next();
-                       SetIteratorOrderNode *toit=toset.iterator();
-                       while(toit->hasNext()) {
-                               OrderNode * nodeto=toit->next();
-                               if (resolveOrder(nodefrom->getID(), nodeto->getID())) {
-                                       delete fromit;
-                                       delete toit;
-                                       return true;
-                               }
-                       }
-                       delete toit;
-               }
-               delete fromit;
-               return false;
-       } else if (from->sccNum != to->sccNum) {
-               OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-               switch (graph->getOrder()->type) {
-               case SATC_TOTAL:
-                       return from->sccNum < to->sccNum;
-               case SATC_PARTIAL:
-                       return resolvePartialOrder(from, to);
-               default:
-                       ASSERT(0);
-               }
-       } else {
-               Order *suborder = NULL;
-               // We should ask this query from the suborder ....
-               suborder = orders.get(from->sccNum);
-               ASSERT(suborder != NULL);
-               return suborder->encoding.resolver->resolveOrder(from->id, to->id);
+       switch (order->type) {
+       case SATC_TOTAL:
+               return from->sccNum < to->sccNum;
+       case SATC_PARTIAL:
+               return resolvePartialOrder(from, to);
+       default:
+               ASSERT(0);
        }
 }
 
@@ -118,6 +111,5 @@ bool DecomposeOrderResolver::resolvePartialOrder(OrderNode *first, OrderNode *se
        } else {
                return graph->isTherePath(first, second);
        }
-
 }
 

diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
index 5948e14b9b26d12f87a35ac2455b13ac2a0c2536..a6bf955d8c64a5635651c565fb9b604775183f42 100644 (file)
--- a/src/Translator/decomposeorderresolver.h
+++ b/src/Translator/decomposeorderresolver.h
@@ -44,6 +44,7 @@ public:
        
  private:
        bool resolvePartialOrder(OrderNode *first, OrderNode *second);
+       void buildGraph();
        OrderGraph *graph;
        Order *order;
        Vector<Order *> orders;