1 #include "orderencoder.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 void DFS(OrderGraph *graph, Vector<OrderNode *> *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 finishNodes->push(node);
23 deleteIterOrderNode(iterator);
26 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
27 uint size = finishNodes->getSize();
29 for (int i = size - 1; i >= 0; i--) {
30 OrderNode *node = finishNodes->get(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, Vector<OrderNode *> *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 finishNodes->push(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 Vector<OrderNode *> finishNodes;
77 DFS(graph, &finishNodes);
78 resetNodeInfoStatusSCC(graph);
79 DFSReverse(graph, &finishNodes);
80 resetNodeInfoStatusSCC(graph);
83 bool isMustBeTrueNode(OrderNode* node){
84 HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges);
85 while(hasNextOrderEdge(iterator)){
86 OrderEdge* edge = nextOrderEdge(iterator);
90 deleteIterOrderEdge(iterator);
91 iterator = iteratorOrderEdge(node->outEdges);
92 while(hasNextOrderEdge(iterator)){
93 OrderEdge* edge = nextOrderEdge(iterator);
97 deleteIterOrderEdge(iterator);
101 void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
102 HSIteratorOrderEdge* iterin = iteratorOrderEdge(node->inEdges);
103 while(hasNextOrderEdge(iterin)){
104 OrderEdge* inEdge = nextOrderEdge(iterin);
105 OrderNode* srcNode = inEdge->source;
106 removeHashSetOrderEdge(srcNode->outEdges, inEdge);
107 HSIteratorOrderEdge* iterout = iteratorOrderEdge(node->outEdges);
108 while(hasNextOrderEdge(iterout)){
109 OrderEdge* outEdge = nextOrderEdge(iterout);
110 OrderNode* sinkNode = outEdge->sink;
111 removeHashSetOrderEdge(sinkNode->inEdges, outEdge);
112 //Adding new edge to new sink and src nodes ...
113 OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
114 newEdge->mustPos = true;
115 newEdge->polPos = true;
116 if (newEdge->mustNeg)
118 addHashSetOrderEdge(srcNode->outEdges, newEdge);
119 addHashSetOrderEdge(sinkNode->inEdges, newEdge);
121 deleteIterOrderEdge(iterout);
123 deleteIterOrderEdge(iterin);
126 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
127 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
128 while(hasNextOrderNode(iterator)){
129 OrderNode* node = nextOrderNode(iterator);
130 if(isMustBeTrueNode(node)){
131 bypassMustBeTrueNode(This,graph, node);
134 deleteIterOrderNode(iterator);
137 /** This function computes a source set for every nodes, the set of
138 nodes that can reach that node via pospolarity edges. It then
139 looks for negative polarity edges from nodes in the the source set
140 to determine whether we need to generate pseudoPos edges. */
142 void completePartialOrderGraph(OrderGraph *graph) {
143 Vector<OrderNode *> finishNodes;
144 DFS(graph, &finishNodes);
145 resetNodeInfoStatusSCC(graph);
146 HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
148 Vector<OrderNode *> sccNodes;
150 uint size = finishNodes.getSize();
152 for (int i = size - 1; i >= 0; i--) {
153 OrderNode *node = finishNodes.get(i);
154 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
155 putNodeToNodeSet(table, node, sources);
157 if (node->status == NOTVISITED) {
158 //Need to do reverse traversal here...
159 node->status = VISITED;
160 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
161 node->status = FINISHED;
162 node->sccNum = sccNum;
166 //Compute in set for entire SCC
167 uint rSize = sccNodes.getSize();
168 for (uint j = 0; j < rSize; j++) {
169 OrderNode *rnode = sccNodes.get(j);
170 //Compute source sets
171 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
172 while (hasNextOrderEdge(iterator)) {
173 OrderEdge *edge = nextOrderEdge(iterator);
174 OrderNode *parent = edge->source;
176 addHashSetOrderNode(sources, parent);
177 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
178 addAllHashSetOrderNode(sources, parent_srcs);
181 deleteIterOrderEdge(iterator);
183 for (uint j=0; j < rSize; j++) {
184 //Copy in set of entire SCC
185 OrderNode *rnode = sccNodes.get(j);
186 HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
187 putNodeToNodeSet(table, rnode, set);
189 //Use source sets to compute pseudoPos edges
190 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
191 while (hasNextOrderEdge(iterator)) {
192 OrderEdge *edge = nextOrderEdge(iterator);
193 OrderNode *parent = edge->source;
194 ASSERT(parent != rnode);
195 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
196 containsHashSetOrderNode(sources, parent)) {
197 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
198 newedge->pseudoPos = true;
201 deleteIterOrderEdge(iterator);
208 resetAndDeleteHashTableNodeToNodeSet(table);
209 deleteHashTableNodeToNodeSet(table);
210 resetNodeInfoStatusSCC(graph);
213 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
214 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
215 while (hasNextOrderNode(iterator)) {
216 OrderNode *node = nextOrderNode(iterator);
217 if (node->status == NOTVISITED) {
218 node->status = VISITED;
219 DFSNodeVisit(node, finishNodes, false, true, 0);
220 node->status = FINISHED;
221 finishNodes->push(node);
224 deleteIterOrderNode(iterator);
227 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
228 uint size = finishNodes->getSize();
229 HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
231 for (int i = size - 1; i >= 0; i--) {
232 OrderNode *node = finishNodes->get(i);
233 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
234 putNodeToNodeSet(table, node, sources);
237 //Compute source sets
238 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
239 while (hasNextOrderEdge(iterator)) {
240 OrderEdge *edge = nextOrderEdge(iterator);
241 OrderNode *parent = edge->source;
243 addHashSetOrderNode(sources, parent);
244 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
245 addAllHashSetOrderNode(sources, parent_srcs);
248 deleteIterOrderEdge(iterator);
250 if (computeTransitiveClosure) {
251 //Compute full transitive closure for nodes
252 HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
253 while (hasNextOrderNode(srciterator)) {
254 OrderNode *srcnode = nextOrderNode(srciterator);
255 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
256 newedge->mustPos = true;
257 newedge->polPos = true;
258 if (newedge->mustNeg)
259 solver->unsat = true;
260 addHashSetOrderEdge(srcnode->outEdges,newedge);
261 addHashSetOrderEdge(node->inEdges,newedge);
263 deleteIterOrderNode(srciterator);
266 //Use source sets to compute mustPos edges
267 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
268 while (hasNextOrderEdge(iterator)) {
269 OrderEdge *edge = nextOrderEdge(iterator);
270 OrderNode *parent = edge->source;
271 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
272 edge->mustPos = true;
275 solver->unsat = true;
278 deleteIterOrderEdge(iterator);
281 //Use source sets to compute mustNeg for edges that would introduce cycle if true
282 HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
283 while (hasNextOrderEdge(iterator)) {
284 OrderEdge *edge = nextOrderEdge(iterator);
285 OrderNode *child = edge->sink;
286 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
287 edge->mustNeg = true;
290 solver->unsat = true;
293 deleteIterOrderEdge(iterator);
297 resetAndDeleteHashTableNodeToNodeSet(table);
298 deleteHashTableNodeToNodeSet(table);
301 /* This function finds edges that would form a cycle with must edges
302 and forces them to be mustNeg. It also decides whether an edge
303 must be true because of transitivity from other must be true
306 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
307 Vector<OrderNode *> finishNodes;
308 //Topologically sort the mustPos edge graph
309 DFSMust(graph, &finishNodes);
310 resetNodeInfoStatusSCC(graph);
312 //Find any backwards edges that complete cycles and force them to be mustNeg
313 DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
316 /* This function finds edges that must be positive and forces the
317 inverse edge to be negative (and clears its positive polarity if it
320 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
321 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
322 while (hasNextOrderEdge(iterator)) {
323 OrderEdge *edge = nextOrderEdge(iterator);
325 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
326 if (invEdge != NULL) {
327 if (!invEdge->mustPos) {
328 invEdge->polPos = false;
330 solver->unsat = true;
332 invEdge->mustNeg = true;
333 invEdge->polNeg = true;
337 deleteIterOrderEdge(iterator);
340 /** This finds edges that must be positive and forces the inverse edge
341 to be negative. It also clears the negative flag of this edge.
342 It also finds edges that must be negative and clears the positive
345 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
346 HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
347 while (hasNextOrderEdge(iterator)) {
348 OrderEdge *edge = nextOrderEdge(iterator);
350 if (!edge->mustNeg) {
351 edge->polNeg = false;
353 solver->unsat = true;
355 OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
356 if (invEdge != NULL) {
357 if (!invEdge->mustPos)
358 invEdge->polPos = false;
360 solver->unsat = true;
361 invEdge->mustNeg = true;
362 invEdge->polNeg = true;
365 if (edge->mustNeg && !edge->mustPos) {
366 edge->polPos = false;
369 deleteIterOrderEdge(iterator);
372 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
373 Vector<Order *> ordervec;
374 Vector<Order *> partialcandidatevec;
375 uint size = order->constraints.getSize();
376 for (uint i = 0; i < size; i++) {
377 BooleanOrder *orderconstraint = order->constraints.get(i);
378 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
379 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
380 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
381 if (from->sccNum != to->sccNum) {
382 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
384 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
385 } else if (edge->polNeg) {
386 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
388 //This case should only be possible if constraint isn't in AST
392 //Build new order and change constraint's order
393 Order *neworder = NULL;
394 if (ordervec.getSize() > from->sccNum)
395 neworder = ordervec.get(from->sccNum);
396 if (neworder == NULL) {
397 MutableSet *set = new MutableSet(order->set->type);
398 neworder = new Order(order->type, set);
399 This->allOrders.push(neworder);
400 ordervec.setExpand(from->sccNum, neworder);
401 if (order->type == PARTIAL)
402 partialcandidatevec.setExpand(from->sccNum, neworder);
404 partialcandidatevec.setExpand(from->sccNum, NULL);
406 if (from->status != ADDEDTOSET) {
407 from->status = ADDEDTOSET;
408 ((MutableSet *)neworder->set)->addElementMSet(from->id);
410 if (to->status != ADDEDTOSET) {
411 to->status = ADDEDTOSET;
412 ((MutableSet *)neworder->set)->addElementMSet(to->id);
414 if (order->type == PARTIAL) {
415 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
417 partialcandidatevec.setExpand(from->sccNum, NULL);
419 orderconstraint->order = neworder;
420 neworder->addOrderConstraint(orderconstraint);
424 uint pcvsize=partialcandidatevec.getSize();
425 for(uint i=0;i<pcvsize;i++) {
426 Order * neworder=partialcandidatevec.get(i);
427 if (neworder != NULL){
428 neworder->type = TOTAL;
429 model_print("i=%u\t", i);
434 void orderAnalysis(CSolver *This) {
435 uint size = This->allOrders.getSize();
436 for (uint i = 0; i < size; i++) {
437 Order *order = This->allOrders.get(i);
438 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
442 OrderGraph *graph = buildOrderGraph(order);
443 if (order->type == PARTIAL) {
444 //Required to do SCC analysis for partial order graphs. It
445 //makes sure we don't incorrectly optimize graphs with negative
447 completePartialOrderGraph(graph);
451 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
454 reachMustAnalysis(This, graph, false);
456 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
458 if (mustReachLocal) {
459 //This pair of analysis is also optional
460 if (order->type == PARTIAL) {
461 localMustAnalysisPartial(This, graph);
463 localMustAnalysisTotal(This, graph);
467 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
470 removeMustBeTrueNodes(This, graph);
472 //This is needed for splitorder
473 computeStronglyConnectedComponentGraph(graph);
475 decomposeOrder(This, order, graph);
477 deleteOrderGraph(graph);