X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FEncoders%2Forderencoder.c;h=3c840e72db264e87772a6187869c003644ac595a;hp=f9b099d8695a5cfdac0ad692f0a5abb0f13dd930;hb=31a3e00533833ee1c9131a2d0748ca90e3c0d880;hpb=4b73b70e0c569e1ff9592c2c3b717c58356e58e6

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index f9b099d..3c840e7 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -1,93 +1,434 @@
-
 #include "orderencoder.h"
 #include "structs.h"
 #include "csolver.h"
 #include "boolean.h"
 #include "ordergraph.h"
 #include "order.h"
+#include "ordernode.h"
+#include "rewriter.h"
+#include "mutableset.h"
 
+OrderGraph *buildOrderGraph(Order *order) {
+	OrderGraph *orderGraph = allocOrderGraph(order);
+	uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+	for (uint j = 0; j < constrSize; j++) {
+		addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+	}
+	return orderGraph;
+}
 
-NodeInfo* allocNodeInfo(){
-	NodeInfo* This = (NodeInfo*) ourmalloc(sizeof(NodeInfo));
-	This->finishTime = 0;
-	This->status = NOTVISITED;
-	return This;
+void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
+	HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
+	while (hasNextOrderNode(iterator)) {
+		OrderNode *node = nextOrderNode(iterator);
+		if (node->status == NOTVISITED) {
+			node->status = VISITED;
+			DFSNodeVisit(node, finishNodes, false, 0);
+			node->status = FINISHED;
+			pushVectorOrderNode(finishNodes, node);
+		}
+	}
+	deleteIterOrderNode(iterator);
 }
 
-void deleteNodeInfo(NodeInfo* info){
-	ourfree(info);
+void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
+	uint size = getSizeVectorOrderNode(finishNodes);
+	uint sccNum = 1;
+	for (int i = size - 1; i >= 0; i--) {
+		OrderNode *node = getVectorOrderNode(finishNodes, i);
+		if (node->status == NOTVISITED) {
+			node->status = VISITED;
+			DFSNodeVisit(node, NULL, true, sccNum);
+			node->sccNum = sccNum;
+			node->status = FINISHED;
+			sccNum++;
+		}
+	}
 }
 
-OrderEncoder* allocOrderEncoder(){
-	OrderEncoder* This = (OrderEncoder*) ourmalloc(sizeof(OrderEncoder));
-	initDefVectorOrderGraph( &This->graphs );
-	return This;
+void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, 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;
+
+		OrderNode *child = isReverse ? edge->source : edge->sink;
+
+		if (child->status == NOTVISITED) {
+			child->status = VISITED;
+			DFSNodeVisit(child, finishNodes, isReverse, sccNum);
+			child->status = FINISHED;
+			if (finishNodes != NULL)
+				pushVectorOrderNode(finishNodes, child);
+			if (isReverse)
+				child->sccNum = sccNum;
+		}
+	}
+	deleteIterOrderEdge(iterator);
 }
 
