From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 1 Sep 2017 22:21:04 +0000 (-0700)
Subject: Editing orderresolver design
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=a768839ef081984f67aa88ffca7b8532c9d91084

Editing orderresolver design
---

diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 49d8855..6115295 100644
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -12,7 +12,7 @@
 #include "ordergraph.h"
 
 DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph* _graph, Vector<Order*>& _orders):
-	OrderResolver(_graph),
+	graph(_graph),
 	orders(_orders.getSize(), _orders.expose())
 {
 }
@@ -21,12 +21,36 @@ DecomposeOrderResolver::~DecomposeOrderResolver() {
 	delete graph;
 }
 
-HappenedBefore DecomposeOrderResolver::getOrder(OrderNode* from, OrderNode* to){
-	ASSERT(from->id == to->id);
-	// We should ask this query from the suborder ....
-	Order *suborder = NULL;
-	suborder = orders.get(from->sccNum);
-	ASSERT(suborder != NULL);
-	return suborder->encoding.resolver->resolveOrder(from->id, to->id);
+HappenedBefore DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second){
+	OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
+	if(from == NULL){
+		return SATC_UNORDERED;
+	}
+	OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
+	if(from == NULL){
+		return SATC_UNORDERED;
+	}
+	if (from->sccNum != to->sccNum) {
+		OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
+		if (edge != NULL && edge->mustPos){
+			return SATC_FIRST;
+		} else if( edge != NULL && edge->mustNeg){
+			return SATC_SECOND;
+		}else {
+			switch(graph->getOrder()->encoding.type){
+				case SATC_TOTAL:
+					return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND;
+				case SATC_PARTIAL:
+				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);
+	}
 }
 
diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
index 6a7d735..590c565 100644
--- a/src/Translator/decomposeorderresolver.h
+++ b/src/Translator/decomposeorderresolver.h
@@ -16,12 +16,11 @@
 class DecomposeOrderResolver : public OrderResolver{
 public:
 	DecomposeOrderResolver(OrderGraph* graph, Vector<Order *> & orders);
+	HappenedBefore resolveOrder(uint64_t first, uint64_t second);
 	virtual ~DecomposeOrderResolver();
 private:
 	OrderGraph* graph;
 	Vector<Order*> orders;
-	
-	HappenedBefore getOrder(OrderNode* from, OrderNode* to);
 };
 
 #endif /* DECOMPOSEORDERRESOLVER_H */
diff --git a/src/Translator/orderresolver.cc b/src/Translator/orderresolver.cc
deleted file mode 100644
index 5ed3a5e..0000000
--- a/src/Translator/orderresolver.cc
+++ /dev/null
@@ -1,39 +0,0 @@
-#include "orderresolver.h"
-#include "ordergraph.h"
-#include "ordernode.h"
-#include "orderedge.h"
-
-OrderResolver::OrderResolver(OrderGraph* _graph)
-	:graph(_graph)
-{
-}
-
-OrderResolver::~OrderResolver(){
-	delete graph;
-}
-
-HappenedBefore OrderResolver::resolveOrder(uint64_t first, uint64_t second){
-	OrderNode *from = graph->getOrderNodeFromOrderGraph(first, false /*Don't create new node if doesn't exist*/);
-	if(from == NULL){
-		return SATC_UNORDERED;
-	}
-	OrderNode *to = graph->getOrderNodeFromOrderGraph(second, false);
-	if(from == NULL){
-		return SATC_UNORDERED;
-	}
-	if (from->sccNum != to->sccNum) {
-		OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to, false /* Don't create a new edge*/);
-		if (edge != NULL && edge->mustPos){
-			return SATC_FIRST;
-		} else if( edge != NULL && edge->mustNeg){
-			return SATC_SECOND;
-		}else {
-			ASSERT(0);
-			//It's a case that either there's no edge, or there is an edge
-			// but we don't know the value! (This case shouldn't happen)
-			//return from->sccNum < to->sccNum? SATC_FIRST: SATC_SECOND;
-		}
-	} else {
-		return getOrder(from, to);
-	}
-}
\ No newline at end of file
diff --git a/src/Translator/orderresolver.h b/src/Translator/orderresolver.h
index 9f248af..35498ff 100644
--- a/src/Translator/orderresolver.h
+++ b/src/Translator/orderresolver.h
@@ -14,13 +14,10 @@
 
 class OrderResolver {
 public:
-	OrderResolver(OrderGraph* _graph);
-	HappenedBefore resolveOrder(uint64_t first, uint64_t second);
-	virtual ~OrderResolver();
+	OrderResolver(){};
+	virtual HappenedBefore resolveOrder(uint64_t first, uint64_t second) = 0;
+	virtual ~OrderResolver(){};
 	CMEMALLOC;
-protected:
-	OrderGraph* graph;
-	virtual HappenedBefore getOrder(OrderNode* from, OrderNode* to) = 0;
 };
 
 #endif /* ORDERRESOLVER_H */