1 #include "orderencoder.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
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);
23 deleteIterOrderNode(iterator);
26 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
27 uint size = getSizeVectorOrderNode(finishNodes);
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;
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);
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 pushVectorOrderNode(finishNodes, child);
61 child->sccNum = sccNum;
64 deleteIterOrderEdge(iterator);
67 void resetNodeInfoStatusSCC(OrderGraph *graph) {
68 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
69 while (hasNextOrderNode(iterator)) {
70 nextOrderNode(iterator)->status = NOTVISITED;
72 deleteIterOrderNode(iterator);
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);
85 void removeMustBeTrueNodes(OrderGraph *graph) {
86 //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
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. */
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);
101 VectorOrderNode sccNodes;
102 initDefVectorOrderNode(&sccNodes);
104 uint size = getSizeVectorOrderNode(&finishNodes);
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);
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;
118 pushVectorOrderNode(&sccNodes, node);
120 //Compute in set for entire SCC
121 uint rSize = getSizeVectorOrderNode(&sccNodes);
122 for (int 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;
130 addHashSetOrderNode(sources, parent);
131 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
132 addAllHashSetOrderNode(sources, parent_srcs);
135 deleteIterOrderEdge(iterator);
137 for (int 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);
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;
155 deleteIterOrderEdge(iterator);
158 clearVectorOrderNode(&sccNodes);
162 resetAndDeleteHashTableNodeToNodeSet(table);
163 deleteHashTableNodeToNodeSet(table);
164 resetNodeInfoStatusSCC(graph);
165 deleteVectorArrayOrderNode(&sccNodes);
166 deleteVectorArrayOrderNode(&finishNodes);
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);
180 deleteIterOrderNode(iterator);
183 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
184 uint size = getSizeVectorOrderNode(finishNodes);
185 HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
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);
193 //Compute source sets
194 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
195 while (hasNextOrderEdge(iterator)) {
196 OrderEdge *edge = nextOrderEdge(iterator);
197 OrderNode *parent = edge->source;
199 addHashSetOrderNode(sources, parent);
200 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
201 addAllHashSetOrderNode(sources, parent_srcs);
204 deleteIterOrderEdge(iterator);
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);
219 deleteIterOrderNode(srciterator);
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;
231 solver->unsat = true;
234 deleteIterOrderEdge(iterator);
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;
246 solver->unsat = true;
249 deleteIterOrderEdge(iterator);
253 resetAndDeleteHashTableNodeToNodeSet(table);
254 deleteHashTableNodeToNodeSet(table);
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
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);
269 //Find any backwards edges that complete cycles and force them to be mustNeg
270 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
271 deleteVectorArrayOrderNode(&finishNodes);
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
278 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
279 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
280 while (hasNextOrderEdge(iterator)) {
281 OrderEdge *edge = nextOrderEdge(iterator);
283 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
284 if (invEdge != NULL) {
285 if (!invEdge->mustPos) {
286 invEdge->polPos = false;
288 solver->unsat = true;
290 invEdge->mustNeg = true;
291 invEdge->polNeg = true;
295 deleteIterOrderEdge(iterator);
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
303 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
304 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
305 while (hasNextOrderEdge(iterator)) {
306 OrderEdge *edge = nextOrderEdge(iterator);
308 if (!edge->mustNeg) {
309 edge->polNeg = false;
311 solver->unsat = true;
313 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
314 if (invEdge != NULL) {
315 if (!invEdge->mustPos)
316 invEdge->polPos = false;
318 solver->unsat = true;
319 invEdge->mustNeg = true;
320 invEdge->polNeg = true;
323 if (edge->mustNeg && !edge->mustPos) {
324 edge->polPos = false;
327 deleteIterOrderEdge(iterator);
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 if (from->sccNum != to->sccNum) {
341 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
343 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
344 } else if (edge->polNeg) {
345 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
347 //This case should only be possible if constraint isn't in AST
351 //Build new order and change constraint's order
352 Order *neworder = NULL;
353 if (getSizeVectorOrder(&ordervec) > from->sccNum)
354 neworder = getVectorOrder(&ordervec, from->sccNum);
355 if (neworder == NULL) {
356 Set *set = (Set *) allocMutableSet(order->set->type);
357 neworder = allocOrder(order->type, set);
358 pushVectorOrder(This->allOrders, neworder);
359 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
360 if (order->type == PARTIAL)
361 setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder);
363 setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
365 if (from->status != ADDEDTOSET) {
366 from->status = ADDEDTOSET;
367 addElementMSet((MutableSet *)neworder->set, from->id);
369 if (to->status != ADDEDTOSET) {
370 to->status = ADDEDTOSET;
371 addElementMSet((MutableSet *)neworder->set, to->id);
373 if (order->type == PARTIAL) {
374 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
376 setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
378 orderconstraint->order = neworder;
379 addOrderConstraint(neworder, orderconstraint);
383 uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
384 for(uint i=0;i<pcvsize;i++) {
385 Order * neworder=getVectorOrder(&partialcandidatevec, i);
386 if (neworder != NULL)
387 neworder->type = TOTAL;
390 deleteVectorArrayOrder(&ordervec);
391 deleteVectorArrayOrder(&partialcandidatevec);
394 void orderAnalysis(CSolver *This) {
395 uint size = getSizeVectorOrder(This->allOrders);
396 for (uint i = 0; i < size; i++) {
397 Order *order = getVectorOrder(This->allOrders, i);
398 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
402 OrderGraph *graph = buildOrderGraph(order);
403 if (order->type == PARTIAL) {
404 //Required to do SCC analysis for partial order graphs. It
405 //makes sure we don't incorrectly optimize graphs with negative
407 completePartialOrderGraph(graph);
411 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
414 reachMustAnalysis(This, graph, false);
416 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
418 if (mustReachLocal) {
419 //This pair of analysis is also optional
420 if (order->type == PARTIAL) {
421 localMustAnalysisPartial(This, graph);
423 localMustAnalysisTotal(This, graph);
427 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
430 removeMustBeTrueNodes(graph);
432 //This is needed for splitorder
433 computeStronglyConnectedComponentGraph(graph);
435 decomposeOrder(This, order, graph);
437 deleteOrderGraph(graph);