From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 24 Aug 2017 21:40:16 +0000 (-0700)
Subject: removing true nodes from the OrderGraph
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=b68780a0eac1a7e8022cf680bceddfc1e66f5d9e;hp=3864e5b351f8262b769f0b2f4034f986871f3d14

removing true nodes from the OrderGraph
---

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 99f826b..32bd910 100644
--- 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 99c3938..f9b4d5f 100644
--- 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);