From: bdemsky <bdemsky@uci.edu>
Date: Sat, 21 Oct 2017 23:19:28 +0000 (-0700)
Subject: New Resolver Strategy
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=5c85052f51461617085157442e8ca37db875e803

New Resolver Strategy
---

diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index a2e52f8..d518b1b 100644
--- 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 7460b20..fc82966 100644
--- 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 d4a2d5f..01a667d 100644
--- 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 f0d3e2a..0e652d8 100644
--- 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 5948e14..a6bf955 100644
--- 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;