From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 5 Jan 2018 21:00:12 +0000 (-0800)
Subject: Bug fixes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ec657324a6ce1b4ba9b5c1534472a47b4cff0201;p=satune.git

Bug fixes
---

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index c75fbec..7dad1d7 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -153,7 +153,6 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
 			}
 			BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
 			solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
-
 			dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
 		}
 	}
diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index a9c062f..0dbaf8d 100644
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -25,8 +25,12 @@ DecomposeOrderResolver::~DecomposeOrderResolver() {
 
 void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
 	DOREdge edge(first, second, 0, first, second);
-	if (!edges.contains(&edge)) {
+	DOREdge *oldedge=edges.get(&edge);
+	if (oldedge != NULL) {
+		oldedge->mustbetrue=true;
+	} else {
 		DOREdge *newedge = new DOREdge(first, second, 0, first, second);
+		newedge->mustbetrue=true;
 		edges.add(newedge);
 	}
 }
@@ -54,6 +58,12 @@ void DecomposeOrderResolver::setEdgeOrder(uint64_t first, uint64_t second, uint
 		DOREdge *newedge = new DOREdge(first, second, sccNum, first, second);
 		edges.add(newedge);
 	}
+	/* Also fix up reverse edge if it exists */
+	DOREdge revedge(second, first, 0, second, first);
+	oldedge = edges.get(&revedge);
+	if (oldedge != NULL) {
+		oldedge->orderindex = sccNum;
+	}
 }
 
 void DecomposeOrderResolver::setOrder(uint sccNum, Order *neworder) {
@@ -72,9 +82,12 @@ void DecomposeOrderResolver::buildGraph() {
 	SetIteratorDOREdge *iterator = edges.iterator();
 	while (iterator->hasNext()) {
 		DOREdge *doredge = iterator->next();
-		if (doredge->orderindex == 0) {
+		if (doredge->mustbetrue) {
 			graph->addEdge(doredge->origfirst, doredge->origsecond);
-		} else {
+			if (doredge->newfirst != doredge->origfirst || doredge->newsecond!=doredge->origsecond) {
+				graph->addEdge(doredge->newfirst, doredge->newsecond);
+			}
+		} else if (doredge->orderindex != 0) {
 			Order *suborder = orders.get(doredge->orderindex);
 			bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
 			if (isEdge)
diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
index a260309..5075547 100644
--- a/src/Translator/decomposeorderresolver.h
+++ b/src/Translator/decomposeorderresolver.h
@@ -20,13 +20,15 @@ public:
 		origsecond(_origsecond),
 		orderindex(_orderindex),
 		newfirst(_newfirst),
-		newsecond(_newsecond) {
+		newsecond(_newsecond),
+		mustbetrue(false) {
 	}
 	uint64_t origfirst;
 	uint64_t origsecond;
 	uint orderindex;
 	uint64_t newfirst;
 	uint64_t newsecond;
+	bool mustbetrue;
 	CMEMALLOC;
 };