1 #include "orderencoder.h"
5 #include "ordergraph.h"
10 OrderGraph *buildOrderGraph(Order *order) {
11 OrderGraph *orderGraph = allocOrderGraph(order);
12 uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
13 for (uint j = 0; j < constrSize; j++) {
14 addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
19 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
20 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
21 while (hasNextOrderNode(iterator)) {
22 OrderNode *node = nextOrderNode(iterator);
23 if (node->status == NOTVISITED) {
24 node->status = VISITED;
25 DFSNodeVisit(node, finishNodes, false, 0);
26 node->status = FINISHED;
27 pushVectorOrderNode(finishNodes, node);
30 deleteIterOrderNode(iterator);
33 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
34 uint size = getSizeVectorOrderNode(finishNodes);
36 for (int i = size - 1; i >= 0; i--) {
37 OrderNode *node = getVectorOrderNode(finishNodes, i);
38 if (node->status == NOTVISITED) {
39 node->status = VISITED;
40 DFSNodeVisit(node, NULL, true, sccNum);
41 node->sccNum = sccNum;
42 node->status = FINISHED;
48 void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum) {
49 HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
50 while (hasNextOrderEdge(iterator)) {
51 OrderEdge *edge = nextOrderEdge(iterator);
52 if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
55 OrderNode *child = isReverse ? edge->source : edge->sink;
57 if (child->status == NOTVISITED) {
58 child->status = VISITED;
59 DFSNodeVisit(child, finishNodes, isReverse, sccNum);
60 child->status = FINISHED;
62 pushVectorOrderNode(finishNodes, child);
64 child->sccNum = sccNum;
67 deleteIterOrderEdge(iterator);
70 void resetNodeInfoStatusSCC(OrderGraph *graph) {
71 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
72 while (hasNextOrderNode(iterator)) {
73 nextOrderNode(iterator)->status = NOTVISITED;
75 deleteIterOrderNode(iterator);
78 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
79 VectorOrderNode finishNodes;
80 initDefVectorOrderNode(&finishNodes);
81 DFS(graph, &finishNodes);
82 resetNodeInfoStatusSCC(graph);
83 DFSReverse(graph, &finishNodes);
84 resetNodeInfoStatusSCC(graph);
85 deleteVectorArrayOrderNode(&finishNodes);
88 void removeMustBeTrueNodes(OrderGraph *graph) {
89 //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
92 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node) {
93 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
94 while (hasNextOrderEdge(iterator)) {
95 OrderEdge *inEdge = nextOrderEdge(iterator);
97 OrderNode *src = inEdge->source;
98 if (src->status == VISITED) {
99 //Make a pseudoEdge to point backwards
100 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
101 newedge->pseudoPos = true;
105 deleteIterOrderEdge(iterator);
106 iterator = iteratorOrderEdge(node->outEdges);
107 while (hasNextOrderEdge(iterator)) {
108 OrderEdge *edge = nextOrderEdge(iterator);
109 if (!edge->polPos)//Ignore edges that do not have positive polarity
112 OrderNode *child = edge->sink;
113 if (child->status == NOTVISITED) {
114 child->status = VISITED;
115 DFSPseudoNodeVisit(graph, child);
116 child->status = FINISHED;
119 deleteIterOrderEdge(iterator);
122 void completePartialOrderGraph(OrderGraph *graph) {
123 VectorOrderNode finishNodes;
124 initDefVectorOrderNode(&finishNodes);
125 DFS(graph, &finishNodes);
126 resetNodeInfoStatusSCC(graph);
128 uint size = getSizeVectorOrderNode(&finishNodes);
129 for (int i = size - 1; i >= 0; i--) {
130 OrderNode *node = getVectorOrderNode(&finishNodes, i);
131 if (node->status == NOTVISITED) {
132 node->status = VISITED;
133 DFSPseudoNodeVisit(graph, node);
134 node->status = FINISHED;
138 resetNodeInfoStatusSCC(graph);
139 deleteVectorArrayOrderNode(&finishNodes);
142 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
143 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
144 while (hasNextOrderNode(iterator)) {
145 OrderNode *node = nextOrderNode(iterator);
146 if (node->status == NOTVISITED) {
147 node->status = VISITED;
148 DFSMustNodeVisit(node, finishNodes, false);
149 node->status = FINISHED;
150 pushVectorOrderNode(finishNodes, node);
153 deleteIterOrderNode(iterator);
156 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges) {
157 //First compute implication of transitive closure on must pos edges
158 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
159 while (hasNextOrderEdge(iterator)) {
160 OrderEdge *edge = nextOrderEdge(iterator);
161 OrderNode *parent = edge->source;
162 if (parent->status == VISITED) {
163 edge->mustPos = true;
166 deleteIterOrderEdge(iterator);
168 //Next compute implication of transitive closure on must neg edges
169 iterator = iteratorOrderEdge(node->outEdges);
170 while (hasNextOrderEdge(iterator)) {
171 OrderEdge *edge = nextOrderEdge(iterator);
172 OrderNode *child = edge->sink;
174 if (clearBackEdges && child->status == VISITED) {
175 //We have a backedge, so note that this edge must be negative
176 edge->mustNeg = true;
179 if (!edge->mustPos) //Ignore edges that are not must Positive edges
182 if (child->status == NOTVISITED) {
183 child->status = VISITED;
184 DFSMustNodeVisit(child, finishNodes, clearBackEdges);
185 child->status = FINISHED;
186 pushVectorOrderNode(finishNodes, child);
189 deleteIterOrderEdge(iterator);
192 void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes) {
193 uint size = getSizeVectorOrderNode(finishNodes);
194 for (int i = size - 1; i >= 0; i--) {
195 OrderNode *node = getVectorOrderNode(finishNodes, i);
196 if (node->status == NOTVISITED) {
197 node->status = VISITED;
198 DFSMustNodeVisit(node, NULL, true);
199 node->status = FINISHED;
204 /* This function finds edges that would form a cycle with must edges
205 and forces them to be mustNeg. It also decides whether an edge
206 must be true because of transitivity from other must be true
209 void reachMustAnalysis(OrderGraph *graph) {
210 VectorOrderNode finishNodes;
211 initDefVectorOrderNode(&finishNodes);
212 //Topologically sort the mustPos edge graph
213 DFSMust(graph, &finishNodes);
214 resetNodeInfoStatusSCC(graph);
216 //Find any backwards edges that complete cycles and force them to be mustNeg
217 DFSClearContradictions(graph, &finishNodes);
218 deleteVectorArrayOrderNode(&finishNodes);
219 resetNodeInfoStatusSCC(graph);
222 /* This function finds edges that must be positive and forces the
223 inverse edge to be negative (and clears its positive polarity if it
226 void localMustAnalysisTotal(OrderGraph *graph) {
227 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
228 while (hasNextOrderEdge(iterator)) {
229 OrderEdge *edge = nextOrderEdge(iterator);
231 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
232 if (invEdge != NULL && !invEdge->mustPos && invEdge->polPos) {
233 invEdge->polPos = false;
235 invEdge->mustNeg = true;
238 deleteIterOrderEdge(iterator);
241 /** This finds edges that must be positive and forces the inverse edge
242 to be negative. It also clears the negative flag of this edge.
243 It also finds edges that must be negative and clears the positive
246 void localMustAnalysisPartial(OrderGraph *graph) {
247 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
248 while (hasNextOrderEdge(iterator)) {
249 OrderEdge *edge = nextOrderEdge(iterator);
251 if (edge->polNeg && !edge->mustNeg) {
252 edge->polNeg = false;
254 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
255 if (invEdge != NULL && !invEdge->mustPos) {
256 invEdge->polPos = false;
258 invEdge->mustNeg = true;
260 if (edge->mustNeg && !edge->mustPos) {
261 edge->polPos = false;
264 deleteIterOrderEdge(iterator);
267 void decomposeOrder(Order *order, OrderGraph *graph) {
268 uint size = getSizeVectorBooleanOrder(&order->constraints);
269 for (uint i = 0; i < size; i++) {
270 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
271 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
272 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
273 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
274 if (from->sccNum < to->sccNum) {
276 replaceBooleanWithTrue((Boolean *)orderconstraint);
277 } else if (to->sccNum < from->sccNum) {
279 replaceBooleanWithFalse((Boolean *)orderconstraint);
281 //Build new order and change constraint's order
287 void orderAnalysis(CSolver *This) {
288 uint size = getSizeVectorOrder(This->allOrders);
289 for (uint i = 0; i < size; i++) {
290 Order *order = getVectorOrder(This->allOrders, i);
291 OrderGraph *graph = buildOrderGraph(order);
292 if (order->type == PARTIAL) {
293 //Required to do SCC analysis for partial order graphs. It
294 //makes sure we don't incorrectly optimize graphs with negative
296 completePartialOrderGraph(graph);
299 //This analysis is completely optional
300 reachMustAnalysis(graph);
302 //This pair of analysis is also optional
303 if (order->type == PARTIAL) {
304 localMustAnalysisPartial(graph);
306 localMustAnalysisTotal(graph);
309 //This optimization is completely optional
310 removeMustBeTrueNodes(graph);
312 //This is needed for splitorder
313 computeStronglyConnectedComponentGraph(graph);
315 decomposeOrder(order, graph);
317 deleteOrderGraph(graph);