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;
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 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node) {
94 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
95 while (hasNextOrderEdge(iterator)) {
96 OrderEdge *inEdge = nextOrderEdge(iterator);
98 OrderNode *src = inEdge->source;
99 if (src->status == VISITED) {
100 //Make a pseudoEdge to point backwards
101 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
102 newedge->pseudoPos = true;
106 deleteIterOrderEdge(iterator);
107 iterator = iteratorOrderEdge(node->outEdges);
108 while (hasNextOrderEdge(iterator)) {
109 OrderEdge *edge = nextOrderEdge(iterator);
110 if (!edge->polPos)//Ignore edges that do not have positive polarity
113 OrderNode *child = edge->sink;
114 if (child->status == NOTVISITED) {
115 child->status = VISITED;
116 DFSPseudoNodeVisit(graph, child);
117 child->status = FINISHED;
120 deleteIterOrderEdge(iterator);
123 void completePartialOrderGraph(OrderGraph *graph) {
124 VectorOrderNode finishNodes;
125 initDefVectorOrderNode(&finishNodes);
126 DFS(graph, &finishNodes);
127 resetNodeInfoStatusSCC(graph);
129 uint size = getSizeVectorOrderNode(&finishNodes);
130 for (int i = size - 1; i >= 0; i--) {
131 OrderNode *node = getVectorOrderNode(&finishNodes, i);
132 if (node->status == NOTVISITED) {
133 node->status = VISITED;
134 DFSPseudoNodeVisit(graph, node);
135 node->status = FINISHED;
139 resetNodeInfoStatusSCC(graph);
140 deleteVectorArrayOrderNode(&finishNodes);
143 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
144 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
145 while (hasNextOrderNode(iterator)) {
146 OrderNode *node = nextOrderNode(iterator);
147 if (node->status == NOTVISITED) {
148 node->status = VISITED;
149 DFSMustNodeVisit(node, finishNodes);
150 node->status = FINISHED;
151 pushVectorOrderNode(finishNodes, node);
154 deleteIterOrderNode(iterator);
157 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
158 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
159 while (hasNextOrderEdge(iterator)) {
160 OrderEdge *edge = nextOrderEdge(iterator);
161 OrderNode *child = edge->sink;
163 if (!edge->mustPos) //Ignore edges that are not must Positive edges
166 if (child->status == NOTVISITED) {
167 child->status = VISITED;
168 DFSMustNodeVisit(child, finishNodes);
169 child->status = FINISHED;
170 pushVectorOrderNode(finishNodes, child);
173 deleteIterOrderEdge(iterator);
177 void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
178 uint size = getSizeVectorOrderNode(finishNodes);
179 HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
181 for (int i = size - 1; i >= 0; i--) {
182 OrderNode *node = getVectorOrderNode(finishNodes, i);
183 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
184 putNodeToNodeSet(table, node, sources);
187 //Compute source sets
188 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
189 while (hasNextOrderEdge(iterator)) {
190 OrderEdge *edge = nextOrderEdge(iterator);
191 OrderNode *parent = edge->source;
193 addHashSetOrderNode(sources, parent);
194 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
195 addAllHashSetOrderNode(sources, parent_srcs);
198 deleteIterOrderEdge(iterator);
200 if (computeTransitiveClosure) {
201 //Compute full transitive closure for nodes
202 HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
203 while (hasNextOrderNode(srciterator)) {
204 OrderNode *srcnode = nextOrderNode(srciterator);
205 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
206 newedge->mustPos = true;
207 newedge->polPos = true;
208 addHashSetOrderEdge(srcnode->outEdges,newedge);
209 addHashSetOrderEdge(node->inEdges,newedge);
211 deleteIterOrderNode(srciterator);
214 //Use source sets to compute mustPos edges
215 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
216 while (hasNextOrderEdge(iterator)) {
217 OrderEdge *edge = nextOrderEdge(iterator);
218 OrderNode *parent = edge->source;
219 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
220 edge->mustPos = true;
223 deleteIterOrderEdge(iterator);
226 //Use source sets to compute mustNeg for edges that would introduce cycle if true
227 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
228 while (hasNextOrderEdge(iterator)) {
229 OrderEdge *edge = nextOrderEdge(iterator);
230 OrderNode *child = edge->sink;
231 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
232 edge->mustNeg = true;
235 deleteIterOrderEdge(iterator);
239 resetAndDeleteHashTableNodeToNodeSet(table);
242 /* This function finds edges that would form a cycle with must edges
243 and forces them to be mustNeg. It also decides whether an edge
244 must be true because of transitivity from other must be true
247 void reachMustAnalysis(OrderGraph *graph, bool computeTransitiveClosure) {
248 VectorOrderNode finishNodes;
249 initDefVectorOrderNode(&finishNodes);
250 //Topologically sort the mustPos edge graph
251 DFSMust(graph, &finishNodes);
252 resetNodeInfoStatusSCC(graph);
254 //Find any backwards edges that complete cycles and force them to be mustNeg
255 DFSClearContradictions(graph, &finishNodes, computeTransitiveClosure);
256 deleteVectorArrayOrderNode(&finishNodes);
257 resetNodeInfoStatusSCC(graph);
260 /* This function finds edges that must be positive and forces the
261 inverse edge to be negative (and clears its positive polarity if it
264 void localMustAnalysisTotal(OrderGraph *graph) {
265 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
266 while (hasNextOrderEdge(iterator)) {
267 OrderEdge *edge = nextOrderEdge(iterator);
269 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
270 if (invEdge != NULL && !invEdge->mustPos && invEdge->polPos) {
271 invEdge->polPos = false;
273 invEdge->mustNeg = true;
276 deleteIterOrderEdge(iterator);
279 /** This finds edges that must be positive and forces the inverse edge
280 to be negative. It also clears the negative flag of this edge.
281 It also finds edges that must be negative and clears the positive
284 void localMustAnalysisPartial(OrderGraph *graph) {
285 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
286 while (hasNextOrderEdge(iterator)) {
287 OrderEdge *edge = nextOrderEdge(iterator);
289 if (edge->polNeg && !edge->mustNeg) {
290 edge->polNeg = false;
292 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
293 if (invEdge != NULL) {
294 if (!invEdge->mustPos)
295 invEdge->polPos = false;
296 invEdge->mustNeg = true;
299 if (edge->mustNeg && !edge->mustPos) {
300 edge->polPos = false;
303 deleteIterOrderEdge(iterator);
306 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
307 VectorOrder ordervec;
308 initDefVectorOrder(&ordervec);
309 uint size = getSizeVectorBooleanOrder(&order->constraints);
310 for (uint i = 0; i < size; i++) {
311 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
312 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
313 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
314 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
315 if (from->sccNum < to->sccNum) {
317 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
318 } else if (to->sccNum < from->sccNum) {
320 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
322 //Build new order and change constraint's order
323 Order *neworder = NULL;
324 if (getSizeVectorOrder(&ordervec) > from->sccNum)
325 neworder = getVectorOrder(&ordervec, from->sccNum);
326 if (neworder == NULL) {
327 Set *set = (Set *) allocMutableSet(order->set->type);
328 neworder = allocOrder(order->type, set);
329 pushVectorOrder(This->allOrders, neworder);
330 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
332 if (from->status != ADDEDTOSET) {
333 from->status = ADDEDTOSET;
334 addElementMSet((MutableSet *)neworder->set, from->id);
336 if (to->status != ADDEDTOSET) {
337 to->status = ADDEDTOSET;
338 addElementMSet((MutableSet *)neworder->set, to->id);
340 orderconstraint->order = neworder;
341 addOrderConstraint(neworder, orderconstraint);
344 deleteVectorArrayOrder(&ordervec);
347 void orderAnalysis(CSolver *This) {
348 uint size = getSizeVectorOrder(This->allOrders);
349 for (uint i = 0; i < size; i++) {
350 Order *order = getVectorOrder(This->allOrders, i);
351 OrderGraph *graph = buildOrderGraph(order);
352 if (order->type == PARTIAL) {
353 //Required to do SCC analysis for partial order graphs. It
354 //makes sure we don't incorrectly optimize graphs with negative
356 completePartialOrderGraph(graph);
359 //This analysis is completely optional
360 reachMustAnalysis(graph, false);
362 //This pair of analysis is also optional
363 if (order->type == PARTIAL) {
364 localMustAnalysisPartial(graph);
366 localMustAnalysisTotal(graph);
369 //This optimization is completely optional
370 removeMustBeTrueNodes(graph);
372 //This is needed for splitorder
373 computeStronglyConnectedComponentGraph(graph);
375 decomposeOrder(This, order, graph);
377 deleteOrderGraph(graph);