From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 5 Sep 2017 00:39:34 +0000 (-0700)
Subject: Adding support for partial order in DecomposeOrderResolver
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=f4a7f8b2d0810ddc521dfcf39bb4b2c63f158857

Adding support for partial order in DecomposeOrderResolver
---

diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
index bb241de..2127db9 100644
--- a/src/ASTAnalyses/ordergraph.cc
+++ b/src/ASTAnalyses/ordergraph.cc
@@ -177,3 +177,45 @@ OrderGraph::~OrderGraph() {
 	delete nodes;
 	delete edges;
 }
+
+bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
+	HashsetOrderNode visited;
+	visited.add(source);
+	SetIteratorOrderEdge *iterator = source->outEdges.iterator();
+	bool found = false;
+	while(iterator->hasNext()){
+		OrderNode* node = iterator->next()->sink;
+		if(!visited.contains(node)){
+			if( node == destination ){
+				found = true;
+				break;
+			}
+			visited.add(node);
+			found =isTherePathVisit(visited, node, destination);
+			if(found){
+				break;
+			}
+		}
+	}
+	delete iterator;
+	return found;
+}
+
+bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
+	SetIteratorOrderEdge *iterator = current->outEdges.iterator();
+	bool found = false;
+	while(iterator->hasNext()){
+		OrderNode* node = iterator->next()->sink;
+		if(node == destination){
+			found = true;
+			break;
+		}
+		visited.add(node);
+		if(isTherePathVisit(visited, node, destination)){
+			found = true;
+			break;
+		}
+	}
+	delete iterator;
+	return found;
+}
diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h
index 5f10c1f..a155c7f 100644
--- a/src/ASTAnalyses/ordergraph.h
+++ b/src/ASTAnalyses/ordergraph.h
@@ -24,7 +24,9 @@ public:
 	void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
 	void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
 	OrderEdge *getInverseOrderEdge(OrderEdge *edge);
-	Order *getOrder() {return order;}
+	Order *getOrder() {return order;} 
+	bool isTherePath(OrderNode* source, OrderNode* destination);
+	bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
 	SetIteratorOrderNode *getNodes() {return nodes->iterator();}
 	SetIteratorOrderEdge *getEdges() {return edges->iterator();}
 
diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index f226fda..8a177fa 100644
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -37,7 +37,7 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
 			case SATC_TOTAL:
 				return from->sccNum < to->sccNum;
 			case SATC_PARTIAL:
-			//Adding support for partial order ...
+				return resolvePartialOrder(from, to);
 			default:
 				ASSERT(0);
 			}
@@ -51,3 +51,12 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
 	}
 }
 
+bool DecomposeOrderResolver::resolvePartialOrder(OrderNode* first, OrderNode* second){
+	if(first->sccNum > second->sccNum){
+		return false;
+	} else {
+		return graph->isTherePath(first, second);
+	}
+		
+}
+
diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
index be25a7d..f1d06c6 100644
--- a/src/Translator/decomposeorderresolver.h
+++ b/src/Translator/decomposeorderresolver.h
@@ -17,6 +17,7 @@ class DecomposeOrderResolver : public OrderResolver {
 public:
 	DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
 	bool resolveOrder(uint64_t first, uint64_t second);
+	bool resolvePartialOrder(OrderNode* first, OrderNode* second);
 	virtual ~DecomposeOrderResolver();
 private:
 	OrderGraph *graph;