1 #include "orderencoder.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
11 OrderGraph *buildOrderGraph(Order *order) {
12 OrderGraph *orderGraph = allocOrderGraph(order);
13 uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
14 for (uint j = 0; j < constrSize; j++) {
15 addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
20 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
21 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
22 while (hasNextOrderNode(iterator)) {
23 OrderNode *node = nextOrderNode(iterator);
24 if (node->status == NOTVISITED) {
25 node->status = VISITED;
26 DFSNodeVisit(node, finishNodes, false, 0);
27 node->status = FINISHED;
28 pushVectorOrderNode(finishNodes, node);
31 deleteIterOrderNode(iterator);
34 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
35 uint size = getSizeVectorOrderNode(finishNodes);
37 for (int i = size - 1; i >= 0; i--) {
38 OrderNode *node = getVectorOrderNode(finishNodes, i);
39 if (node->status == NOTVISITED) {
40 node->status = VISITED;
41 DFSNodeVisit(node, NULL, true, sccNum);
42 node->sccNum = sccNum;
43 node->status = FINISHED;
49 void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum) {
50 HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
51 while (hasNextOrderEdge(iterator)) {
52 OrderEdge *edge = nextOrderEdge(iterator);
53 if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
56 OrderNode *child = isReverse ? edge->source : edge->sink;
58 if (child->status == NOTVISITED) {
59 child->status = VISITED;
60 DFSNodeVisit(child, finishNodes, isReverse, sccNum);
61 child->status = FINISHED;
62 if (finishNodes != NULL)
63 pushVectorOrderNode(finishNodes, child);
65 child->sccNum = sccNum;
68 deleteIterOrderEdge(iterator);
71 void resetNodeInfoStatusSCC(OrderGraph *graph) {
72 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
73 while (hasNextOrderNode(iterator)) {
74 nextOrderNode(iterator)->status = NOTVISITED;
76 deleteIterOrderNode(iterator);
79 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
80 VectorOrderNode finishNodes;
81 initDefVectorOrderNode(&finishNodes);
82 DFS(graph, &finishNodes);
83 resetNodeInfoStatusSCC(graph);
84 DFSReverse(graph, &finishNodes);
85 resetNodeInfoStatusSCC(graph);
86 deleteVectorArrayOrderNode(&finishNodes);
89 void removeMustBeTrueNodes(OrderGraph *graph) {
90 //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
93 /** This function computes a source set for every nodes, the set of
94 nodes that can reach that node via pospolarity edges. It then
95 looks for negative polarity edges from nodes in the the source set
96 to determine whether we need to generate pseudoPos edges. */
98 void completePartialOrderGraph(OrderGraph *graph) {
99 VectorOrderNode finishNodes;
100 initDefVectorOrderNode(&finishNodes);
101 DFS(graph, &finishNodes);
102 resetNodeInfoStatusSCC(graph);
103 HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
105 VectorOrderNode sccNodes;
106 initDefVectorOrderNode(&sccNodes);
108 uint size = getSizeVectorOrderNode(&finishNodes);
110 for (int i = size - 1; i >= 0; i--) {
111 OrderNode *node = getVectorOrderNode(&finishNodes, i);
112 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
113 putNodeToNodeSet(table, node, sources);
115 if (node->status == NOTVISITED) {
116 //Need to do reverse traversal here...
117 node->status = VISITED;
118 DFSNodeVisit(node, &sccNodes, true, sccNum);
119 node->status = FINISHED;
120 node->sccNum = sccNum;
122 pushVectorOrderNode(&sccNodes, node);
124 //Compute in set for entire SCC
125 uint rSize = getSizeVectorOrderNode(&sccNodes);
126 for (int j = 0; j < rSize; j++) {
127 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
128 //Compute source sets
129 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
130 while (hasNextOrderEdge(iterator)) {
131 OrderEdge *edge = nextOrderEdge(iterator);
132 OrderNode *parent = edge->source;
134 addHashSetOrderNode(sources, parent);
135 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
136 addAllHashSetOrderNode(sources, parent_srcs);
139 deleteIterOrderEdge(iterator);
141 for (int j=0; j < rSize; j++) {
142 //Copy in set of entire SCC
143 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
144 HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
145 putNodeToNodeSet(table, rnode, set);
147 //Use source sets to compute pseudoPos edges
148 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
149 while (hasNextOrderEdge(iterator)) {
150 OrderEdge *edge = nextOrderEdge(iterator);
151 OrderNode *parent = edge->source;
152 ASSERT(parent != rnode);
153 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
154 containsHashSetOrderNode(sources, parent)) {
155 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
156 newedge->pseudoPos = true;
159 deleteIterOrderEdge(iterator);
162 clearVectorOrderNode(&sccNodes);
166 resetAndDeleteHashTableNodeToNodeSet(table);
167 resetNodeInfoStatusSCC(graph);
168 deleteVectorArrayOrderNode(&sccNodes);
169 deleteVectorArrayOrderNode(&finishNodes);
172 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
173 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
174 while (hasNextOrderNode(iterator)) {
175 OrderNode *node = nextOrderNode(iterator);
176 if (node->status == NOTVISITED) {
177 node->status = VISITED;
178 DFSMustNodeVisit(node, finishNodes);
179 node->status = FINISHED;
180 pushVectorOrderNode(finishNodes, node);
183 deleteIterOrderNode(iterator);
186 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
187 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
188 while (hasNextOrderEdge(iterator)) {
189 OrderEdge *edge = nextOrderEdge(iterator);
190 OrderNode *child = edge->sink;
192 if (!edge->mustPos) //Ignore edges that are not must Positive edges
195 if (child->status == NOTVISITED) {
196 child->status = VISITED;
197 DFSMustNodeVisit(child, finishNodes);
198 child->status = FINISHED;
199 pushVectorOrderNode(finishNodes, child);
202 deleteIterOrderEdge(iterator);
206 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
207 uint size = getSizeVectorOrderNode(finishNodes);
208 HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
210 for (int i = size - 1; i >= 0; i--) {
211 OrderNode *node = getVectorOrderNode(finishNodes, i);
212 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
213 putNodeToNodeSet(table, node, sources);
216 //Compute source sets
217 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
218 while (hasNextOrderEdge(iterator)) {
219 OrderEdge *edge = nextOrderEdge(iterator);
220 OrderNode *parent = edge->source;
222 addHashSetOrderNode(sources, parent);
223 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
224 addAllHashSetOrderNode(sources, parent_srcs);
227 deleteIterOrderEdge(iterator);
229 if (computeTransitiveClosure) {
230 //Compute full transitive closure for nodes
231 HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
232 while (hasNextOrderNode(srciterator)) {
233 OrderNode *srcnode = nextOrderNode(srciterator);
234 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
235 newedge->mustPos = true;
236 newedge->polPos = true;
237 if (newedge->mustNeg)
238 solver->unsat = true;
239 addHashSetOrderEdge(srcnode->outEdges,newedge);
240 addHashSetOrderEdge(node->inEdges,newedge);
242 deleteIterOrderNode(srciterator);
245 //Use source sets to compute mustPos edges
246 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
247 while (hasNextOrderEdge(iterator)) {
248 OrderEdge *edge = nextOrderEdge(iterator);
249 OrderNode *parent = edge->source;
250 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
251 edge->mustPos = true;
254 solver->unsat = true;
257 deleteIterOrderEdge(iterator);
260 //Use source sets to compute mustNeg for edges that would introduce cycle if true
261 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
262 while (hasNextOrderEdge(iterator)) {
263 OrderEdge *edge = nextOrderEdge(iterator);
264 OrderNode *child = edge->sink;
265 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
266 edge->mustNeg = true;
269 solver->unsat = true;
272 deleteIterOrderEdge(iterator);
276 resetAndDeleteHashTableNodeToNodeSet(table);
279 /* This function finds edges that would form a cycle with must edges
280 and forces them to be mustNeg. It also decides whether an edge
281 must be true because of transitivity from other must be true
284 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
285 VectorOrderNode finishNodes;
286 initDefVectorOrderNode(&finishNodes);
287 //Topologically sort the mustPos edge graph
288 DFSMust(graph, &finishNodes);
289 resetNodeInfoStatusSCC(graph);
291 //Find any backwards edges that complete cycles and force them to be mustNeg
292 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
293 deleteVectorArrayOrderNode(&finishNodes);
296 /* This function finds edges that must be positive and forces the
297 inverse edge to be negative (and clears its positive polarity if it
300 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
301 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
302 while (hasNextOrderEdge(iterator)) {
303 OrderEdge *edge = nextOrderEdge(iterator);
305 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
306 if (invEdge != NULL) {
307 if (!invEdge->mustPos) {
308 invEdge->polPos = false;
310 solver->unsat = true;
312 invEdge->mustNeg = true;
313 invEdge->polNeg = true;
317 deleteIterOrderEdge(iterator);
320 /** This finds edges that must be positive and forces the inverse edge
321 to be negative. It also clears the negative flag of this edge.
322 It also finds edges that must be negative and clears the positive
325 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
326 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
327 while (hasNextOrderEdge(iterator)) {
328 OrderEdge *edge = nextOrderEdge(iterator);
330 if (!edge->mustNeg) {
331 edge->polNeg = false;
333 solver->unsat = true;
335 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
336 if (invEdge != NULL) {
337 if (!invEdge->mustPos)
338 invEdge->polPos = false;
340 solver->unsat = true;
341 invEdge->mustNeg = true;
342 invEdge->polNeg = true;
345 if (edge->mustNeg && !edge->mustPos) {
346 edge->polPos = false;
349 deleteIterOrderEdge(iterator);
352 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
353 VectorOrder ordervec;
354 initDefVectorOrder(&ordervec);
355 uint size = getSizeVectorBooleanOrder(&order->constraints);
356 for (uint i = 0; i < size; i++) {
357 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
358 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
359 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
360 if (from->sccNum != to->sccNum) {
361 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
363 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
364 } else if (edge->polNeg) {
365 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
367 //This case should only be possible if constraint isn't in AST
371 //Build new order and change constraint's order
372 Order *neworder = NULL;
373 if (getSizeVectorOrder(&ordervec) > from->sccNum)
374 neworder = getVectorOrder(&ordervec, from->sccNum);
375 if (neworder == NULL) {
376 Set *set = (Set *) allocMutableSet(order->set->type);
377 neworder = allocOrder(order->type, set);
378 pushVectorOrder(This->allOrders, neworder);
379 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
381 if (from->status != ADDEDTOSET) {
382 from->status = ADDEDTOSET;
383 addElementMSet((MutableSet *)neworder->set, from->id);
385 if (to->status != ADDEDTOSET) {
386 to->status = ADDEDTOSET;
387 addElementMSet((MutableSet *)neworder->set, to->id);
389 orderconstraint->order = neworder;
390 addOrderConstraint(neworder, orderconstraint);
393 deleteVectorArrayOrder(&ordervec);
396 void orderAnalysis(CSolver *This) {
397 uint size = getSizeVectorOrder(This->allOrders);
398 for (uint i = 0; i < size; i++) {
399 Order *order = getVectorOrder(This->allOrders, i);
400 OrderGraph *graph = buildOrderGraph(order);
401 if (order->type == PARTIAL) {
402 //Required to do SCC analysis for partial order graphs. It
403 //makes sure we don't incorrectly optimize graphs with negative
405 completePartialOrderGraph(graph);
408 //This analysis is completely optional
409 reachMustAnalysis(This, graph, false);
411 //This pair of analysis is also optional
412 if (order->type == PARTIAL) {
413 localMustAnalysisPartial(This, graph);
415 localMustAnalysisTotal(This, graph);
418 //This optimization is completely optional
419 removeMustBeTrueNodes(graph);
421 //This is needed for splitorder
422 computeStronglyConnectedComponentGraph(graph);
424 decomposeOrder(This, order, graph);
426 deleteOrderGraph(graph);