#include "ordergraph.h"
#include "order.h"
#include "ordernode.h"
+#include "rewriter.h"
-
-NodeInfo* allocNodeInfo() {
- NodeInfo* This = (NodeInfo*) ourmalloc(sizeof(NodeInfo));
- This->status = NOTVISITED;
- return This;
-}
-
-void deleteNodeInfo(NodeInfo* info) {
- ourfree(info);
-}
-
-OrderGraph* buildOrderGraph(Order *order) {
- OrderGraph* orderGraph = allocOrderGraph(order);
- uint constrSize = getSizeVectorBoolean(&order->constraints);
- for(uint j=0; j<constrSize; j++){
- addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
+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;
}
-void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
- HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
- while(hasNextOrderNode(iterator)){
- OrderNode* node = nextOrderNode(iterator);
- NodeInfo* info= getNodeInfo(nodeToInfo, node);
- if(info->status == NOTVISITED){
- info->status = VISITED;
- DFSNodeVisit(node, finishNodes, nodeToInfo, false);
- info->status = FINISHED;
+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 DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
+void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
uint size = getSizeVectorOrderNode(finishNodes);
- for(int i=size-1; i>=0; i--){
- OrderNode* node = getVectorOrderNode(finishNodes, i);
- NodeInfo* info= getNodeInfo(nodeToInfo, node);
- if(info->status == NOTVISITED){
- info->status = VISITED;
- DFSNodeVisit(node, NULL, nodeToInfo, true);
- info->status = FINISHED;
- pushVectorOrderNode(&graph->scc, node);
+ 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++;
}
}
}
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo, bool isReverse) {
- 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
+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;
-
- NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
- if(childInfo->status == NOTVISITED){
- childInfo->status = VISITED;
- DFSNodeVisit(child, finishNodes, nodeToInfo, isReverse);
- childInfo->status = FINISHED;
- if(!isReverse)
- pushVectorOrderNode(finishNodes, child);
+
+ OrderNode *child = isReverse ? edge->source : edge->sink;
+
+ if (child->status == NOTVISITED) {
+ child->status = VISITED;
+ DFSNodeVisit(child, finishNodes, isReverse, sccNum);
+ child->status = FINISHED;
+ if (!isReverse)
+ pushVectorOrderNode(finishNodes, child);
+ else
+ child->sccNum = sccNum;
}
}
deleteIterOrderEdge(iterator);
}
-void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
- HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
- while(hasNextOrderNode(iterator)){
- putNodeInfo(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
+void resetNodeInfoStatusSCC(OrderGraph *graph) {
+ HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
+ while (hasNextOrderNode(iterator)) {
+ nextOrderNode(iterator)->status = NOTVISITED;
}
deleteIterOrderNode(iterator);
}
-void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
- HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
- while(hasNextOrderNode(iterator)){
- NodeInfo* info= getNodeInfo(nodeToInfo, nextOrderNode(iterator));
- info->status = NOTVISITED;
- }
- deleteIterOrderNode(iterator);
-}
-
-void computeStronglyConnectedComponentGraph(OrderGraph* graph) {
+void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
VectorOrderNode finishNodes;
- initDefVectorOrderNode(& finishNodes);
- HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- initializeNodeInfoSCC(graph, nodeToInfo);
- DFS(graph, &finishNodes, nodeToInfo);
- resetNodeInfoStatusSCC(graph, nodeToInfo);
- DFSReverse(graph, &finishNodes, nodeToInfo);
- deleteHashTableNodeInfo(nodeToInfo);
+ initDefVectorOrderNode(&finishNodes);
+ DFS(graph, &finishNodes);
+ resetNodeInfoStatusSCC(graph);
+ DFSReverse(graph, &finishNodes);
+ resetNodeInfoStatusSCC(graph);
deleteVectorArrayOrderNode(&finishNodes);
}
-void removeMustBeTrueNodes(OrderGraph* graph) {
+void removeMustBeTrueNodes(OrderGraph *graph) {
//TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
}
-void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode* node, HashTableNodeInfo* nodeToInfo) {
- HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges);
- while(hasNextOrderEdge(iterator)){
- OrderEdge* inEdge = nextOrderEdge(iterator);
+void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node) {
+ HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
+ while (hasNextOrderEdge(iterator)) {
+ OrderEdge *inEdge = nextOrderEdge(iterator);
if (inEdge->polNeg) {
- OrderNode* src = inEdge->source;
- NodeInfo* srcInfo = getNodeInfo(nodeToInfo, src);
- if (srcInfo->status==VISITED) {
+ OrderNode *src = inEdge->source;
+ if (src->status == VISITED) {
//Make a pseudoEdge to point backwards
- OrderEdge * newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
+ OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
newedge->pseudoPos = true;
}
}
}
deleteIterOrderEdge(iterator);
iterator = iteratorOrderEdge(node->outEdges);
- while(hasNextOrderEdge(iterator)){
- OrderEdge* edge = nextOrderEdge(iterator);
- if (!edge->polPos) //Ignore edges that do not have positive polarity
+ while (hasNextOrderEdge(iterator)) {
+ OrderEdge *edge = nextOrderEdge(iterator);
+ if (!edge->polPos)//Ignore edges that do not have positive polarity
continue;
-
- OrderNode* child = edge->sink;
- NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
- if(childInfo->status == NOTVISITED){
- childInfo->status = VISITED;
- DFSPseudoNodeVisit(graph, child, nodeToInfo);
- childInfo->status = FINISHED;
+
+ OrderNode *child = edge->sink;
+ if (child->status == NOTVISITED) {
+ child->status = VISITED;
+ DFSPseudoNodeVisit(graph, child);
+ child->status = FINISHED;
}
}
deleteIterOrderEdge(iterator);
}
-void completePartialOrderGraph(OrderGraph* graph) {
+void completePartialOrderGraph(OrderGraph *graph) {
VectorOrderNode finishNodes;
- initDefVectorOrderNode(& finishNodes);
- HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- initializeNodeInfoSCC(graph, nodeToInfo);
- DFS(graph, &finishNodes, nodeToInfo);
- resetNodeInfoStatusSCC(graph, nodeToInfo);
+ initDefVectorOrderNode(&finishNodes);
+ DFS(graph, &finishNodes);
+ resetNodeInfoStatusSCC(graph);
uint size = getSizeVectorOrderNode(&finishNodes);
- for(int i=size-1; i>=0; i--){
- OrderNode* node = getVectorOrderNode(&finishNodes, i);
- NodeInfo* info= getNodeInfo(nodeToInfo, node);
- if(info->status == NOTVISITED){
- info->status = VISITED;
- DFSPseudoNodeVisit(graph, node, nodeToInfo);
- info->status = FINISHED;
+ for (int i = size - 1; i >= 0; i--) {
+ OrderNode *node = getVectorOrderNode(&finishNodes, i);
+ if (node->status == NOTVISITED) {
+ node->status = VISITED;
+ DFSPseudoNodeVisit(graph, node);
+ node->status = FINISHED;
}
}
-
- deleteHashTableNodeInfo(nodeToInfo);
+
+ resetNodeInfoStatusSCC(graph);
deleteVectorArrayOrderNode(&finishNodes);
}
-void DFSMust(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
- HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
- while(hasNextOrderNode(iterator)){
- OrderNode* node = nextOrderNode(iterator);
- NodeInfo* info= getNodeInfo(nodeToInfo, node);
- if(info->status == NOTVISITED){
- info->status = VISITED;
- DFSMustNodeVisit(node, finishNodes, nodeToInfo, false);
- info->status = FINISHED;
+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, false);
+ node->status = FINISHED;
pushVectorOrderNode(finishNodes, node);
}
}
deleteIterOrderNode(iterator);
}
-void DFSMustNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
- HashTableNodeInfo* nodeToInfo, bool clearBackEdges) {
- HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->outEdges);
- while(hasNextOrderEdge(iterator)){
- OrderEdge* edge = nextOrderEdge(iterator);
- OrderNode* child = edge->sink;
- NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
-
- if (clearBackEdges && childInfo->status==VISITED) {
+void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges) {
+ //First compute implication of transitive closure on must pos edges
+ HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
+ while (hasNextOrderEdge(iterator)) {
+ OrderEdge *edge = nextOrderEdge(iterator);
+ OrderNode *parent = edge->source;
+ if (parent->status == VISITED) {
+ edge->mustPos = true;
+ }
+ }
+ deleteIterOrderEdge(iterator);
+
+ //Next compute implication of transitive closure on must neg edges
+ iterator = iteratorOrderEdge(node->outEdges);
+ while (hasNextOrderEdge(iterator)) {
+ OrderEdge *edge = nextOrderEdge(iterator);
+ OrderNode *child = edge->sink;
+
+ if (clearBackEdges && child->status == VISITED) {
//We have a backedge, so note that this edge must be negative
edge->mustNeg = true;
}
- if (!edge->mustPos) //Ignore edges that are not must Positive edges
+ if (!edge->mustPos) //Ignore edges that are not must Positive edges
continue;
- if(childInfo->status == NOTVISITED){
- childInfo->status = VISITED;
- DFSMustNodeVisit(child, finishNodes, nodeToInfo, clearBackEdges);
- childInfo->status = FINISHED;
- pushVectorOrderNode(finishNodes, child);
+ if (child->status == NOTVISITED) {
+ child->status = VISITED;
+ DFSMustNodeVisit(child, finishNodes, clearBackEdges);
+ child->status = FINISHED;
+ pushVectorOrderNode(finishNodes, child);
}
}
deleteIterOrderEdge(iterator);
}
-void DFSClearContradictions(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
- uint size=getSizeVectorOrderNode(finishNodes);
- for(int i=size-1; i>=0; i--){
- OrderNode* node=getVectorOrderNode(finishNodes, i);
- NodeInfo* info=getNodeInfo(nodeToInfo, node);
- if(info->status == NOTVISITED){
- info->status = VISITED;
- DFSMustNodeVisit(node, NULL, nodeToInfo, true);
- info->status = FINISHED;
+void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes) {
+ uint size = getSizeVectorOrderNode(finishNodes);
+ for (int i = size - 1; i >= 0; i--) {
+ OrderNode *node = getVectorOrderNode(finishNodes, i);
+ if (node->status == NOTVISITED) {
+ node->status = VISITED;
+ DFSMustNodeVisit(node, NULL, true);
+ node->status = FINISHED;
}
}
}
/* This function finds edges that would form a cycle with must edges
- and forces them to be mustNeg. */
+ 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(OrderGraph *graph) {
- HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
VectorOrderNode finishNodes;
- initDefVectorOrderNode(& finishNodes);
+ initDefVectorOrderNode(&finishNodes);
//Topologically sort the mustPos edge graph
- DFSMust(graph, &finishNodes, nodeToInfo);
- resetNodeInfoStatusSCC(graph, nodeToInfo);
+ DFSMust(graph, &finishNodes);
+ resetNodeInfoStatusSCC(graph);
//Find any backwards edges that complete cycles and force them to be mustNeg
- DFSClearContradictions(graph, &finishNodes, nodeToInfo);
+ DFSClearContradictions(graph, &finishNodes);
deleteVectorArrayOrderNode(&finishNodes);
- deleteHashTableNodeInfo(nodeToInfo);
+ resetNodeInfoStatusSCC(graph);
}
/* 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). */
+ inverse edge to be negative (and clears its positive polarity if it
+ had one). */
void localMustAnalysisTotal(OrderGraph *graph) {
- HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
- while(hasNextOrderEdge(iterator)) {
+ HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
+ while (hasNextOrderEdge(iterator)) {
OrderEdge *edge = nextOrderEdge(iterator);
- if (edge -> mustPos) {
- OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
- if (invEdge!= NULL && !invEdge -> mustPos && invEdge->polPos) {
+ if (edge->mustPos) {
+ OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+ if (invEdge != NULL && !invEdge->mustPos && invEdge->polPos) {
invEdge->polPos = false;
}
invEdge->mustNeg = true;
}
/** 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. */
+ 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(OrderGraph *graph) {
- HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
- while(hasNextOrderEdge(iterator)) {
+ HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
+ while (hasNextOrderEdge(iterator)) {
OrderEdge *edge = nextOrderEdge(iterator);
- if (edge -> mustPos) {
+ if (edge->mustPos) {
if (edge->polNeg && !edge->mustNeg) {
edge->polNeg = false;
}
- OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
- if (invEdge != NULL && !invEdge -> mustPos) {
+ OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+ if (invEdge != NULL && !invEdge->mustPos) {
invEdge->polPos = false;
}
invEdge->mustNeg = true;
deleteIterOrderEdge(iterator);
}
-void orderAnalysis(CSolver* This) {
+void decomposeOrder(Order *order, OrderGraph *graph) {
+ 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);
+ OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ if (from->sccNum < to->sccNum) {
+ //replace with true
+ replaceBooleanWithTrue((Boolean *)orderconstraint);
+ } else if (to->sccNum < from->sccNum) {
+ //replace with false
+ replaceBooleanWithFalse((Boolean *)orderconstraint);
+ } else {
+ //Build new order and change constraint's order
+
+ }
+ }
+}
+
+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) {
+ 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
//This analysis is completely optional
reachMustAnalysis(graph);
-
+
//This pair of analysis is also optional
- if (order->type==PARTIAL) {
+ if (order->type == PARTIAL) {
localMustAnalysisPartial(graph);
} else {
localMustAnalysisTotal(graph);
}
- //This analysis is completely optional
+ //This optimization is completely optional
removeMustBeTrueNodes(graph);
-
+ //This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
+
+ decomposeOrder(order, graph);
+
deleteOrderGraph(graph);
}
}
projects / satune.git / blobdiff