removing true nodes from the OrderGraph

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 99f826baeb59ab33132caa707a8aa6914b9d7fa8..32bd91092f16699200675b02911399527a2e6524 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -82,8 +82,58 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
        deleteVectorArrayOrderNode(&finishNodes);
 }
 
-void removeMustBeTrueNodes(OrderGraph *graph) {
-       //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
+bool isMustBeTrueNode(OrderNode* node){
+       HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges);
+       while(hasNextOrderEdge(iterator)){
+               OrderEdge* edge = nextOrderEdge(iterator);
+               if(!edge->mustPos)
+                       return false;
+       }
+       deleteIterOrderEdge(iterator);
+       iterator = iteratorOrderEdge(node->outEdges);
+       while(hasNextOrderEdge(iterator)){
+               OrderEdge* edge = nextOrderEdge(iterator);
+               if(!edge->mustPos)
+                       return false;
+       }
+       deleteIterOrderEdge(iterator);
+       return true;
+}
+
+void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
+       HSIteratorOrderEdge* iterin = iteratorOrderEdge(node->inEdges);
+       while(hasNextOrderEdge(iterin)){
+               OrderEdge* inEdge = nextOrderEdge(iterin);
+               OrderNode* srcNode = inEdge->source;
+               removeHashSetOrderEdge(srcNode->outEdges, inEdge);
+               HSIteratorOrderEdge* iterout = iteratorOrderEdge(node->outEdges);
+               while(hasNextOrderEdge(iterout)){
+                       OrderEdge* outEdge = nextOrderEdge(iterout);
+                       OrderNode* sinkNode = outEdge->sink;
+                       removeHashSetOrderEdge(sinkNode->inEdges, outEdge);
+                       //Adding new edge to new sink and src nodes ...
+                       OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
+                       newEdge->mustPos = true;
+                       newEdge->polPos = true;
+                       if (newEdge->mustNeg)
+                               This->unsat = true;
+                       addHashSetOrderEdge(srcNode->outEdges, newEdge);
+                       addHashSetOrderEdge(sinkNode->inEdges, newEdge);
+               }
+               deleteIterOrderEdge(iterout);
+       }
+       deleteIterOrderEdge(iterin);
+}
+
+void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
+       HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
+       while(hasNextOrderNode(iterator)){
+               OrderNode* node = nextOrderNode(iterator);
+               if(isMustBeTrueNode(node)){
+                       bypassMustBeTrueNode(This,graph, node);
+               }
+       }
+       deleteIterOrderNode(iterator);
 }
 
 /** This function computes a source set for every nodes, the set of
@@ -430,7 +480,7 @@ void orderAnalysis(CSolver *This) {
                bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
                
                if (mustReachPrune)
-                       removeMustBeTrueNodes(graph);
+                       removeMustBeTrueNodes(This, graph);
                
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index 99c3938af6ca30dcda4fa9b9963cec93f85f3468..f9b4d5f2edb0fe2fdefcf35ee8b92be437a0edc6 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -19,7 +19,9 @@ void DFS(OrderGraph *graph, VectorOrderNode *finishNodes);
 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes);
 void completePartialOrderGraph(OrderGraph *graph);
 void resetNodeInfoStatusSCC(OrderGraph *graph);
-void removeMustBeTrueNodes(OrderGraph *graph);
+bool isMustBeTrueNode(OrderNode* node);
+void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node);
+void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
 void completePartialOrderGraph(OrderGraph *graph);
 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes);
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure);