From: bdemsky Date: Fri, 25 Aug 2017 02:31:43 +0000 (-0700) Subject: Move X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4fc3453e743c2e647f2e95cad5b09d12bc6a0761;p=satune.git Move --- diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc new file mode 100644 index 0000000..42ac5aa --- /dev/null +++ b/src/ASTAnalyses/orderencoder.cc @@ -0,0 +1,492 @@ +#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" +#include "tunable.h" + +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, false, 0); + node->status = FINISHED; + pushVectorOrderNode(finishNodes, node); + } + } + deleteIterOrderNode(iterator); +} + +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, false, sccNum); + node->sccNum = sccNum; + node->status = FINISHED; + sccNum++; + } + } +} + +void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { + HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges); + while (hasNextOrderEdge(iterator)) { + OrderEdge *edge = nextOrderEdge(iterator); + if (mustvisit) { + if (!edge->mustPos) + continue; + } else + 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, mustvisit, sccNum); + child->status = FINISHED; + if (finishNodes != NULL) + pushVectorOrderNode(finishNodes, child); + if (isReverse) + child->sccNum = sccNum; + } + } + deleteIterOrderEdge(iterator); +} + +void resetNodeInfoStatusSCC(OrderGraph *graph) { + HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); + while (hasNextOrderNode(iterator)) { + nextOrderNode(iterator)->status = NOTVISITED; + } + deleteIterOrderNode(iterator); +} + +void computeStronglyConnectedComponentGraph(OrderGraph *graph) { + VectorOrderNode finishNodes; + initDefVectorOrderNode(&finishNodes); + DFS(graph, &finishNodes); + resetNodeInfoStatusSCC(graph); + DFSReverse(graph, &finishNodes); + resetNodeInfoStatusSCC(graph); + deleteVectorArrayOrderNode(&finishNodes); +} + +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 + 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, false, sccNum); + node->status = FINISHED; + node->sccNum = sccNum; + sccNum++; + pushVectorOrderNode(&sccNodes, node); + + //Compute in set for entire SCC + uint rSize = getSizeVectorOrderNode(&sccNodes); + for (uint 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 (uint 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); + } + } + + resetAndDeleteHashTableNodeToNodeSet(table); + deleteHashTableNodeToNodeSet(table); + resetNodeInfoStatusSCC(graph); + deleteVectorArrayOrderNode(&sccNodes); + deleteVectorArrayOrderNode(&finishNodes); +} + +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; + DFSNodeVisit(node, finishNodes, false, true, 0); + node->status = FINISHED; + pushVectorOrderNode(finishNodes, node); + } + } + deleteIterOrderNode(iterator); +} + +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); + } + } + + resetAndDeleteHashTableNodeToNodeSet(table); + deleteHashTableNodeToNodeSet(table); +} + +/* 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); + //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; + VectorOrder partialcandidatevec; + initDefVectorOrder(&ordervec); + initDefVectorOrder(&partialcandidatevec); + 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 = new Order(order->type, set); + pushVectorOrder(This->allOrders, neworder); + setExpandVectorOrder(&ordervec, from->sccNum, neworder); + if (order->type == PARTIAL) + setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder); + else + setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); + } + 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); + } + if (order->type == PARTIAL) { + OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to); + if (edge->polNeg) + setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); + } + orderconstraint->order = neworder; + neworder->addOrderConstraint(orderconstraint); + } + } + + uint pcvsize=getSizeVectorOrder(&partialcandidatevec); + for(uint i=0;itype = TOTAL; + model_print("i=%u\t", i); + } + } + + deleteVectorArrayOrder(&ordervec); + deleteVectorArrayOrder(&partialcandidatevec); +} + +void orderAnalysis(CSolver *This) { + uint size = getSizeVectorOrder(This->allOrders); + for (uint i = 0; i < size; i++) { + Order *order = getVectorOrder(This->allOrders, i); + bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff); + if (!doDecompose) + continue; + + 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); + } + + + bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff); + + if (mustReachGlobal) + reachMustAnalysis(This, graph, false); + + bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff); + + if (mustReachLocal) { + //This pair of analysis is also optional + if (order->type == PARTIAL) { + localMustAnalysisPartial(This, graph); + } else { + localMustAnalysisTotal(This, graph); + } + } + + bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff); + + if (mustReachPrune) + removeMustBeTrueNodes(This, graph); + + //This is needed for splitorder + computeStronglyConnectedComponentGraph(graph); + + decomposeOrder(This, order, graph); + + deleteOrderGraph(graph); + } +} diff --git a/src/ASTAnalyses/orderencoder.h b/src/ASTAnalyses/orderencoder.h new file mode 100644 index 0000000..f9b4d5f --- /dev/null +++ b/src/ASTAnalyses/orderencoder.h @@ -0,0 +1,35 @@ +/* + * File: orderencoder.h + * Author: hamed + * + * Created on August 8, 2017, 6:36 PM + */ + +#ifndef ORDERGRAPHBUILDER_H +#define ORDERGRAPHBUILDER_H +#include "classlist.h" +#include "structs.h" +#include "mymemory.h" + +void computeStronglyConnectedComponentGraph(OrderGraph *graph); +void orderAnalysis(CSolver *solver); +void initializeNodeInfoSCC(OrderGraph *graph); +void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum); +void DFS(OrderGraph *graph, VectorOrderNode *finishNodes); +void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes); +void completePartialOrderGraph(OrderGraph *graph); +void resetNodeInfoStatusSCC(OrderGraph *graph); +bool isMustBeTrueNode(OrderNode* node); +void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node); +void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph); +void completePartialOrderGraph(OrderGraph *graph); +void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes); +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure); +void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); +void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); +void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph); +void orderAnalysis(CSolver *This); +void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph); + +#endif/* ORDERGRAPHBUILDER_H */ + diff --git a/src/Encoders/orderencoder.cc b/src/Encoders/orderencoder.cc deleted file mode 100644 index 42ac5aa..0000000 --- a/src/Encoders/orderencoder.cc +++ /dev/null @@ -1,492 +0,0 @@ -#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" -#include "tunable.h" - -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, false, 0); - node->status = FINISHED; - pushVectorOrderNode(finishNodes, node); - } - } - deleteIterOrderNode(iterator); -} - -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, false, sccNum); - node->sccNum = sccNum; - node->status = FINISHED; - sccNum++; - } - } -} - -void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { - HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges); - while (hasNextOrderEdge(iterator)) { - OrderEdge *edge = nextOrderEdge(iterator); - if (mustvisit) { - if (!edge->mustPos) - continue; - } else - 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, mustvisit, sccNum); - child->status = FINISHED; - if (finishNodes != NULL) - pushVectorOrderNode(finishNodes, child); - if (isReverse) - child->sccNum = sccNum; - } - } - deleteIterOrderEdge(iterator); -} - -void resetNodeInfoStatusSCC(OrderGraph *graph) { - HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes); - while (hasNextOrderNode(iterator)) { - nextOrderNode(iterator)->status = NOTVISITED; - } - deleteIterOrderNode(iterator); -} - -void computeStronglyConnectedComponentGraph(OrderGraph *graph) { - VectorOrderNode finishNodes; - initDefVectorOrderNode(&finishNodes); - DFS(graph, &finishNodes); - resetNodeInfoStatusSCC(graph); - DFSReverse(graph, &finishNodes); - resetNodeInfoStatusSCC(graph); - deleteVectorArrayOrderNode(&finishNodes); -} - -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 - 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, false, sccNum); - node->status = FINISHED; - node->sccNum = sccNum; - sccNum++; - pushVectorOrderNode(&sccNodes, node); - - //Compute in set for entire SCC - uint rSize = getSizeVectorOrderNode(&sccNodes); - for (uint 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 (uint 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); - } - } - - resetAndDeleteHashTableNodeToNodeSet(table); - deleteHashTableNodeToNodeSet(table); - resetNodeInfoStatusSCC(graph); - deleteVectorArrayOrderNode(&sccNodes); - deleteVectorArrayOrderNode(&finishNodes); -} - -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; - DFSNodeVisit(node, finishNodes, false, true, 0); - node->status = FINISHED; - pushVectorOrderNode(finishNodes, node); - } - } - deleteIterOrderNode(iterator); -} - -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); - } - } - - resetAndDeleteHashTableNodeToNodeSet(table); - deleteHashTableNodeToNodeSet(table); -} - -/* 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); - //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; - VectorOrder partialcandidatevec; - initDefVectorOrder(&ordervec); - initDefVectorOrder(&partialcandidatevec); - 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 = new Order(order->type, set); - pushVectorOrder(This->allOrders, neworder); - setExpandVectorOrder(&ordervec, from->sccNum, neworder); - if (order->type == PARTIAL) - setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder); - else - setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); - } - 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); - } - if (order->type == PARTIAL) { - OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to); - if (edge->polNeg) - setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL); - } - orderconstraint->order = neworder; - neworder->addOrderConstraint(orderconstraint); - } - } - - uint pcvsize=getSizeVectorOrder(&partialcandidatevec); - for(uint i=0;itype = TOTAL; - model_print("i=%u\t", i); - } - } - - deleteVectorArrayOrder(&ordervec); - deleteVectorArrayOrder(&partialcandidatevec); -} - -void orderAnalysis(CSolver *This) { - uint size = getSizeVectorOrder(This->allOrders); - for (uint i = 0; i < size; i++) { - Order *order = getVectorOrder(This->allOrders, i); - bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff); - if (!doDecompose) - continue; - - 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); - } - - - bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff); - - if (mustReachGlobal) - reachMustAnalysis(This, graph, false); - - bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff); - - if (mustReachLocal) { - //This pair of analysis is also optional - if (order->type == PARTIAL) { - localMustAnalysisPartial(This, graph); - } else { - localMustAnalysisTotal(This, graph); - } - } - - bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff); - - if (mustReachPrune) - removeMustBeTrueNodes(This, graph); - - //This is needed for splitorder - computeStronglyConnectedComponentGraph(graph); - - decomposeOrder(This, order, graph); - - deleteOrderGraph(graph); - } -} diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h deleted file mode 100644 index f9b4d5f..0000000 --- a/src/Encoders/orderencoder.h +++ /dev/null @@ -1,35 +0,0 @@ -/* - * File: orderencoder.h - * Author: hamed - * - * Created on August 8, 2017, 6:36 PM - */ - -#ifndef ORDERGRAPHBUILDER_H -#define ORDERGRAPHBUILDER_H -#include "classlist.h" -#include "structs.h" -#include "mymemory.h" - -void computeStronglyConnectedComponentGraph(OrderGraph *graph); -void orderAnalysis(CSolver *solver); -void initializeNodeInfoSCC(OrderGraph *graph); -void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum); -void DFS(OrderGraph *graph, VectorOrderNode *finishNodes); -void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes); -void completePartialOrderGraph(OrderGraph *graph); -void resetNodeInfoStatusSCC(OrderGraph *graph); -bool isMustBeTrueNode(OrderNode* node); -void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node); -void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph); -void completePartialOrderGraph(OrderGraph *graph); -void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes); -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure); -void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); -void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); -void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph); -void orderAnalysis(CSolver *This); -void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph); - -#endif/* ORDERGRAPHBUILDER_H */ -