X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FASTTransform%2Fdecomposeordertransform.cc;h=62b08284cbcd446fccb6677e01b49d26b53d563b;hb=73239bf3a5168ce4562a191c823b5a5e6c8ebd5b;hp=4c95db88c3196cf0db0559422affd7d01fd26c07;hpb=45bda60d0c548e27157100efb7855f45a5104606;p=satune.git

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 4c95db8..62b0828 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -16,6 +16,7 @@
 #include "decomposeorderresolver.h"
 #include "tunable.h"
 #include "orderanalysis.h"
+#include "polarityassignment.h"
 
 
 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
@@ -36,9 +37,9 @@ void DecomposeOrderTransform::doTransform() {
 			continue;
 		}
 
-		DecomposeOrderResolver *dor=new DecomposeOrderResolver(order);
+		DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
 		order->setOrderResolver(dor);
-		
+
 		OrderGraph *graph = buildOrderGraph(order);
 		if (order->type == SATC_PARTIAL) {
 			//Required to do SCC analysis for partial order graphs.  It
@@ -62,18 +63,20 @@ void DecomposeOrderTransform::doTransform() {
 		}
 
 		bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-		HashsetOrderEdge *edgesRemoved = NULL;
 
 		if (mustReachPrune) {
-			edgesRemoved = new HashsetOrderEdge();
-			removeMustBeTrueNodes(graph, edgesRemoved);
+			removeMustBeTrueNodes(graph, dor);
+		}
+
+		bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
+
+		if (pruneEdges) {
+			mustEdgePrune(graph, dor);
 		}
 
 		//This is needed for splitorder
 		graph->computeStronglyConnectedComponentGraph();
-		decomposeOrder(order, graph, edgesRemoved, dor);
-		if (edgesRemoved != NULL)
-			delete edgesRemoved;
+		decomposeOrder(order, graph, dor);
 		delete graph;
 	}
 	delete orderit;
@@ -81,7 +84,7 @@ void DecomposeOrderTransform::doTransform() {
 }
 
 
-void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
 	Vector<Order *> partialcandidatevec;
 	uint size = currOrder->constraints.getSize();
 	for (uint i = 0; i < size; i++) {
@@ -90,17 +93,8 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
 		OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
 		OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
 		OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
-		if (edgesRemoved != NULL) {
-			if (edgesRemoved->contains(edge)) {
-				dor->mustOrderEdge(from->getID(), to->getID());
-				solver->replaceBooleanWithTrue(orderconstraint);
-				continue;
-			} else if (edgesRemoved->contains(invedge)) {
-				dor->mustOrderEdge(to->getID(), from->getID());
-				solver->replaceBooleanWithFalse(orderconstraint);
-				continue;
-			}
-		}
+		if (from->removed || to->removed)
+			continue;
 
 		if (from->sccNum != to->sccNum) {
 			if (edge != NULL) {
@@ -108,7 +102,7 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
 					dor->mustOrderEdge(from->getID(), to->getID());
 					solver->replaceBooleanWithTrue(orderconstraint);
 				} else if (edge->polNeg) {
-					if (currOrder->type == SATC_TOTAL)					
+					if (currOrder->type == SATC_TOTAL)
 						dor->mustOrderEdge(to->getID(), from->getID());
 					solver->replaceBooleanWithFalse(orderconstraint);
 				} else {
@@ -158,9 +152,10 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG
 				if (edge->polNeg)
 					partialcandidatevec.setExpand(from->sccNum, NULL);
 			}
-			orderconstraint->order = neworder;
+			BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
+			solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
+			updateEdgePolarity(neworderconstraint, orderconstraint);
 			dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
-			neworder->addOrderConstraint(orderconstraint);
 		}
 	}
 	solver->getActiveOrders()->remove(currOrder);
@@ -195,24 +190,21 @@ bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
 	return true;
 }
 
-void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 	node->removed = true;
 	SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 	while (iterin->hasNext()) {
 		OrderEdge *inEdge = iterin->next();
 		OrderNode *srcNode = inEdge->source;
 		srcNode->outEdges.remove(inEdge);
-		edgesRemoved->add(inEdge);
-		bool removeOutgoingEdges = !iterin->hasNext();
+		dor->mustOrderEdge(srcNode->getID(), node->getID());
+		BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
+		solver->replaceBooleanWithTrue(be);
 
 		SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 		while (iterout->hasNext()) {
 			OrderEdge *outEdge = iterout->next();
 			OrderNode *sinkNode = outEdge->sink;
-			if (removeOutgoingEdges) {
-				sinkNode->inEdges.remove(outEdge);
-				edgesRemoved->add(outEdge);
-			}
 			//Adding new edge to new sink and src nodes ...
 			if (srcNode == sinkNode) {
 				solver->setUnSAT();
@@ -222,6 +214,7 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
 			}
 			//Add new order constraint
 			BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+			updateEdgePolarity(orderconstraint, P_TRUE);
 			solver->addConstraint(orderconstraint);
 
 			//Add new edge
@@ -236,15 +229,141 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
 		delete iterout;
 	}
 	delete iterin;
+
+	//Clean up old edges...  Keep this later in case we don't have any in edges
+	SetIteratorOrderEdge *iterout = node->outEdges.iterator();
+	while (iterout->hasNext()) {
+		OrderEdge *outEdge = iterout->next();
+		OrderNode *sinkNode = outEdge->sink;
+		dor->mustOrderEdge(node->getID(), sinkNode->getID());
+		sinkNode->inEdges.remove(outEdge);
+		BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
+		solver->replaceBooleanWithTrue(be2);
+	}
+	delete iterout;
 }
 
