Bug Fixes + add more tracing prints + turning off some optimizations
[satune.git] / src / ASTAnalyses / Order / orderanalysis.cc
1 #include <stdint.h>
2
3 #include "orderanalysis.h"
4 #include "structs.h"
5 #include "csolver.h"
6 #include "boolean.h"
7 #include "ordergraph.h"
8 #include "order.h"
9 #include "ordernode.h"
10 #include "rewriter.h"
11 #include "mutableset.h"
12 #include "tunable.h"
13
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);
23                 }
24         }
25         delete iterator;
26 }
27
28 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
29         uint size = finishNodes->getSize();
30         uint sccNum = 1;
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;
38                         sccNum++;
39                 }
40         }
41 }
42
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 #ifdef TRACE_DEBUG
46         model_print("Node:%lu=>", node->id);
47 #endif
48         while (iterator->hasNext()) {
49                 OrderEdge *edge = iterator->next();
50 #ifdef TRACE_DEBUG
51                 model_print("Edge:%lu=>",(uintptr_t) edge);
52 #endif
53                 if (mustvisit) {
54                         if (!edge->mustPos)
55                                 continue;
56                 } else
57                 if (!edge->polPos && !edge->pseudoPos)  //Ignore edges that do not have positive polarity
58                         continue;
59
60                 OrderNode *child = isReverse ? edge->source : edge->sink;
61 #ifdef TRACE_DEBUG
62                 model_println("NodeChild:%lu", child->id);
63 #endif
64                 if (child->status == NOTVISITED) {
65                         child->status = VISITED;
66                         DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
67                         child->status = FINISHED;
68                         if (finishNodes != NULL)
69                                 finishNodes->push(child);
70                         if (isReverse)
71                                 child->sccNum = sccNum;
72                 }
73         }
74         delete iterator;
75 }
76
77 void resetNodeInfoStatusSCC(OrderGraph *graph) {
78         SetIteratorOrderNode *iterator = graph->getNodes();
79         while (iterator->hasNext()) {
80                 iterator->next()->status = NOTVISITED;
81         }
82         delete iterator;
83 }
84
85 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
86         Vector<OrderNode *> finishNodes;
87         DFS(graph, &finishNodes);
88         resetNodeInfoStatusSCC(graph);
89         DFSReverse(graph, &finishNodes);
90         resetNodeInfoStatusSCC(graph);
91 }
92
93 bool isMustBeTrueNode(OrderNode *node) {
94         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
95         while (iterator->hasNext()) {
96                 OrderEdge *edge = iterator->next();
97                 if (!edge->mustPos) {
98                         delete iterator;
99                         return false;
100                 }
101         }
102         delete iterator;
103         iterator = node->outEdges.iterator();
104         while (iterator->hasNext()) {
105                 OrderEdge *edge = iterator->next();
106                 if (!edge->mustPos) {
107                         delete iterator;
108                         return false;
109                 }
110         }
111         delete iterator;
112         return true;
113 }
114
115 void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
116         SetIteratorOrderEdge *iterin = node->inEdges.iterator();
117         while (iterin->hasNext()) {
118                 OrderEdge *inEdge = iterin->next();
119                 OrderNode *srcNode = inEdge->source;
120                 srcNode->outEdges.remove(inEdge);
121                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
122                 while (iterout->hasNext()) {
123                         OrderEdge *outEdge = iterout->next();
124                         OrderNode *sinkNode = outEdge->sink;
125                         sinkNode->inEdges.remove(outEdge);
126                         //Adding new edge to new sink and src nodes ...
127                         if(srcNode == sinkNode){
128 #ifdef TRACE_DEBUG
129                                 model_println("bypassMustBe 1");
130 #endif
131                                 This->setUnSAT();
132                                 delete iterout;
133                                 delete iterin;
134                                 return;
135                         }
136                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
137                         newEdge->mustPos = true;
138                         newEdge->polPos = true;
139                         if (newEdge->mustNeg){
140 #ifdef TRACE_DEBUG
141                                 model_println("BypassMustBe 2");
142 #endif
143                                 This->setUnSAT();
144                         }
145                         srcNode->outEdges.add(newEdge);
146                         sinkNode->inEdges.add(newEdge);
147                 }
148                 delete iterout;
149         }
150         delete iterin;
151 }
152
153 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
154         SetIteratorOrderNode *iterator = graph->getNodes();
155         while (iterator->hasNext()) {
156                 OrderNode *node = iterator->next();
157                 if (isMustBeTrueNode(node)) {
158                         bypassMustBeTrueNode(This, graph, node);
159                 }
160         }
161         delete iterator;
162 }
163
164 /** This function computes a source set for every nodes, the set of
165     nodes that can reach that node via pospolarity edges.  It then
166     looks for negative polarity edges from nodes in the the source set
167     to determine whether we need to generate pseudoPos edges. */
168
169 void completePartialOrderGraph(OrderGraph *graph) {
170         Vector<OrderNode *> finishNodes;
171         DFS(graph, &finishNodes);
172         resetNodeInfoStatusSCC(graph);
173         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
174
175         Vector<OrderNode *> sccNodes;
176
177         uint size = finishNodes.getSize();
178         uint sccNum = 1;
179         for (int i = size - 1; i >= 0; i--) {
180                 OrderNode *node = finishNodes.get(i);
181                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
182                 table->put(node, sources);
183
184                 if (node->status == NOTVISITED) {
185                         //Need to do reverse traversal here...
186                         node->status = VISITED;
187                         DFSNodeVisit(node, &sccNodes, true, false, sccNum);
188                         node->status = FINISHED;
189                         node->sccNum = sccNum;
190                         sccNum++;
191                         sccNodes.push(node);
192
193                         //Compute in set for entire SCC
194                         uint rSize = sccNodes.getSize();
195                         for (uint j = 0; j < rSize; j++) {
196                                 OrderNode *rnode = sccNodes.get(j);
197                                 //Compute source sets
198                                 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
199                                 while (iterator->hasNext()) {
200                                         OrderEdge *edge = iterator->next();
201                                         OrderNode *parent = edge->source;
202                                         if (edge->polPos) {
203                                                 sources->add(parent);
204                                                 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
205                                                 sources->addAll(parent_srcs);
206                                         }
207                                 }
208                                 delete iterator;
209                         }
210                         for (uint j = 0; j < rSize; j++) {
211                                 //Copy in set of entire SCC
212                                 OrderNode *rnode = sccNodes.get(j);
213                                 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
214                                 table->put(rnode, set);
215
216                                 //Use source sets to compute pseudoPos edges
217                                 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
218                                 while (iterator->hasNext()) {
219                                         OrderEdge *edge = iterator->next();
220                                         OrderNode *parent = edge->source;
221                                         ASSERT(parent != rnode);
222                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
223                                                         sources->contains(parent)) {
224                                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
225                                                 newedge->pseudoPos = true;
226                                         }
227                                 }
228                                 delete iterator;
229                         }
230
231                         sccNodes.clear();
232                 }
233         }
234
235         table->resetanddelete();
236         delete table;
237         resetNodeInfoStatusSCC(graph);
238 }
239
240 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
241         SetIteratorOrderNode *iterator = graph->getNodes();
242         while (iterator->hasNext()) {
243                 OrderNode *node = iterator->next();
244                 if (node->status == NOTVISITED) {
245                         node->status = VISITED;
246                         DFSNodeVisit(node, finishNodes, false, true, 0);
247                         node->status = FINISHED;
248                         finishNodes->push(node);
249                 }
250         }
251         delete iterator;
252 }
253
254 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
255         uint size = finishNodes->getSize();
256         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
257
258         for (int i = size - 1; i >= 0; i--) {
259                 OrderNode *node = finishNodes->get(i);
260                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
261                 table->put(node, sources);
262
263                 {
264                         //Compute source sets
265                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
266                         while (iterator->hasNext()) {
267                                 OrderEdge *edge = iterator->next();
268                                 OrderNode *parent = edge->source;
269                                 if (edge->mustPos) {
270                                         sources->add(parent);
271                                         HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
272                                         sources->addAll(parent_srcs);
273                                 }
274                         }
275                         delete iterator;
276                 }
277                 if (computeTransitiveClosure) {
278                         //Compute full transitive closure for nodes
279                         SetIteratorOrderNode *srciterator = sources->iterator();
280                         while (srciterator->hasNext()) {
281                                 OrderNode *srcnode = srciterator->next();
282                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
283                                 newedge->mustPos = true;
284                                 newedge->polPos = true;
285                                 if (newedge->mustNeg){
286 #ifdef TRACE_DEBUG
287                                         model_println("DFS clear 1");
288 #endif
289                                         solver->setUnSAT();
290                                 }
291                                 srcnode->outEdges.add(newedge);
292                                 node->inEdges.add(newedge);
293                         }
294                         delete srciterator;
295                 }
296                 {
297                         //Use source sets to compute mustPos edges
298                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
299                         while (iterator->hasNext()) {
300                                 OrderEdge *edge = iterator->next();
301                                 OrderNode *parent = edge->source;
302                                 if (!edge->mustPos && sources->contains(parent)) {
303                                         edge->mustPos = true;
304                                         edge->polPos = true;
305                                         if (edge->mustNeg){
306 #ifdef TRACE_DEBUG
307                                                 model_println("DFS clear 2");
308 #endif
309                                                 solver->setUnSAT();
310                                         }
311                                 }
312                         }
313                         delete iterator;
314                 }
315                 {
316                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
317                         SetIteratorOrderEdge *iterator = node->outEdges.iterator();
318                         while (iterator->hasNext()) {
319                                 OrderEdge *edge = iterator->next();
320                                 OrderNode *child = edge->sink;
321                                 if (!edge->mustNeg && sources->contains(child)) {
322                                         edge->mustNeg = true;
323                                         edge->polNeg = true;
324                                         if (edge->mustPos){
325 #ifdef TRACE_DEBUG
326                                                 model_println("DFS clear 3: NodeFrom:%lu=>edge%lu=>NodeTo:%lu", node->id, (uintptr_t) edge, child->id);
327 #endif
328                                                 solver->setUnSAT();
329                                         }
330                                 }
331                         }
332                         delete iterator;
333                 }
334         }
335
336         table->resetanddelete();
337         delete table;
338 }
339
340 /* This function finds edges that would form a cycle with must edges
341    and forces them to be mustNeg.  It also decides whether an edge
342    must be true because of transitivity from other must be true
343    edges. */
344
345 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
346         Vector<OrderNode *> finishNodes;
347         //Topologically sort the mustPos edge graph
348         DFSMust(graph, &finishNodes);
349         resetNodeInfoStatusSCC(graph);
350
351         //Find any backwards edges that complete cycles and force them to be mustNeg
352         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
353 }
354
355 /* This function finds edges that must be positive and forces the
356    inverse edge to be negative (and clears its positive polarity if it
357    had one). */
358
359 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
360         SetIteratorOrderEdge *iterator = graph->getEdges();
361         while (iterator->hasNext()) {
362                 OrderEdge *edge = iterator->next();
363                 if (edge->mustPos) {
364                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
365                         if (invEdge != NULL) {
366                                 if (!invEdge->mustPos) {
367                                         invEdge->polPos = false;
368                                 } else {
369 #ifdef TRACE_DEBUG
370                                         model_println("localMustAnalysis Total");
371 #endif
372                                         solver->setUnSAT();
373                                 }
374                                 invEdge->mustNeg = true;
375                                 invEdge->polNeg = true;
376                         }
377                 }
378         }
379         delete iterator;
380 }
381
382 /** This finds edges that must be positive and forces the inverse edge
383     to be negative.  It also clears the negative flag of this edge.
384     It also finds edges that must be negative and clears the positive
385     polarity. */
386
387 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
388         SetIteratorOrderEdge *iterator = graph->getEdges();
389         while (iterator->hasNext()) {
390                 OrderEdge *edge = iterator->next();
391                 if (edge->mustPos) {
392                         if (!edge->mustNeg) {
393                                 edge->polNeg = false;
394                         } else{
395 #ifdef TRACE_DEBUG
396                                 model_println("Local must analysis partial");
397 #endif
398                                 solver->setUnSAT();
399                         }
400                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
401                         if (invEdge != NULL) {
402                                 if (!invEdge->mustPos)
403                                         invEdge->polPos = false;
404                                 else{
405 #ifdef TRACE_DEBUG
406                                         model_println("Local must analysis partial 2");
407 #endif
408                                         solver->setUnSAT();
409                                 }
410                                 invEdge->mustNeg = true;
411                                 invEdge->polNeg = true;
412                         }
413                 }
414                 if (edge->mustNeg && !edge->mustPos) {
415                         edge->polPos = false;
416                 }
417         }
418         delete iterator;
419 }