Extend Must Analysis

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index d15592132c65b3d3d59528b92a3a80f7c9bd003e..8f83906d1d9b70e5701346e52789bb22e1f3e2e8 100644 (file)
--- 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;