80558f3916df2fd4d49f19a350e061636c5368b2
[satune.git] / src / Encoders / orderencoder.cc
1 #include "orderencoder.h"
2 #include "structs.h"
3 #include "csolver.h"
4 #include "boolean.h"
5 #include "ordergraph.h"
6 #include "order.h"
7 #include "ordernode.h"
8 #include "rewriter.h"
9 #include "mutableset.h"
10 #include "tunable.h"
11
12 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
13         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
14         while (hasNextOrderNode(iterator)) {
15                 OrderNode *node = nextOrderNode(iterator);
16                 if (node->status == NOTVISITED) {
17                         node->status = VISITED;
18                         DFSNodeVisit(node, finishNodes, false, false, 0);
19                         node->status = FINISHED;
20                         pushVectorOrderNode(finishNodes, node);
21                 }
22         }
23         deleteIterOrderNode(iterator);
24 }
25
26 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
27         uint size = getSizeVectorOrderNode(finishNodes);
28         uint sccNum = 1;
29         for (int i = size - 1; i >= 0; i--) {
30                 OrderNode *node = getVectorOrderNode(finishNodes, 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;
36                         sccNum++;
37                 }
38         }
39 }
40
41 void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
42         HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
43         while (hasNextOrderEdge(iterator)) {
44                 OrderEdge *edge = nextOrderEdge(iterator);
45                 if (mustvisit) {
46                         if (!edge->mustPos)
47                                 continue;
48                 } else
49                         if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
50                                 continue;
51
52                 OrderNode *child = isReverse ? edge->source : edge->sink;
53
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                                 pushVectorOrderNode(finishNodes, child);
60                         if (isReverse)
61                                 child->sccNum = sccNum;
62                 }
63         }
64         deleteIterOrderEdge(iterator);
65 }
66
67 void resetNodeInfoStatusSCC(OrderGraph *graph) {
68         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
69         while (hasNextOrderNode(iterator)) {
70                 nextOrderNode(iterator)->status = NOTVISITED;
71         }
72         deleteIterOrderNode(iterator);
73 }
74
75 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
76         VectorOrderNode finishNodes;
77         initDefVectorOrderNode(&finishNodes);
78         DFS(graph, &finishNodes);
79         resetNodeInfoStatusSCC(graph);
80         DFSReverse(graph, &finishNodes);
81         resetNodeInfoStatusSCC(graph);
82         deleteVectorArrayOrderNode(&finishNodes);
83 }
84
85 void removeMustBeTrueNodes(OrderGraph *graph) {
86         //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
87 }
88
89 /** This function computes a source set for every nodes, the set of
90                 nodes that can reach that node via pospolarity edges.  It then
91                 looks for negative polarity edges from nodes in the the source set
92                 to determine whether we need to generate pseudoPos edges. */
93
94 void completePartialOrderGraph(OrderGraph *graph) {
95         VectorOrderNode finishNodes;
96         initDefVectorOrderNode(&finishNodes);
97         DFS(graph, &finishNodes);
98         resetNodeInfoStatusSCC(graph);
99         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
100
101         VectorOrderNode sccNodes;
102         initDefVectorOrderNode(&sccNodes);
103         
104         uint size = getSizeVectorOrderNode(&finishNodes);
105         uint sccNum = 1;
106         for (int i = size - 1; i >= 0; i--) {
107                 OrderNode *node = getVectorOrderNode(&finishNodes, i);
108                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
109                 putNodeToNodeSet(table, node, sources);
110                 
111                 if (node->status == NOTVISITED) {
112                         //Need to do reverse traversal here...
113                         node->status = VISITED;
114                         DFSNodeVisit(node, &sccNodes, true, false, sccNum);
115                         node->status = FINISHED;
116                         node->sccNum = sccNum;
117                         sccNum++;
118                         pushVectorOrderNode(&sccNodes, node);
119
120                         //Compute in set for entire SCC
121                         uint rSize = getSizeVectorOrderNode(&sccNodes);
122                         for (uint j = 0; j < rSize; j++) {
123                                 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
124                                 //Compute source sets
125                                 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
126                                 while (hasNextOrderEdge(iterator)) {
127                                         OrderEdge *edge = nextOrderEdge(iterator);
128                                         OrderNode *parent = edge->source;
129                                         if (edge->polPos) {
130                                                 addHashSetOrderNode(sources, parent);
131                                                 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
132                                                 addAllHashSetOrderNode(sources, parent_srcs);
133                                         }
134                                 }
135                                 deleteIterOrderEdge(iterator);
136                         }
137                         for (uint j=0; j < rSize; j++) {
138                                 //Copy in set of entire SCC
139                                 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
140                                 HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
141                                 putNodeToNodeSet(table, rnode, set);
142
143                                 //Use source sets to compute pseudoPos edges
144                                 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
145                                 while (hasNextOrderEdge(iterator)) {
146                                         OrderEdge *edge = nextOrderEdge(iterator);
147                                         OrderNode *parent = edge->source;
148                                         ASSERT(parent != rnode);
149                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
150                                                         containsHashSetOrderNode(sources, parent)) {
151                                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
152                                                 newedge->pseudoPos = true;
153                                         }
154                                 }
155                                 deleteIterOrderEdge(iterator);
156                         }
157                         
158                         clearVectorOrderNode(&sccNodes);
159                 }
160         }
161
162         resetAndDeleteHashTableNodeToNodeSet(table);
163         deleteHashTableNodeToNodeSet(table);
164         resetNodeInfoStatusSCC(graph);
165         deleteVectorArrayOrderNode(&sccNodes);
166         deleteVectorArrayOrderNode(&finishNodes);
167 }
168
169 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
170         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
171         while (hasNextOrderNode(iterator)) {
172                 OrderNode *node = nextOrderNode(iterator);
173                 if (node->status == NOTVISITED) {
174                         node->status = VISITED;
175                         DFSNodeVisit(node, finishNodes, false, true, 0);
176                         node->status = FINISHED;
177                         pushVectorOrderNode(finishNodes, node);
178                 }
179         }
180         deleteIterOrderNode(iterator);
181 }
182
183 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
184         uint size = getSizeVectorOrderNode(finishNodes);
185         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
186
187         for (int i = size - 1; i >= 0; i--) {
188                 OrderNode *node = getVectorOrderNode(finishNodes, i);
189                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
190                 putNodeToNodeSet(table, node, sources);
191
192                 {
193                         //Compute source sets
194                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
195                         while (hasNextOrderEdge(iterator)) {
196                                 OrderEdge *edge = nextOrderEdge(iterator);
197                                 OrderNode *parent = edge->source;
198                                 if (edge->mustPos) {
199                                         addHashSetOrderNode(sources, parent);
200                                         HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
201                                         addAllHashSetOrderNode(sources, parent_srcs);
202                                 }
203                         }
204                         deleteIterOrderEdge(iterator);
205                 }
206                 if (computeTransitiveClosure) {
207                         //Compute full transitive closure for nodes
208                         HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
209                         while (hasNextOrderNode(srciterator)) {
210                                 OrderNode *srcnode = nextOrderNode(srciterator);
211                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
212                                 newedge->mustPos = true;
213                                 newedge->polPos = true;
214                                 if (newedge->mustNeg)
215                                         solver->unsat = true;
216                                 addHashSetOrderEdge(srcnode->outEdges,newedge);
217                                 addHashSetOrderEdge(node->inEdges,newedge);
218                         }
219                         deleteIterOrderNode(srciterator);
220                 }
221                 {
222                         //Use source sets to compute mustPos edges
223                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
224                         while (hasNextOrderEdge(iterator)) {
225                                 OrderEdge *edge = nextOrderEdge(iterator);
226                                 OrderNode *parent = edge->source;
227                                 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
228                                         edge->mustPos = true;
229                                         edge->polPos = true;
230                                         if (edge->mustNeg)
231                                                 solver->unsat = true;
232                                 }
233                         }
234                         deleteIterOrderEdge(iterator);
235                 }
236                 {
237                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
238                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
239                         while (hasNextOrderEdge(iterator)) {
240                                 OrderEdge *edge = nextOrderEdge(iterator);
241                                 OrderNode *child = edge->sink;
242                                 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
243                                         edge->mustNeg = true;
244                                         edge->polNeg = true;
245                                         if (edge->mustPos)
246                                                 solver->unsat = true;
247                                 }
248                         }
249                         deleteIterOrderEdge(iterator);
250                 }
251         }
252
253         resetAndDeleteHashTableNodeToNodeSet(table);
254         deleteHashTableNodeToNodeSet(table);
255 }
256
257 /* This function finds edges that would form a cycle with must edges
258    and forces them to be mustNeg.  It also decides whether an edge
259    must be true because of transitivity from other must be true
260    edges. */
261
262 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
263         VectorOrderNode finishNodes;
264         initDefVectorOrderNode(&finishNodes);
265         //Topologically sort the mustPos edge graph
266         DFSMust(graph, &finishNodes);
267         resetNodeInfoStatusSCC(graph);
268
269         //Find any backwards edges that complete cycles and force them to be mustNeg
270         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
271         deleteVectorArrayOrderNode(&finishNodes);
272 }
273
274 /* This function finds edges that must be positive and forces the
275    inverse edge to be negative (and clears its positive polarity if it
276    had one). */
277
278 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
279         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
280         while (hasNextOrderEdge(iterator)) {
281                 OrderEdge *edge = nextOrderEdge(iterator);
282                 if (edge->mustPos) {
283                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
284                         if (invEdge != NULL) {
285                                 if (!invEdge->mustPos) {
286                                         invEdge->polPos = false;
287                                 } else {
288                                         solver->unsat = true;
289                                 }
290                                 invEdge->mustNeg = true;
291                                 invEdge->polNeg = true;
292                         }
293                 }
294         }
295         deleteIterOrderEdge(iterator);
296 }
297
298 /** This finds edges that must be positive and forces the inverse edge
299     to be negative.  It also clears the negative flag of this edge.
300     It also finds edges that must be negative and clears the positive
301     polarity. */
302
303 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
304         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
305         while (hasNextOrderEdge(iterator)) {
306                 OrderEdge *edge = nextOrderEdge(iterator);
307                 if (edge->mustPos) {
308                         if (!edge->mustNeg) {
309                                 edge->polNeg = false;
310                         } else
311                                 solver->unsat = true;
312
313                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
314                         if (invEdge != NULL) {
315                                 if (!invEdge->mustPos)
316                                         invEdge->polPos = false;
317                                 else
318                                         solver->unsat = true;
319                                 invEdge->mustNeg = true;
320                                 invEdge->polNeg = true;
321                         }
322                 }
323                 if (edge->mustNeg && !edge->mustPos) {
324                         edge->polPos = false;
325                 }
326         }
327         deleteIterOrderEdge(iterator);
328 }
329
330 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
331         VectorOrder ordervec;
332         VectorOrder partialcandidatevec;
333         initDefVectorOrder(&ordervec);
334         initDefVectorOrder(&partialcandidatevec);
335         uint size = getSizeVectorBooleanOrder(&order->constraints);
336         for (uint i = 0; i < size; i++) {
337                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
338                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
339                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
340                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
341                 if (from->sccNum != to->sccNum) {
342                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
343                         if (edge->polPos) {
344                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
345                         } else if (edge->polNeg) {
346                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
347                         } else {
348                                 //This case should only be possible if constraint isn't in AST
349                                 ASSERT(0);
350                         }
351                 } else {
352                         //Build new order and change constraint's order
353                         Order *neworder = NULL;
354                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
355                                 neworder = getVectorOrder(&ordervec, from->sccNum);
356                         if (neworder == NULL) {
357                                 Set *set = (Set *) allocMutableSet(order->set->type);
358                                 neworder = allocOrder(order->type, set);
359                                 pushVectorOrder(This->allOrders, neworder);
360                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
361                                 if (order->type == PARTIAL)
362                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder);
363                                 else
364                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
365                         }
366                         if (from->status != ADDEDTOSET) {
367                                 from->status = ADDEDTOSET;
368                                 addElementMSet((MutableSet *)neworder->set, from->id);
369                         }
370                         if (to->status != ADDEDTOSET) {
371                                 to->status = ADDEDTOSET;
372                                 addElementMSet((MutableSet *)neworder->set, to->id);
373                         }
374                         if (order->type == PARTIAL) {
375                                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
376                                 if (edge->polNeg)
377                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
378                         }
379                         orderconstraint->order = neworder;
380                         addOrderConstraint(neworder, orderconstraint);
381                 }
382         }
383
384         uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
385         for(uint i=0;i<pcvsize;i++) {
386                 Order * neworder=getVectorOrder(&partialcandidatevec, i);
387                 if (neworder != NULL){
388                         neworder->type = TOTAL;
389                         model_print("i=%u\t", i);
390                 }
391         }
392         
393         deleteVectorArrayOrder(&ordervec);
394         deleteVectorArrayOrder(&partialcandidatevec);
395 }
396
397 void orderAnalysis(CSolver *This) {
398         uint size = getSizeVectorOrder(This->allOrders);
399         for (uint i = 0; i < size; i++) {
400                 Order *order = getVectorOrder(This->allOrders, i);
401                 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
402                 if (!doDecompose)
403                         continue;
404                 
405                 OrderGraph *graph = buildOrderGraph(order);
406                 if (order->type == PARTIAL) {
407                         //Required to do SCC analysis for partial order graphs.  It
408                         //makes sure we don't incorrectly optimize graphs with negative
409                         //polarity edges
410                         completePartialOrderGraph(graph);
411                 }
412
413
414                 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
415
416                 if (mustReachGlobal)
417                         reachMustAnalysis(This, graph, false);
418
419                 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
420                 
421                 if (mustReachLocal) {
422                         //This pair of analysis is also optional
423                         if (order->type == PARTIAL) {
424                                 localMustAnalysisPartial(This, graph);
425                         } else {
426                                 localMustAnalysisTotal(This, graph);
427                         }
428                 }
429
430                 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
431                 
432                 if (mustReachPrune)
433                         removeMustBeTrueNodes(graph);
434                 
435                 //This is needed for splitorder
436                 computeStronglyConnectedComponentGraph(graph);
437                 
438                 decomposeOrder(This, order, graph);
439                 
440                 deleteOrderGraph(graph);
441         }
442 }