--- /dev/null
+#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;i<pcvsize;i++) {
+ Order * neworder=getVectorOrder(&partialcandidatevec, i);
+ if (neworder != NULL){
+ neworder->type = 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);
+ }
+}
--- /dev/null
+/*
+ * 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 */
+
+++ /dev/null
-#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;i<pcvsize;i++) {
- Order * neworder=getVectorOrder(&partialcandidatevec, i);
- if (neworder != NULL){
- neworder->type = 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);
- }
-}
+++ /dev/null
-/*
- * 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 */
-
projects / satune.git / commitdiff