3 #include "orderanalysis.h"
7 #include "ordergraph.h"
11 #include "mutableset.h"
14 void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
15 SetIteratorOrderNode *iterator = graph->getNodes();
16 while (iterator->hasNext()) {
17 OrderNode *node = iterator->next();
18 if (node->status == NOTVISITED) {
19 node->status = VISITED;
20 DFSNodeVisit(node, finishNodes, false, false, 0);
21 node->status = FINISHED;
22 finishNodes->push(node);
28 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
29 uint size = finishNodes->getSize();
31 for (int i = size - 1; i >= 0; i--) {
32 OrderNode *node = finishNodes->get(i);
33 if (node->status == NOTVISITED) {
34 node->status = VISITED;
35 DFSNodeVisit(node, NULL, true, false, sccNum);
36 node->sccNum = sccNum;
37 node->status = FINISHED;
43 void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
44 SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
45 while (iterator->hasNext()) {
46 OrderEdge *edge = iterator->next();
51 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
54 OrderNode *child = isReverse ? edge->source : edge->sink;
55 if (child->status == NOTVISITED) {
56 child->status = VISITED;
57 DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
58 child->status = FINISHED;
59 if (finishNodes != NULL) {
60 finishNodes->push(child);
63 child->sccNum = sccNum;
69 void resetNodeInfoStatusSCC(OrderGraph *graph) {
70 SetIteratorOrderNode *iterator = graph->getNodes();
71 while (iterator->hasNext()) {
72 iterator->next()->status = NOTVISITED;
77 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
78 Vector<OrderNode *> finishNodes;
79 DFS(graph, &finishNodes);
80 resetNodeInfoStatusSCC(graph);
81 DFSReverse(graph, &finishNodes);
82 resetNodeInfoStatusSCC(graph);
87 /** This function computes a source set for every nodes, the set of
88 nodes that can reach that node via pospolarity edges. It then
89 looks for negative polarity edges from nodes in the the source set
90 to determine whether we need to generate pseudoPos edges. */
92 void completePartialOrderGraph(OrderGraph *graph) {
93 Vector<OrderNode *> finishNodes;
94 DFS(graph, &finishNodes);
95 resetNodeInfoStatusSCC(graph);
96 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
98 Vector<OrderNode *> sccNodes;
100 uint size = finishNodes.getSize();
102 for (int i = size - 1; i >= 0; i--) {
103 OrderNode *node = finishNodes.get(i);
104 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
105 table->put(node, sources);
107 if (node->status == NOTVISITED) {
108 //Need to do reverse traversal here...
109 node->status = VISITED;
110 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
111 node->status = FINISHED;
112 node->sccNum = sccNum;
116 //Compute in set for entire SCC
117 uint rSize = sccNodes.getSize();
118 for (uint j = 0; j < rSize; j++) {
119 OrderNode *rnode = sccNodes.get(j);
120 //Compute source sets
121 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
122 while (iterator->hasNext()) {
123 OrderEdge *edge = iterator->next();
124 OrderNode *parent = edge->source;
126 sources->add(parent);
127 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
128 sources->addAll(parent_srcs);
133 for (uint j = 0; j < rSize; j++) {
134 //Copy in set of entire SCC
135 OrderNode *rnode = sccNodes.get(j);
136 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
137 table->put(rnode, set);
139 //Use source sets to compute pseudoPos edges
140 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
141 while (iterator->hasNext()) {
142 OrderEdge *edge = iterator->next();
143 OrderNode *parent = edge->source;
144 ASSERT(parent != rnode);
145 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
146 sources->contains(parent)) {
147 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
148 newedge->pseudoPos = true;
158 table->resetanddelete();
160 resetNodeInfoStatusSCC(graph);
163 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
164 SetIteratorOrderNode *iterator = graph->getNodes();
165 while (iterator->hasNext()) {
166 OrderNode *node = iterator->next();
167 if (node->status == NOTVISITED) {
168 node->status = VISITED;
169 DFSNodeVisit(node, finishNodes, false, true, 0);
170 node->status = FINISHED;
171 finishNodes->push(node);
177 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
178 uint size = finishNodes->getSize();
179 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
181 for (int i = size - 1; i >= 0; i--) {
182 OrderNode *node = finishNodes->get(i);
183 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
184 table->put(node, sources);
187 //Compute source sets
188 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
189 while (iterator->hasNext()) {
190 OrderEdge *edge = iterator->next();
191 OrderNode *parent = edge->source;
193 sources->add(parent);
194 HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
195 sources->addAll(parent_srcs);
200 if (computeTransitiveClosure) {
201 //Compute full transitive closure for nodes
202 SetIteratorOrderNode *srciterator = sources->iterator();
203 while (srciterator->hasNext()) {
204 OrderNode *srcnode = srciterator->next();
205 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
206 newedge->mustPos = true;
207 newedge->polPos = true;
208 if (newedge->mustNeg)
210 srcnode->outEdges.add(newedge);
211 node->inEdges.add(newedge);
216 //Use source sets to compute mustPos edges
217 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
218 while (iterator->hasNext()) {
219 OrderEdge *edge = iterator->next();
220 OrderNode *parent = edge->source;
221 if (!edge->mustPos && sources->contains(parent)) {
222 edge->mustPos = true;
231 //Use source sets to compute mustNeg for edges that would introduce cycle if true
232 SetIteratorOrderEdge *iterator = node->outEdges.iterator();
233 while (iterator->hasNext()) {
234 OrderEdge *edge = iterator->next();
235 OrderNode *child = edge->sink;
236 if (!edge->mustNeg && sources->contains(child)) {
237 edge->mustNeg = true;
248 table->resetanddelete();
252 /* This function finds edges that would form a cycle with must edges
253 and forces them to be mustNeg. It also decides whether an edge
254 must be true because of transitivity from other must be true
257 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
258 Vector<OrderNode *> finishNodes;
259 //Topologically sort the mustPos edge graph
260 DFSMust(graph, &finishNodes);
261 resetNodeInfoStatusSCC(graph);
263 //Find any backwards edges that complete cycles and force them to be mustNeg
264 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
267 /* This function finds edges that must be positive and forces the
268 inverse edge to be negative (and clears its positive polarity if it
271 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
272 SetIteratorOrderEdge *iterator = graph->getEdges();
273 while (iterator->hasNext()) {
274 OrderEdge *edge = iterator->next();
276 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
277 if (invEdge != NULL) {
278 if (!invEdge->mustPos) {
279 invEdge->polPos = false;
282 invEdge->mustNeg = true;
283 invEdge->polNeg = true;
290 /** This finds edges that must be positive and forces the inverse edge
291 to be negative. It also clears the negative flag of this edge.
292 It also finds edges that must be negative and clears the positive
295 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
296 SetIteratorOrderEdge *iterator = graph->getEdges();
297 while (iterator->hasNext()) {
298 OrderEdge *edge = iterator->next();
300 if (!edge->mustNeg) {
301 edge->polNeg = false;
305 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
306 if (invEdge != NULL) {
307 if (!invEdge->mustPos)
308 invEdge->polPos = false;
311 invEdge->mustNeg = true;
312 invEdge->polNeg = true;
315 if (edge->mustNeg && !edge->mustPos) {
316 edge->polPos = false;