X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FEncoders%2Forderencoder.c;h=103b96204bbabefabcf6a4dda160fd5711ca93ca;hb=4221735881b9d1cd53ef410d9448efd2d12a51ad;hp=b1179a6a315a73ef79ca0261d9d66fcb5a7c4687;hpb=21f25f4b21aff9453953d590eff032464f5e8e9b;p=satune.git diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c index b1179a6..103b962 100644 --- a/src/Encoders/orderencoder.c +++ b/src/Encoders/orderencoder.c @@ -5,247 +5,231 @@ #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; jconstraints, 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; @@ -255,20 +239,20 @@ void localMustAnalysisTotal(OrderGraph *graph) { } /** 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; @@ -280,12 +264,32 @@ void localMustAnalysisPartial(OrderGraph *graph) { 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; iallOrders, 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 @@ -294,19 +298,22 @@ void orderAnalysis(CSolver* This) { //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); } }