-void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
+void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
 	SetIteratorOrderNode *iterator = graph->getNodes();
 	while (iterator->hasNext()) {
-		OrderNode *node = iterator->next();
+		OrderNode *node = (OrderNode *)iterator->next();
+		if (node->removed)
+			continue;
 		if (isMustBeTrueNode(node)) {
-			bypassMustBeTrueNode(graph, node, edgesRemoved);
+			bypassMustBeTrueNode(graph, node, dor);
 		}
 	}
 	delete iterator;
 }
+
+void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
+	SetIteratorOrderNode *iterator = graph->getNodes();
+	while (iterator->hasNext()) {
+		OrderNode *node = (OrderNode *)iterator->next();
+		if (node->removed)
+			continue;
+		attemptNodeMerge(graph, node, dor);
+	}
+	delete iterator;
+}
+
+void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
+	SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
+	while (edgeit->hasNext()) {
+		OrderEdge *outedge = edgeit->next();
+		//Only eliminate must edges
+		if (!outedge->mustPos)
+			continue;
+		OrderNode *dstnode = outedge->sink;
+		uint numOutEdges = node->outEdges.getSize();
+		uint numInEdges = dstnode->inEdges.getSize();
+		/*
+		   Need to avoid a situation where we create new reachability by
+		   the merge.  This can only happen if there is an extra in edge to
+		   the dstnode and an extra out edge to our node.
+		 */
+
+		if (numOutEdges == 1 || numInEdges == 1) {
+			/* Safe to do the Merge */
+			mergeNodes(graph, node, outedge, dstnode, dor);
+
+			//Throw away the iterator and start over
+			delete edgeit;
+			edgeit = node->outEdges.iterator();
+		}
+	}
+	delete edgeit;
+}
+
+void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
+	/* Fix up must edge between the two nodes */
+	node->outEdges.remove(edge);
+	dstnode->inEdges.remove(edge);
+	dor->mustOrderEdge(node->getID(), dstnode->getID());
+
+	BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
+	solver->replaceBooleanWithTrue(be);
+
+	/* Go through the incoming edges to the new node */
+	SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
+	while (inedgeit->hasNext()) {
+		OrderEdge *inedge = inedgeit->next();
+		OrderNode *source = inedge->source;
+		//remove it from the source node
+		source->outEdges.remove(inedge);
+		//save the remapping that we did
+		dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
+		//create the new edge
+		OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
+		//update the flags
+		newedge->polPos |= inedge->polPos;
+		newedge->polNeg |= inedge->polNeg;
+		newedge->mustPos |= inedge->mustPos;
+		newedge->mustNeg |= inedge->mustNeg;
+		newedge->pseudoPos |= inedge->pseudoPos;
+		//add new edge to both
+		source->outEdges.add(newedge);
+		node->inEdges.add(newedge);
+
+		BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
+		BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
+		updateEdgePolarity(benew, be);
+		solver->replaceBooleanWithBoolean(be, benew);
+	}
+	dstnode->inEdges.reset();
+	delete inedgeit;
+
+	/* Go through the outgoing edges from the new node */
+	SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
+	while (outedgeit->hasNext()) {
+		OrderEdge *outedge = outedgeit->next();
+		OrderNode *sink = outedge->sink;
+		//remove it from the sink node
+		sink->inEdges.remove(outedge);
+		//save the remapping that we did
+		dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
+
+		//create the new edge
+		OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
+		//update the flags
+		newedge->polPos |= outedge->polPos;
+		newedge->polNeg |= outedge->polNeg;
+		newedge->mustPos |= outedge->mustPos;
+		newedge->mustNeg |= outedge->mustNeg;
+		newedge->pseudoPos |= outedge->pseudoPos;
+		//add new edge to both
+		sink->inEdges.add(newedge);
+		node->outEdges.add(newedge);
+
+		BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
+		BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
+		updateEdgePolarity(benew, be);
+		solver->replaceBooleanWithBoolean(be, benew);
+	}
+	dstnode->outEdges.reset();
+	delete outedgeit;
+
+
+	/* Mark destination as removed */
+	dstnode->removed = true;
+}