From a2681aaa0d32ab12f05453b9da273966e8e3cb68 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Sat, 21 Oct 2017 00:16:27 -0700
Subject: [PATCH] Fix bug regarding order translation for removed nodes

---
 src/ASTAnalyses/Encoding/encodinggraph.cc   |  3 -
 src/ASTAnalyses/Order/ordernode.cc          |  1 +
 src/ASTAnalyses/Order/ordernode.h           |  1 +
 src/ASTTransform/decomposeordertransform.cc |  1 +
 src/Translator/decomposeorderresolver.cc    | 68 ++++++++++++++++-----
 5 files changed, 56 insertions(+), 18 deletions(-)

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 9f9bb04..f0cd830 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -81,13 +81,10 @@ void EncodingGraph::encode() {
 						continue;
 					uint encodingSize = subgraph->getEncodingMaxVal(n)+1;
 					uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
-					model_print("encoding size=%u\n", encodingSize);
-					model_print("padded=%u\n", paddedSize);
 					encoding->allocInUseArrayElement(paddedSize);
 					encoding->allocEncodingArrayElement(paddedSize);
 					Set *s = e->getRange();
 					for (uint i = 0; i < s->getSize(); i++) {
-						model_print("index=%u\n", i);
 						uint64_t value = s->getElement(i);
 						uint encodingIndex = subgraph->getEncoding(n, value);
 						encoding->setInUseElement(encodingIndex);
diff --git a/src/ASTAnalyses/Order/ordernode.cc b/src/ASTAnalyses/Order/ordernode.cc
index 02f3146..41b11a5 100644
--- a/src/ASTAnalyses/Order/ordernode.cc
+++ b/src/ASTAnalyses/Order/ordernode.cc
@@ -4,6 +4,7 @@
 OrderNode::OrderNode(uint64_t _id) :
 	id(_id),
 	status(NOTVISITED),
+	removed(false),
 	sccNum(0),
 	inEdges(),
 	outEdges() {
diff --git a/src/ASTAnalyses/Order/ordernode.h b/src/ASTAnalyses/Order/ordernode.h
index 0ae8867..a9bc1d3 100644
--- a/src/ASTAnalyses/Order/ordernode.h
+++ b/src/ASTAnalyses/Order/ordernode.h
@@ -26,6 +26,7 @@ public:
 
 	uint64_t id;
 	NodeStatus status;
+	bool removed;
 	uint sccNum;
 	HashsetOrderEdge inEdges;
 	HashsetOrderEdge outEdges;
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index fd5fda8..51d6a51 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -191,6 +191,7 @@ bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
 }
 
 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+	node->removed = true;
 	SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 	while (iterin->hasNext()) {
 		OrderEdge *inEdge = iterin->next();
diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 64ebc34..1e5fdf0 100644
--- 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;
-- 
2.34.1