X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FEncoders%2Forderencoder.c;h=32bd91092f16699200675b02911399527a2e6524;hp=a43d39dfec00b974994d414ffb5650e1d5d1c690;hb=b68780a0eac1a7e8022cf680bceddfc1e66f5d9e;hpb=9cb55c1cf260106cf90f7aa39b08157d113599bd

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index a43d39d..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
@@ -160,6 +210,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
 	}
 
 	resetAndDeleteHashTableNodeToNodeSet(table);
+	deleteHashTableNodeToNodeSet(table);
 	resetNodeInfoStatusSCC(graph);
 	deleteVectorArrayOrderNode(&sccNodes);
 	deleteVectorArrayOrderNode(&finishNodes);
@@ -250,6 +301,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode
 	}
 
 	resetAndDeleteHashTableNodeToNodeSet(table);
+	deleteHashTableNodeToNodeSet(table);
 }
 
 /* This function finds edges that would form a cycle with must edges
@@ -335,6 +387,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 		BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 		OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 		OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+		model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
 		if (from->sccNum != to->sccNum) {
 			OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);			
 			if (edge->polPos) {
@@ -381,8 +434,10 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 	uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
 	for(uint i=0;i<pcvsize;i++) {
 		Order * neworder=getVectorOrder(&partialcandidatevec, i);
-		if (neworder != NULL)
+		if (neworder != NULL){
 			neworder->type = TOTAL;
+			model_print("i=%u\t", i);
+		}
 	}
 	
 	deleteVectorArrayOrder(&ordervec);
@@ -425,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);