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 if(srcNode == sinkNode){
123 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
124 newEdge->mustPos = true;
125 newEdge->polPos = true;
126 if (newEdge->mustNeg){
129 srcNode->outEdges.add(newEdge);
130 sinkNode->inEdges.add(newEdge);
137 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
138 SetIteratorOrderNode *iterator = graph->getNodes();
139 while (iterator->hasNext()) {
140 OrderNode *node = iterator->next();
141 if (isMustBeTrueNode(node)) {
142 bypassMustBeTrueNode(This, graph, node);
148 /** This function computes a source set for every nodes, the set of
149 nodes that can reach that node via pospolarity edges. It then
150 looks for negative polarity edges from nodes in the the source set
151 to determine whether we need to generate pseudoPos edges. */
153 void completePartialOrderGraph(OrderGraph *graph) {
154 Vector<OrderNode *> finishNodes;
155 DFS(graph, &finishNodes);
156 resetNodeInfoStatusSCC(graph);
157 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
159 Vector<OrderNode *> sccNodes;
161 uint size = finishNodes.getSize();
163 for (int i = size - 1; i >= 0; i--) {
164 OrderNode *node = finishNodes.get(i);
165 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
166 table->put(node, sources);
168 if (node->status == NOTVISITED) {
169 //Need to do reverse traversal here...
170 node->status = VISITED;
171 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
172 node->status = FINISHED;
173 node->sccNum = sccNum;
177 //Compute in set for entire SCC
178 uint rSize = sccNodes.getSize();
179 for (uint j = 0; j < rSize; j++) {
180 OrderNode *rnode = sccNodes.get(j);
181 //Compute source sets
182 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
183 while (iterator->hasNext()) {
184 OrderEdge *edge = iterator->next();
185 OrderNode *parent = edge->source;
187 sources->add(parent);
188 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
189 sources->addAll(parent_srcs);
194 for (uint j = 0; j < rSize; j++) {
195 //Copy in set of entire SCC
196 OrderNode *rnode = sccNodes.get(j);
197 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
198 table->put(rnode, set);
200 //Use source sets to compute pseudoPos edges
201 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
202 while (iterator->hasNext()) {
203 OrderEdge *edge = iterator->next();
204 OrderNode *parent = edge->source;
205 ASSERT(parent != rnode);
206 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
207 sources->contains(parent)) {
208 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
209 newedge->pseudoPos = true;
219 table->resetanddelete();
221 resetNodeInfoStatusSCC(graph);
224 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
225 SetIteratorOrderNode *iterator = graph->getNodes();
226 while (iterator->hasNext()) {
227 OrderNode *node = iterator->next();
228 if (node->status == NOTVISITED) {
229 node->status = VISITED;
230 DFSNodeVisit(node, finishNodes, false, true, 0);
231 node->status = FINISHED;
232 finishNodes->push(node);
238 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
239 uint size = finishNodes->getSize();
240 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
242 for (int i = size - 1; i >= 0; i--) {
243 OrderNode *node = finishNodes->get(i);
244 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
245 table->put(node, sources);
248 //Compute source sets
249 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
250 while (iterator->hasNext()) {
251 OrderEdge *edge = iterator->next();
252 OrderNode *parent = edge->source;
254 sources->add(parent);
255 HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
256 sources->addAll(parent_srcs);
261 if (computeTransitiveClosure) {
262 //Compute full transitive closure for nodes
263 SetIteratorOrderNode *srciterator = sources->iterator();
264 while (srciterator->hasNext()) {
265 OrderNode *srcnode = srciterator->next();
266 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
267 newedge->mustPos = true;
268 newedge->polPos = true;
269 if (newedge->mustNeg)
271 srcnode->outEdges.add(newedge);
272 node->inEdges.add(newedge);
277 //Use source sets to compute mustPos edges
278 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
279 while (iterator->hasNext()) {
280 OrderEdge *edge = iterator->next();
281 OrderNode *parent = edge->source;
282 if (!edge->mustPos && sources->contains(parent)) {
283 edge->mustPos = true;
292 //Use source sets to compute mustNeg for edges that would introduce cycle if true
293 SetIteratorOrderEdge *iterator = node->outEdges.iterator();
294 while (iterator->hasNext()) {
295 OrderEdge *edge = iterator->next();
296 OrderNode *child = edge->sink;
297 if (!edge->mustNeg && sources->contains(child)) {
298 edge->mustNeg = true;
308 table->resetanddelete();
312 /* This function finds edges that would form a cycle with must edges
313 and forces them to be mustNeg. It also decides whether an edge
314 must be true because of transitivity from other must be true
317 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
318 Vector<OrderNode *> finishNodes;
319 //Topologically sort the mustPos edge graph
320 DFSMust(graph, &finishNodes);
321 resetNodeInfoStatusSCC(graph);
323 //Find any backwards edges that complete cycles and force them to be mustNeg
324 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
327 /* This function finds edges that must be positive and forces the
328 inverse edge to be negative (and clears its positive polarity if it
331 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
332 SetIteratorOrderEdge *iterator = graph->getEdges();
333 while (iterator->hasNext()) {
334 OrderEdge *edge = iterator->next();
336 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
337 if (invEdge != NULL) {
338 if (!invEdge->mustPos) {
339 invEdge->polPos = false;
343 invEdge->mustNeg = true;
344 invEdge->polNeg = true;
351 /** This finds edges that must be positive and forces the inverse edge
352 to be negative. It also clears the negative flag of this edge.
353 It also finds edges that must be negative and clears the positive
356 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
357 SetIteratorOrderEdge *iterator = graph->getEdges();
358 while (iterator->hasNext()) {
359 OrderEdge *edge = iterator->next();
361 if (!edge->mustNeg) {
362 edge->polNeg = false;
366 OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
367 if (invEdge != NULL) {
368 if (!invEdge->mustPos)
369 invEdge->polPos = false;
373 invEdge->mustNeg = true;
374 invEdge->polNeg = true;
377 if (edge->mustNeg && !edge->mustPos) {
378 edge->polPos = false;