1 #include "orderanalysis.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
13 SetIteratorOrderNode *iterator = graph->getNodes();
14 while (iterator->hasNext()) {
15 OrderNode *node = iterator->next();
16 if (node->status == NOTVISITED) {
17 node->status = VISITED;
18 DFSNodeVisit(node, finishNodes, false, false, 0);
19 node->status = FINISHED;
20 finishNodes->push(node);
26 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
27 uint size = finishNodes->getSize();
29 for (int i = size - 1; i >= 0; i--) {
30 OrderNode *node = finishNodes->get(i);
31 if (node->status == NOTVISITED) {
32 node->status = VISITED;
33 DFSNodeVisit(node, NULL, true, false, sccNum);
34 node->sccNum = sccNum;
35 node->status = FINISHED;
41 void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
42 SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
43 while (iterator->hasNext()) {
44 OrderEdge *edge = iterator->next();
49 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
52 OrderNode *child = isReverse ? edge->source : edge->sink;
54 if (child->status == NOTVISITED) {
55 child->status = VISITED;
56 DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
57 child->status = FINISHED;
58 if (finishNodes != NULL)
59 finishNodes->push(child);
61 child->sccNum = sccNum;
67 void resetNodeInfoStatusSCC(OrderGraph *graph) {
68 SetIteratorOrderNode *iterator = graph->getNodes();
69 while (iterator->hasNext()) {
70 iterator->next()->status = NOTVISITED;
75 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
76 Vector<OrderNode *> finishNodes;
77 DFS(graph, &finishNodes);
78 resetNodeInfoStatusSCC(graph);
79 DFSReverse(graph, &finishNodes);
80 resetNodeInfoStatusSCC(graph);
83 bool isMustBeTrueNode(OrderNode *node) {
84 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
85 while (iterator->hasNext()) {
86 OrderEdge *edge = iterator->next();
93 iterator = node->outEdges.iterator();
94 while (iterator->hasNext()) {
95 OrderEdge *edge = iterator->next();
105 void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
106 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
107 while (iterin->hasNext()) {
108 OrderEdge *inEdge = iterin->next();
109 OrderNode *srcNode = inEdge->source;
110 srcNode->outEdges.remove(inEdge);
111 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
112 while (iterout->hasNext()) {
113 OrderEdge *outEdge = iterout->next();
114 OrderNode *sinkNode = outEdge->sink;
115 sinkNode->inEdges.remove(outEdge);
116 //Adding new edge to new sink and src nodes ...
117 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
118 newEdge->mustPos = true;
119 newEdge->polPos = true;
120 if (newEdge->mustNeg)
122 srcNode->outEdges.add(newEdge);
123 sinkNode->inEdges.add(newEdge);
130 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
131 SetIteratorOrderNode *iterator = graph->getNodes();
132 while (iterator->hasNext()) {
133 OrderNode *node = iterator->next();
134 if (isMustBeTrueNode(node)) {
135 bypassMustBeTrueNode(This, graph, node);
141 /** This function computes a source set for every nodes, the set of
142 nodes that can reach that node via pospolarity edges. It then
143 looks for negative polarity edges from nodes in the the source set
144 to determine whether we need to generate pseudoPos edges. */
146 void completePartialOrderGraph(OrderGraph *graph) {
147 Vector<OrderNode *> finishNodes;
148 DFS(graph, &finishNodes);
149 resetNodeInfoStatusSCC(graph);
150 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
152 Vector<OrderNode *> sccNodes;
154 uint size = finishNodes.getSize();
156 for (int i = size - 1; i >= 0; i--) {
157 OrderNode *node = finishNodes.get(i);
158 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
159 table->put(node, sources);
161 if (node->status == NOTVISITED) {
162 //Need to do reverse traversal here...
163 node->status = VISITED;
164 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
165 node->status = FINISHED;
166 node->sccNum = sccNum;
170 //Compute in set for entire SCC
171 uint rSize = sccNodes.getSize();
172 for (uint j = 0; j < rSize; j++) {
173 OrderNode *rnode = sccNodes.get(j);
174 //Compute source sets
175 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
176 while (iterator->hasNext()) {
177 OrderEdge *edge = iterator->next();
178 OrderNode *parent = edge->source;
180 sources->add(parent);
181 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
182 sources->addAll(parent_srcs);
187 for (uint j = 0; j < rSize; j++) {
188 //Copy in set of entire SCC
189 OrderNode *rnode = sccNodes.get(j);
190 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
191 table->put(rnode, set);
193 //Use source sets to compute pseudoPos edges
194 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
195 while (iterator->hasNext()) {
196 OrderEdge *edge = iterator->next();
197 OrderNode *parent = edge->source;
198 ASSERT(parent != rnode);
199 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
200 sources->contains(parent)) {
201 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
202 newedge->pseudoPos = true;
212 table->resetanddelete();
214 resetNodeInfoStatusSCC(graph);
217 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
218 SetIteratorOrderNode *iterator = graph->getNodes();
219 while (iterator->hasNext()) {
220 OrderNode *node = iterator->next();
221 if (node->status == NOTVISITED) {
222 node->status = VISITED;
223 DFSNodeVisit(node, finishNodes, false, true, 0);
224 node->status = FINISHED;
225 finishNodes->push(node);
231 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
232 uint size = finishNodes->getSize();
233 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
235 for (int i = size - 1; i >= 0; i--) {
236 OrderNode *node = finishNodes->get(i);
237 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
238 table->put(node, sources);
241 //Compute source sets
242 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
243 while (iterator->hasNext()) {
244 OrderEdge *edge = iterator->next();
245 OrderNode *parent = edge->source;
247 sources->add(parent);
248 HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
249 sources->addAll(parent_srcs);
254 if (computeTransitiveClosure) {
255 //Compute full transitive closure for nodes
256 SetIteratorOrderNode *srciterator = sources->iterator();
257 while (srciterator->hasNext()) {
258 OrderNode *srcnode = srciterator->next();
259 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
260 newedge->mustPos = true;
261 newedge->polPos = true;
262 if (newedge->mustNeg)
264 srcnode->outEdges.add(newedge);
265 node->inEdges.add(newedge);
270 //Use source sets to compute mustPos edges
271 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
272 while (iterator->hasNext()) {
273 OrderEdge *edge = iterator->next();
274 OrderNode *parent = edge->source;
275 if (!edge->mustPos && sources->contains(parent)) {
276 edge->mustPos = true;
285 //Use source sets to compute mustNeg for edges that would introduce cycle if true
286 SetIteratorOrderEdge *iterator = node->outEdges.iterator();
287 while (iterator->hasNext()) {
288 OrderEdge *edge = iterator->next();
289 OrderNode *child = edge->sink;
290 if (!edge->mustNeg && sources->contains(child)) {
291 edge->mustNeg = true;
301 table->resetanddelete();
305 /* This function finds edges that would form a cycle with must edges
306 and forces them to be mustNeg. It also decides whether an edge
307 must be true because of transitivity from other must be true
310 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
311 Vector<OrderNode *> finishNodes;
312 //Topologically sort the mustPos edge graph
313 DFSMust(graph, &finishNodes);
314 resetNodeInfoStatusSCC(graph);
316 //Find any backwards edges that complete cycles and force them to be mustNeg
317 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
320 /* This function finds edges that must be positive and forces the
321 inverse edge to be negative (and clears its positive polarity if it
324 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
325 SetIteratorOrderEdge *iterator = graph->getEdges();
326 while (iterator->hasNext()) {
327 OrderEdge *edge = iterator->next();
329 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
330 if (invEdge != NULL) {
331 if (!invEdge->mustPos) {
332 invEdge->polPos = false;
336 invEdge->mustNeg = true;
337 invEdge->polNeg = true;
344 /** This finds edges that must be positive and forces the inverse edge
345 to be negative. It also clears the negative flag of this edge.
346 It also finds edges that must be negative and clears the positive
349 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
350 SetIteratorOrderEdge *iterator = graph->getEdges();
351 while (iterator->hasNext()) {
352 OrderEdge *edge = iterator->next();
354 if (!edge->mustNeg) {
355 edge->polNeg = false;
359 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
360 if (invEdge != NULL) {
361 if (!invEdge->mustPos)
362 invEdge->polPos = false;
366 invEdge->mustNeg = true;
367 invEdge->polNeg = true;
370 if (edge->mustNeg && !edge->mustPos) {
371 edge->polPos = false;