Fix bug regarding order translation for removed nodes

[satune.git] / src / Translator / decomposeorderresolver.cc

diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 64ebc3426e925ce2310037d017654e2e9f12f3f1..1e5fdf0cca7dc43cee7fc532e938aaed665e5bae 100644 (file)
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -20,27 +20,65 @@ DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order
 DecomposeOrderResolver::~DecomposeOrderResolver() {
 }
 
+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);
+}
+
 bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
        OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
        ASSERT(from != NULL);
        OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
        ASSERT(to != NULL);
-
-       if (from->sccNum != to->sccNum) {
-               OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-               if (edge != NULL && edge->mustPos) {
-                       return true;
-               } else if ( edge != NULL && edge->mustNeg) {
-                       return false;
-               } else {
-                       switch (graph->getOrder()->type) {
-                       case SATC_TOTAL:
-                               return from->sccNum < to->sccNum;
-                       case SATC_PARTIAL:
-                               return resolvePartialOrder(from, to);
-                       default:
-                               ASSERT(0);
+       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;