1 #include "orderencoder.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
13 HSIteratorOrderNode *iterator = graph->nodes->iterator();
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 HSIteratorOrderEdge *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 HSIteratorOrderNode *iterator = graph->nodes->iterator();
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 HSIteratorOrderEdge* iterator = node->inEdges->iterator();
85 while(iterator->hasNext()){
86 OrderEdge* edge = iterator->next();
91 iterator = node->outEdges->iterator();
92 while(iterator->hasNext()){
93 OrderEdge* edge = iterator->next();
101 void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
102 HSIteratorOrderEdge* iterin = node->inEdges->iterator();
103 while(iterin->hasNext()){
104 OrderEdge* inEdge = iterin->next();
105 OrderNode* srcNode = inEdge->source;
106 srcNode->outEdges->remove(inEdge);
107 HSIteratorOrderEdge* iterout = node->outEdges->iterator();
108 while(iterout->hasNext()){
109 OrderEdge* outEdge = iterout->next();
110 OrderNode* sinkNode = outEdge->sink;
111 sinkNode->inEdges->remove(outEdge);
112 //Adding new edge to new sink and src nodes ...
113 OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
114 newEdge->mustPos = true;
115 newEdge->polPos = true;
116 if (newEdge->mustNeg)
118 srcNode->outEdges->add(newEdge);
119 sinkNode->inEdges->add(newEdge);
126 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
127 HSIteratorOrderNode* iterator = graph->nodes->iterator();
128 while(iterator->hasNext()) {
129 OrderNode* node = iterator->next();
130 if(isMustBeTrueNode(node)){
131 bypassMustBeTrueNode(This,graph, node);
137 /** This function computes a source set for every nodes, the set of
138 nodes that can reach that node via pospolarity edges. It then
139 looks for negative polarity edges from nodes in the the source set
140 to determine whether we need to generate pseudoPos edges. */
142 void completePartialOrderGraph(OrderGraph *graph) {
143 Vector<OrderNode *> finishNodes;
144 DFS(graph, &finishNodes);
145 resetNodeInfoStatusSCC(graph);
146 HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25);
148 Vector<OrderNode *> sccNodes;
150 uint size = finishNodes.getSize();
152 for (int i = size - 1; i >= 0; i--) {
153 OrderNode *node = finishNodes.get(i);
154 HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25);
155 table->put(node, sources);
157 if (node->status == NOTVISITED) {
158 //Need to do reverse traversal here...
159 node->status = VISITED;
160 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
161 node->status = FINISHED;
162 node->sccNum = sccNum;
166 //Compute in set for entire SCC
167 uint rSize = sccNodes.getSize();
168 for (uint j = 0; j < rSize; j++) {
169 OrderNode *rnode = sccNodes.get(j);
170 //Compute source sets
171 HSIteratorOrderEdge *iterator = rnode->inEdges->iterator();
172 while (iterator->hasNext()) {
173 OrderEdge *edge = iterator->next();
174 OrderNode *parent = edge->source;
176 sources->add(parent);
177 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)table->get(parent);
178 sources->addAll(parent_srcs);
183 for (uint j=0; j < rSize; j++) {
184 //Copy in set of entire SCC
185 OrderNode *rnode = sccNodes.get(j);
186 HashSetOrderNode * set = (j==0) ? sources : sources->copy();
187 table->put(rnode, set);
189 //Use source sets to compute pseudoPos edges
190 HSIteratorOrderEdge *iterator = node->inEdges->iterator();
191 while (iterator->hasNext()) {
192 OrderEdge *edge = iterator->next();
193 OrderNode *parent = edge->source;
194 ASSERT(parent != rnode);
195 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
196 sources->contains(parent)) {
197 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
198 newedge->pseudoPos = true;
208 table->resetanddelete();
210 resetNodeInfoStatusSCC(graph);
213 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
214 HSIteratorOrderNode *iterator = graph->nodes->iterator();
215 while (iterator->hasNext()) {
216 OrderNode *node = iterator->next();
217 if (node->status == NOTVISITED) {
218 node->status = VISITED;
219 DFSNodeVisit(node, finishNodes, false, true, 0);
220 node->status = FINISHED;
221 finishNodes->push(node);
227 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
228 uint size = finishNodes->getSize();
229 HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25);
231 for (int i = size - 1; i >= 0; i--) {
232 OrderNode *node = finishNodes->get(i);
233 HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25);
234 table->put(node, sources);
237 //Compute source sets
238 HSIteratorOrderEdge *iterator = node->inEdges->iterator();
239 while (iterator->hasNext()) {
240 OrderEdge *edge = iterator->next();
241 OrderNode *parent = edge->source;
243 sources->add(parent);
244 HashSetOrderNode *parent_srcs = (HashSetOrderNode *) table->get(parent);
245 sources->addAll(parent_srcs);
250 if (computeTransitiveClosure) {
251 //Compute full transitive closure for nodes
252 HSIteratorOrderNode *srciterator = sources->iterator();
253 while (srciterator->hasNext()) {
254 OrderNode *srcnode = srciterator->next();
255 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
256 newedge->mustPos = true;
257 newedge->polPos = true;
258 if (newedge->mustNeg)
259 solver->unsat = true;
260 srcnode->outEdges->add(newedge);
261 node->inEdges->add(newedge);
266 //Use source sets to compute mustPos edges
267 HSIteratorOrderEdge *iterator =node->inEdges->iterator();
268 while (iterator->hasNext()) {
269 OrderEdge *edge = iterator->next();
270 OrderNode *parent = edge->source;
271 if (!edge->mustPos && sources->contains(parent)) {
272 edge->mustPos = true;
275 solver->unsat = true;
281 //Use source sets to compute mustNeg for edges that would introduce cycle if true
282 HSIteratorOrderEdge *iterator = node->outEdges->iterator();
283 while (iterator->hasNext()) {
284 OrderEdge *edge = iterator->next();
285 OrderNode *child = edge->sink;
286 if (!edge->mustNeg && sources->contains(child)) {
287 edge->mustNeg = true;
290 solver->unsat = true;
297 table->resetanddelete();
301 /* This function finds edges that would form a cycle with must edges
302 and forces them to be mustNeg. It also decides whether an edge
303 must be true because of transitivity from other must be true
306 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
307 Vector<OrderNode *> finishNodes;
308 //Topologically sort the mustPos edge graph
309 DFSMust(graph, &finishNodes);
310 resetNodeInfoStatusSCC(graph);
312 //Find any backwards edges that complete cycles and force them to be mustNeg
313 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
316 /* This function finds edges that must be positive and forces the
317 inverse edge to be negative (and clears its positive polarity if it
320 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
321 HSIteratorOrderEdge *iterator = graph->edges->iterator();
322 while (iterator->hasNext()) {
323 OrderEdge *edge = iterator->next();
325 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
326 if (invEdge != NULL) {
327 if (!invEdge->mustPos) {
328 invEdge->polPos = false;
330 solver->unsat = true;
332 invEdge->mustNeg = true;
333 invEdge->polNeg = true;
340 /** This finds edges that must be positive and forces the inverse edge
341 to be negative. It also clears the negative flag of this edge.
342 It also finds edges that must be negative and clears the positive
345 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
346 HSIteratorOrderEdge *iterator = graph->edges->iterator();
347 while (iterator->hasNext()) {
348 OrderEdge *edge = iterator->next();
350 if (!edge->mustNeg) {
351 edge->polNeg = false;
353 solver->unsat = true;
355 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
356 if (invEdge != NULL) {
357 if (!invEdge->mustPos)
358 invEdge->polPos = false;
360 solver->unsat = true;
361 invEdge->mustNeg = true;
362 invEdge->polNeg = true;
365 if (edge->mustNeg && !edge->mustPos) {
366 edge->polPos = false;