3 #include "orderanalysis.h"
7 #include "ordergraph.h"
11 #include "mutableset.h"
14 /** Returns a table that maps a node to the set of nodes that can reach the node. */
15 HashtableNodeToNodeSet *getMustReachMap(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
16 uint size = finishNodes->getSize();
17 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
19 for (int i = size - 1; i >= 0; i--) {
20 OrderNode *node = finishNodes->get(i);
21 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
22 table->put(node, sources);
26 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
27 while (iterator->hasNext()) {
28 OrderEdge *edge = iterator->next();
29 OrderNode *parent = edge->source;
32 HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
33 sources->addAll(parent_srcs);
42 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet *table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
43 uint size = finishNodes->getSize();
45 for (int i = size - 1; i >= 0; i--) {
46 OrderNode *node = finishNodes->get(i);
47 HashsetOrderNode *sources = table->get(node);
49 if (computeTransitiveClosure) {
50 //Compute full transitive closure for nodes
51 SetIteratorOrderNode *srciterator = sources->iterator();
52 while (srciterator->hasNext()) {
53 OrderNode *srcnode = (OrderNode *)srciterator->next();
54 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
55 newedge->mustPos = true;
56 newedge->polPos = true;
59 srcnode->outEdges.add(newedge);
60 node->inEdges.add(newedge);
65 //Use source sets to compute mustPos edges
66 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
67 while (iterator->hasNext()) {
68 OrderEdge *edge = iterator->next();
69 OrderNode *parent = edge->source;
70 if (!edge->mustPos && sources->contains(parent)) {
80 //Use source sets to compute mustNeg for edges that would introduce cycle if true
81 SetIteratorOrderEdge *iterator = node->outEdges.iterator();
82 while (iterator->hasNext()) {
83 OrderEdge *edge = iterator->next();
84 OrderNode *child = edge->sink;
85 if (!edge->mustNeg && sources->contains(child)) {
98 /* This function finds edges that would form a cycle with must edges
99 and forces them to be mustNeg. It also decides whether an edge
100 must be true because of transitivity from other must be true
103 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
104 Vector<OrderNode *> finishNodes;
105 //Topologically sort the mustPos edge graph
106 graph->DFSMust(&finishNodes);
107 graph->resetNodeInfoStatusSCC();
108 HashtableNodeToNodeSet *table = getMustReachMap(solver, graph, &finishNodes);
109 //Find any backwards edges that complete cycles and force them to be mustNeg
110 DFSClearContradictions(solver, graph, table, &finishNodes, computeTransitiveClosure);
111 table->resetAndDeleteVals();
115 /* This function finds edges that must be positive and forces the
116 inverse edge to be negative (and clears its positive polarity if it
119 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
120 SetIteratorOrderEdge *iterator = graph->getEdges();
121 while (iterator->hasNext()) {
122 OrderEdge *edge = iterator->next();
124 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
125 if (invEdge != NULL) {
126 if (!invEdge->mustPos) {
127 invEdge->polPos = false;
130 invEdge->mustNeg = true;
131 invEdge->polNeg = true;
138 /** This finds edges that must be positive and forces the inverse edge
139 to be negative. It also clears the negative flag of this edge.
140 It also finds edges that must be negative and clears the positive
143 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
144 SetIteratorOrderEdge *iterator = graph->getEdges();
145 while (iterator->hasNext()) {
146 OrderEdge *edge = iterator->next();
148 if (!edge->mustNeg) {
149 edge->polNeg = false;
153 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
154 if (invEdge != NULL) {
155 if (!invEdge->mustPos)
156 invEdge->polPos = false;
159 invEdge->mustNeg = true;
160 invEdge->polNeg = true;
163 if (edge->mustNeg && !edge->mustPos) {
164 edge->polPos = false;