From: bdemsky <bdemsky@uci.edu>
Date: Wed, 23 Aug 2017 05:26:44 +0000 (-0700)
Subject: Get rid of redundant code
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=0f51635cad60cb49bd00dbc3966b6ba6bb540869

Get rid of redundant code
---

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index e172d18..066695c 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -15,7 +15,7 @@ void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
 		OrderNode *node = nextOrderNode(iterator);
 		if (node->status == NOTVISITED) {
 			node->status = VISITED;
-			DFSNodeVisit(node, finishNodes, false, 0);
+			DFSNodeVisit(node, finishNodes, false, false, 0);
 			node->status = FINISHED;
 			pushVectorOrderNode(finishNodes, node);
 		}
@@ -30,7 +30,7 @@ void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
 		OrderNode *node = getVectorOrderNode(finishNodes, i);
 		if (node->status == NOTVISITED) {
 			node->status = VISITED;
-			DFSNodeVisit(node, NULL, true, sccNum);
+			DFSNodeVisit(node, NULL, true, false, sccNum);
 			node->sccNum = sccNum;
 			node->status = FINISHED;
 			sccNum++;
@@ -38,18 +38,22 @@ void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
 	}
 }
 
-void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum) {
+void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
 	HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
 	while (hasNextOrderEdge(iterator)) {
 		OrderEdge *edge = nextOrderEdge(iterator);
-		if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
-			continue;
+		if (mustvisit) {
+			if (!edge->mustPos)
+				continue;
+		} else
+			if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
+				continue;
 
 		OrderNode *child = isReverse ? edge->source : edge->sink;
 
 		if (child->status == NOTVISITED) {
 			child->status = VISITED;
-			DFSNodeVisit(child, finishNodes, isReverse, sccNum);
+			DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
 			child->status = FINISHED;
 			if (finishNodes != NULL)
 				pushVectorOrderNode(finishNodes, child);
@@ -107,7 +111,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
 		if (node->status == NOTVISITED) {
 			//Need to do reverse traversal here...
 			node->status = VISITED;
-			DFSNodeVisit(node, &sccNodes, true, sccNum);
+			DFSNodeVisit(node, &sccNodes, true, false, sccNum);
 			node->status = FINISHED;
 			node->sccNum = sccNum;
 			sccNum++;
@@ -167,7 +171,7 @@ void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 		OrderNode *node = nextOrderNode(iterator);
 		if (node->status == NOTVISITED) {
 			node->status = VISITED;
-			DFSMustNodeVisit(node, finishNodes);
+			DFSNodeVisit(node, finishNodes, false, true, 0);
 			node->status = FINISHED;
 			pushVectorOrderNode(finishNodes, node);
 		}
@@ -175,26 +179,6 @@ void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 	deleteIterOrderNode(iterator);
 }
 
-void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
-	HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
-	while (hasNextOrderEdge(iterator)) {
-		OrderEdge *edge = nextOrderEdge(iterator);
-		OrderNode *child = edge->sink;
-
-		if (!edge->mustPos)	//Ignore edges that are not must Positive edges
-			continue;
-
-		if (child->status == NOTVISITED) {
-			child->status = VISITED;
-			DFSMustNodeVisit(child, finishNodes);
-			child->status = FINISHED;
-			pushVectorOrderNode(finishNodes, child);
-		}
-	}
-	deleteIterOrderEdge(iterator);
-}
-
-
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
 	uint size = getSizeVectorOrderNode(finishNodes);
 	HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index 67a56b9..99c3938 100644
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -14,16 +14,14 @@
 void computeStronglyConnectedComponentGraph(OrderGraph *graph);
 void orderAnalysis(CSolver *solver);
 void initializeNodeInfoSCC(OrderGraph *graph);
-void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum);
+void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes);
 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes);
 void completePartialOrderGraph(OrderGraph *graph);
 void resetNodeInfoStatusSCC(OrderGraph *graph);
 void removeMustBeTrueNodes(OrderGraph *graph);
-void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node);
 void completePartialOrderGraph(OrderGraph *graph);
 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes);
-void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes);
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure);
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);