-void deleteOrderEncoder(OrderEncoder* This){
-	uint size = getSizeVectorOrderGraph(&This->graphs);
-	for(uint i=0; i<size; i++){
-		deleteOrderGraph(getVectorOrderGraph(&This->graphs, i));
+void resetNodeInfoStatusSCC(OrderGraph *graph) {
+	HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
+	while (hasNextOrderNode(iterator)) {
+		nextOrderNode(iterator)->status = NOTVISITED;
 	}
-	ourfree(This);
+	deleteIterOrderNode(iterator);
 }
 
-OrderEncoder* buildOrderGraphs(CSolver* This){
-	uint size = getSizeVectorOrder(This->allOrders);
-	OrderEncoder* oEncoder = allocOrderEncoder();
-	for(uint i=0; i<size; i++){
-		OrderGraph* orderGraph = allocOrderGraph();
-		Order* order = getVectorOrder(This->allOrders, i);
-		uint constrSize = getSizeVectorBoolean(&order->constraints);
-		for(uint j=0; j<constrSize; j++){
-			addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
-		}
-		pushVectorOrderGraph(&oEncoder->graphs, orderGraph);
+void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
+	VectorOrderNode finishNodes;
+	initDefVectorOrderNode(&finishNodes);
+	DFS(graph, &finishNodes);
+	resetNodeInfoStatusSCC(graph);
+	DFSReverse(graph, &finishNodes);
+	resetNodeInfoStatusSCC(graph);
+	deleteVectorArrayOrderNode(&finishNodes);
+}
+
+void removeMustBeTrueNodes(OrderGraph *graph) {
+	//TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
+}
+
+/** This function computes a source set for every nodes, the set of
+		nodes that can reach that node via pospolarity edges.  It then
+		looks for negative polarity edges from nodes in the the source set
+		to determine whether we need to generate pseudoPos edges. */
+
+void completePartialOrderGraph(OrderGraph *graph) {
+	VectorOrderNode finishNodes;
+	initDefVectorOrderNode(&finishNodes);
+	DFS(graph, &finishNodes);
+	resetNodeInfoStatusSCC(graph);
+	HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
+
+	VectorOrderNode sccNodes;
+	initDefVectorOrderNode(&sccNodes);
+	
+	uint size = getSizeVectorOrderNode(&finishNodes);
+	uint sccNum = 1;
+	for (int i = size - 1; i >= 0; i--) {
+		OrderNode *node = getVectorOrderNode(&finishNodes, i);
+		HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
+		putNodeToNodeSet(table, node, sources);
+		
+		if (node->status == NOTVISITED) {
+			//Need to do reverse traversal here...
+			node->status = VISITED;
+			DFSNodeVisit(node, &sccNodes, true, sccNum);
+			node->status = FINISHED;
+			node->sccNum = sccNum;
+			sccNum++;
+			pushVectorOrderNode(&sccNodes, node);
+
+			//Compute in set for entire SCC
+			uint rSize = getSizeVectorOrderNode(&sccNodes);
+			for (int j = 0; j < rSize; j++) {
+				OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
+				//Compute source sets
+				HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
+				while (hasNextOrderEdge(iterator)) {
+					OrderEdge *edge = nextOrderEdge(iterator);
+					OrderNode *parent = edge->source;
+					if (edge->polPos) {
+						addHashSetOrderNode(sources, parent);
+						HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
+						addAllHashSetOrderNode(sources, parent_srcs);
+					}
+				}
+				deleteIterOrderEdge(iterator);
+			}
+			for (int j=0; j < rSize; j++) {
+				//Copy in set of entire SCC
+				OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
+				HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
+				putNodeToNodeSet(table, rnode, set);
+
+				//Use source sets to compute pseudoPos edges
+				HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
+				while (hasNextOrderEdge(iterator)) {
+					OrderEdge *edge = nextOrderEdge(iterator);
+					OrderNode *parent = edge->source;
+					ASSERT(parent != rnode);
+					if (edge->polNeg && parent->sccNum != rnode->sccNum &&
+							containsHashSetOrderNode(sources, parent)) {
+						OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
+						newedge->pseudoPos = true;
+					}
+				}
+				deleteIterOrderEdge(iterator);
+			}
+			
+			clearVectorOrderNode(&sccNodes);
+		}
 	}
-	return oEncoder;
+
+	resetAndDeleteHashTableNodeToNodeSet(table);
+	resetNodeInfoStatusSCC(graph);
+	deleteVectorArrayOrderNode(&sccNodes);
+	deleteVectorArrayOrderNode(&finishNodes);
 }
 
-void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNode* nodeToInfo, bool isReverse){
-	uint timer=0;
-	HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
-	while(hasNextOrderNode(iterator)){
-		OrderNode* node = nextOrderNode(iterator);
-		NodeInfo* info= getNode(nodeToInfo, node);
-		if(info->status == NOTVISITED){
-			info->status = VISITED;
-			//TODO ...
+void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
+	HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
+	while (hasNextOrderNode(iterator)) {
+		OrderNode *node = nextOrderNode(iterator);
+		if (node->status == NOTVISITED) {
+			node->status = VISITED;
+			DFSMustNodeVisit(node, finishNodes);
+			node->status = FINISHED;
+			pushVectorOrderNode(finishNodes, node);
 		}
 	}
 	deleteIterOrderNode(iterator);
 }
 
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNode* nodeToInfo, uint* timer, bool isReverse){
-	NodeInfo* info= getNode(nodeToInfo, node);
+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 initializeNodeInfoSCC(OrderGraph* graph, HashTableNode* nodeToInfo){
-	HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
-	while(hasNextOrderNode(iterator)){
-		putNode(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
+
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
+	uint size = getSizeVectorOrderNode(finishNodes);
+	HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
+
+	for (int i = size - 1; i >= 0; i--) {
+		OrderNode *node = getVectorOrderNode(finishNodes, i);
+		HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
+		putNodeToNodeSet(table, node, sources);
+
+		{
+			//Compute source sets
+			HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
+			while (hasNextOrderEdge(iterator)) {
+				OrderEdge *edge = nextOrderEdge(iterator);
+				OrderNode *parent = edge->source;
+				if (edge->mustPos) {
+					addHashSetOrderNode(sources, parent);
+					HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
+					addAllHashSetOrderNode(sources, parent_srcs);
+				}
+			}
+			deleteIterOrderEdge(iterator);
+		}
+		if (computeTransitiveClosure) {
+			//Compute full transitive closure for nodes
+			HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
+			while (hasNextOrderNode(srciterator)) {
+				OrderNode *srcnode = nextOrderNode(srciterator);
+				OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
+				newedge->mustPos = true;
+				newedge->polPos = true;
+				if (newedge->mustNeg)
+					solver->unsat = true;
+				addHashSetOrderEdge(srcnode->outEdges,newedge);
+				addHashSetOrderEdge(node->inEdges,newedge);
+			}
+			deleteIterOrderNode(srciterator);
+		}
+		{
+			//Use source sets to compute mustPos edges
+			HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
+			while (hasNextOrderEdge(iterator)) {
+				OrderEdge *edge = nextOrderEdge(iterator);
+				OrderNode *parent = edge->source;
+				if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
+					edge->mustPos = true;
+					edge->polPos = true;
+					if (edge->mustNeg)
+						solver->unsat = true;
+				}
+			}
+			deleteIterOrderEdge(iterator);
+		}
+		{
+			//Use source sets to compute mustNeg for edges that would introduce cycle if true
+			HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
+			while (hasNextOrderEdge(iterator)) {
+				OrderEdge *edge = nextOrderEdge(iterator);
+				OrderNode *child = edge->sink;
+				if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
+					edge->mustNeg = true;
+					edge->polNeg = true;
+					if (edge->mustPos)
+						solver->unsat = true;
+				}
+			}
+			deleteIterOrderEdge(iterator);
+		}
 	}
-	deleteIterOrderNode(iterator);
+
+	resetAndDeleteHashTableNodeToNodeSet(table);
 }
 
-void computeStronglyConnectedComponentGraph(OrderGraph* graph){
+/* This function finds edges that would form a cycle with must edges
+   and forces them to be mustNeg.  It also decides whether an edge
+   must be true because of transitivity from other must be true
+   edges. */
+
+void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
 	VectorOrderNode finishNodes;
-	initDefVectorOrderNode(& finishNodes);
-	HashTableNode* nodeToInfo = allocHashTableNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
-	initializeNodeInfoSCC(graph, nodeToInfo);
-	// TODO
-	deleteHashTableNode(nodeToInfo);
-}
-
-void orderAnalysis(CSolver* solver){
-	OrderEncoder* oEncoder = buildOrderGraphs(solver);
-	uint size = getSizeVectorOrderGraph(&oEncoder->graphs);
-	for(uint i=0; i<size; i++){
-		OrderGraph* graph = getVectorOrderGraph(&oEncoder->graphs, i);
-		computeStronglyConnectedComponentGraph(graph);
+	initDefVectorOrderNode(&finishNodes);
+	//Topologically sort the mustPos edge graph
+	DFSMust(graph, &finishNodes);
+	resetNodeInfoStatusSCC(graph);
+
+	//Find any backwards edges that complete cycles and force them to be mustNeg
+	DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
+	deleteVectorArrayOrderNode(&finishNodes);
+}
+
+/* This function finds edges that must be positive and forces the
+   inverse edge to be negative (and clears its positive polarity if it
+   had one). */
+
+void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
+	HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
+	while (hasNextOrderEdge(iterator)) {
+		OrderEdge *edge = nextOrderEdge(iterator);
+		if (edge->mustPos) {
+			OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+			if (invEdge != NULL) {
+				if (!invEdge->mustPos) {
+					invEdge->polPos = false;
+				} else {
+					solver->unsat = true;
+				}
+				invEdge->mustNeg = true;
+				invEdge->polNeg = true;
+			}
+		}
+	}
+	deleteIterOrderEdge(iterator);
+}
+
+/** This finds edges that must be positive and forces the inverse edge
+    to be negative.  It also clears the negative flag of this edge.
+    It also finds edges that must be negative and clears the positive
+    polarity. */
+
+void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
+	HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
+	while (hasNextOrderEdge(iterator)) {
+		OrderEdge *edge = nextOrderEdge(iterator);
+		if (edge->mustPos) {
+			if (!edge->mustNeg) {
+				edge->polNeg = false;
+			} else
+				solver->unsat = true;
+
+			OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+			if (invEdge != NULL) {
+				if (!invEdge->mustPos)
+					invEdge->polPos = false;
+				else
+					solver->unsat = true;
+				invEdge->mustNeg = true;
+				invEdge->polNeg = true;
+			}
+		}
+		if (edge->mustNeg && !edge->mustPos) {
+			edge->polPos = false;
+		}
 	}
+	deleteIterOrderEdge(iterator);
 }
 
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
+	VectorOrder ordervec;
+	initDefVectorOrder(&ordervec);
+	uint size = getSizeVectorBooleanOrder(&order->constraints);
+	for (uint i = 0; i < size; i++) {
+		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) {
+				replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
+			} else if (edge->polNeg) {
+				replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
+			} else {
+				//This case should only be possible if constraint isn't in AST
+				ASSERT(0);
+			}
+		} else {
+			//Build new order and change constraint's order
+			Order *neworder = NULL;
+			if (getSizeVectorOrder(&ordervec) > from->sccNum)
+				neworder = getVectorOrder(&ordervec, from->sccNum);
+			if (neworder == NULL) {
+				Set *set = (Set *) allocMutableSet(order->set->type);
+				neworder = allocOrder(order->type, set);
+				pushVectorOrder(This->allOrders, neworder);
+				setExpandVectorOrder(&ordervec, from->sccNum, neworder);
+			}
+			if (from->status != ADDEDTOSET) {
+				from->status = ADDEDTOSET;
+				addElementMSet((MutableSet *)neworder->set, from->id);
+			}
+			if (to->status != ADDEDTOSET) {
+				to->status = ADDEDTOSET;
+				addElementMSet((MutableSet *)neworder->set, to->id);
+			}
+			orderconstraint->order = neworder;
+			addOrderConstraint(neworder, orderconstraint);
+		}
+	}
+	for(uint i=0; i<getSizeVectorOrder(&ordervec); i++){
+		Order* order = getVectorOrder(&ordervec, i);
+		if(order!=NULL)
+			model_print("i=%u\t", i);
+	}
+	deleteVectorArrayOrder(&ordervec);
+}
+
+void orderAnalysis(CSolver *This) {
+	uint size = getSizeVectorOrder(This->allOrders);
+	for (uint i = 0; i < size; i++) {
+		Order *order = getVectorOrder(This->allOrders, i);
+		OrderGraph *graph = buildOrderGraph(order);
+		if (order->type == PARTIAL) {
+			//Required to do SCC analysis for partial order graphs.  It
+			//makes sure we don't incorrectly optimize graphs with negative
+			//polarity edges
+			completePartialOrderGraph(graph);
+		}
+
+		//This analysis is completely optional
+		reachMustAnalysis(This, graph, false);
+
+		//This pair of analysis is also optional
+		if (order->type == PARTIAL) {
+			localMustAnalysisPartial(This, graph);
+		} else {
+			localMustAnalysisTotal(This, graph);
+		}
+
+		//This optimization is completely optional
+		removeMustBeTrueNodes(graph);
+
+		//This is needed for splitorder
+		computeStronglyConnectedComponentGraph(graph);
+
+		decomposeOrder(This, order, graph);
+
+		deleteOrderGraph(graph);
+	}
+}