X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FTranslator%2Fdecomposeorderresolver.cc;h=0dbaf8d1881861b03003bde07be16d15963e0834;hb=677be047108738c94bb836f95b9db4d052912c5a;hp=1e5fdf0cca7dc43cee7fc532e938aaed665e5bae;hpb=a2681aaa0d32ab12f05453b9da273966e8e3cb68;p=satune.git

diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 1e5fdf0..0dbaf8d 100644
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -11,81 +11,118 @@
 #include "ordernode.h"
 #include "ordergraph.h"
 
-DecomposeOrderResolver::DecomposeOrderResolver(OrderGraph *_graph, Vector<Order *> &_orders) :
-	graph(_graph),
-	orders(_orders.getSize(), _orders.expose())
+DecomposeOrderResolver::DecomposeOrderResolver(Order *_order) :
+	graph(NULL),
+	order(_order)
 {
 }
 
 DecomposeOrderResolver::~DecomposeOrderResolver() {
+	if (graph != NULL)
+		delete graph;
+	edges.resetAndDelete();
 }
 
-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);
-				}
+void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
+	DOREdge edge(first, second, 0, first, second);
+	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);
+	}
+}
+
+void DecomposeOrderResolver::remapEdge(uint64_t first, uint64_t second, uint64_t newfirst, uint64_t newsecond) {
+	DOREdge edge(first, second, 0, first, second);
+	DOREdge *oldedge = edges.get(&edge);
+	if (oldedge != NULL) {
+		edges.remove(oldedge);
+		oldedge->newfirst = newfirst;
+		oldedge->newsecond = newsecond;
+		edges.add(oldedge);
+	} else {
+		DOREdge *newedge = new DOREdge(first, second, 0, newfirst, newsecond);
+		edges.add(newedge);
+	}
+}
+
+void DecomposeOrderResolver::setEdgeOrder(uint64_t first, uint64_t second, uint sccNum) {
+	DOREdge edge(first, second, 0, first, second);
+	DOREdge *oldedge = edges.get(&edge);
+	if (oldedge != NULL) {
+		oldedge->orderindex = sccNum;
+	} else {
+		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) {
+	orders.setExpand(sccNum, neworder);
+}
+
+Order *DecomposeOrderResolver::getOrder(uint sccNum) {
+	Order *neworder = NULL;
+	if (orders.getSize() > sccNum)
+		neworder = orders.get(sccNum);
+	return neworder;
+}
+
+void DecomposeOrderResolver::buildGraph() {
+	graph = new OrderGraph(order);
+	SetIteratorDOREdge *iterator = edges.iterator();
+	while (iterator->hasNext()) {
+		DOREdge *doredge = iterator->next();
+		if (doredge->mustbetrue) {
+			graph->addEdge(doredge->origfirst, doredge->origsecond);
+			if (doredge->newfirst != doredge->origfirst || doredge->newsecond!=doredge->origsecond) {
+				graph->addEdge(doredge->newfirst, doredge->newsecond);
 			}
-			delete iterator;
+		} else if (doredge->orderindex != 0) {
+			Order *suborder = orders.get(doredge->orderindex);
+			bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
+			if (isEdge)
+				graph->addEdge(doredge->origfirst, doredge->origsecond);
+			else if (order->type == SATC_TOTAL)
+				graph->addEdge(doredge->origsecond, doredge->origfirst);
 		}
-	} else
-		set->add(node);
+	}
+	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);
+	if (from == NULL) {
+		ASSERT(order->type != SATC_TOTAL);
+		return false;
+	}
 	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;
+	if (to == NULL) {
+		ASSERT(order->type != SATC_TOTAL);
 		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);
 	}
 }
 
@@ -95,6 +132,5 @@ bool DecomposeOrderResolver::resolvePartialOrder(OrderNode *first, OrderNode *se
 	} else {
 		return graph->isTherePath(first, second);
 	}
-
 }