From: bdemsky <bdemsky@uci.edu>
Date: Wed, 16 Aug 2017 19:14:24 +0000 (-0700)
Subject: Extend Must Analysis
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=82d5bc3b844e4aa6146ff917c61e6c94b454553e;p=satune.git

Extend Must Analysis
---

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index d155921..8f83906 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -154,7 +154,19 @@ void DFSMust(OrderGraph* graph, VectorOrderNode* finishNodes) {
 }
 
 void DFSMustNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool clearBackEdges) {
+	//First compute implication of transitive closure on must pos edges
 	HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->outEdges);
+	while(hasNextOrderEdge(iterator)){
+		OrderEdge* edge = nextOrderEdge(iterator);
+		OrderNode* parent = edge->source;
+		if (parent->status == VISITED) {
+			edge->mustPos = true;
+		}
+	}
+	deleteIterOrderEdge(iterator);
+
+	//Next compute implication of transitive closure on must neg edges
+	iterator = iteratorOrderEdge(node->outEdges);
 	while(hasNextOrderEdge(iterator)){
 		OrderEdge* edge = nextOrderEdge(iterator);
 		OrderNode* child = edge->sink;
@@ -190,7 +202,9 @@ void DFSClearContradictions(OrderGraph* graph, VectorOrderNode* finishNodes) {
 }
 
 /* This function finds edges that would form a cycle with must edges
-	 and forces them to be mustNeg. */
+	 and forces them to be mustNeg.  It also decides whether an edge
+	 must be true because of transitivity from other must be true
+	 edges. */
 
 void reachMustAnalysis(OrderGraph *graph) {
 	VectorOrderNode finishNodes;