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 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->mustPos && 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 && !invEdge->mustPos) {
294 invEdge->polPos = false;
296 invEdge->mustNeg = true;
298 if (edge->mustNeg && !edge->mustPos) {
299 edge->polPos = false;
302 deleteIterOrderEdge(iterator);
305 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
306 VectorOrder ordervec;
307 initDefVectorOrder(&ordervec);
308 uint size = getSizeVectorBooleanOrder(&order->constraints);
309 for (uint i = 0; i < size; i++) {
310 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
311 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
312 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
313 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
314 if (from->sccNum < to->sccNum) {
316 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
317 } else if (to->sccNum < from->sccNum) {
319 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
321 //Build new order and change constraint's order
322 Order *neworder = NULL;
323 if (getSizeVectorOrder(&ordervec) > from->sccNum)
324 neworder = getVectorOrder(&ordervec, from->sccNum);
325 if (neworder == NULL) {
326 Set *set = (Set *) allocMutableSet(order->set->type);
327 neworder = allocOrder(order->type, set);
328 pushVectorOrder(This->allOrders, neworder);
329 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
331 if (from->status != ADDEDTOSET) {
332 from->status = ADDEDTOSET;
333 addElementMSet((MutableSet *)neworder->set, from->id);
335 if (to->status != ADDEDTOSET) {
336 to->status = ADDEDTOSET;
337 addElementMSet((MutableSet *)neworder->set, to->id);
339 orderconstraint->order = neworder;
340 addOrderConstraint(neworder, orderconstraint);
343 deleteVectorArrayOrder(&ordervec);
346 void orderAnalysis(CSolver *This) {
347 uint size = getSizeVectorOrder(This->allOrders);
348 for (uint i = 0; i < size; i++) {
349 Order *order = getVectorOrder(This->allOrders, i);
350 OrderGraph *graph = buildOrderGraph(order);
351 if (order->type == PARTIAL) {
352 //Required to do SCC analysis for partial order graphs. It
353 //makes sure we don't incorrectly optimize graphs with negative
355 completePartialOrderGraph(graph);
358 //This analysis is completely optional
359 reachMustAnalysis(graph, false);
361 //This pair of analysis is also optional
362 if (order->type == PARTIAL) {
363 localMustAnalysisPartial(graph);
365 localMustAnalysisTotal(graph);
368 //This optimization is completely optional
369 removeMustBeTrueNodes(graph);
371 //This is needed for splitorder
372 computeStronglyConnectedComponentGraph(graph);
374 decomposeOrder(This, order, graph);
376 deleteOrderGraph(graph);