1 #include "orderdecompose.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 #include "orderencoder.h"
15 void orderAnalysis(CSolver *This) {
16 uint size = This->allOrders.getSize();
17 for (uint i = 0; i < size; i++) {
18 Order *order = This->allOrders.get(i);
19 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
23 OrderGraph *graph = buildOrderGraph(order);
24 if (order->type == PARTIAL) {
25 //Required to do SCC analysis for partial order graphs. It
26 //makes sure we don't incorrectly optimize graphs with negative
28 completePartialOrderGraph(graph);
32 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
35 reachMustAnalysis(This, graph, false);
37 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
40 //This pair of analysis is also optional
41 if (order->type == PARTIAL) {
42 localMustAnalysisPartial(This, graph);
44 localMustAnalysisTotal(This, graph);
48 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
51 removeMustBeTrueNodes(This, graph);
53 //This is needed for splitorder
54 computeStronglyConnectedComponentGraph(graph);
56 decomposeOrder(This, order, graph);
58 deleteOrderGraph(graph);
62 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
63 Vector<Order *> ordervec;
64 Vector<Order *> partialcandidatevec;
65 uint size = order->constraints.getSize();
66 for (uint i = 0; i < size; i++) {
67 BooleanOrder *orderconstraint = order->constraints.get(i);
68 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
69 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
70 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
71 if (from->sccNum != to->sccNum) {
72 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
74 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
75 } else if (edge->polNeg) {
76 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
78 //This case should only be possible if constraint isn't in AST
82 //Build new order and change constraint's order
83 Order *neworder = NULL;
84 if (ordervec.getSize() > from->sccNum)
85 neworder = ordervec.get(from->sccNum);
86 if (neworder == NULL) {
87 MutableSet *set = new MutableSet(order->set->type);
88 This->allSets.push(set);
89 neworder = new Order(order->type, set);
90 This->allOrders.push(neworder);
91 ordervec.setExpand(from->sccNum, neworder);
92 if (order->type == PARTIAL)
93 partialcandidatevec.setExpand(from->sccNum, neworder);
95 partialcandidatevec.setExpand(from->sccNum, NULL);
97 if (from->status != ADDEDTOSET) {
98 from->status = ADDEDTOSET;
99 ((MutableSet *)neworder->set)->addElementMSet(from->id);
101 if (to->status != ADDEDTOSET) {
102 to->status = ADDEDTOSET;
103 ((MutableSet *)neworder->set)->addElementMSet(to->id);
105 if (order->type == PARTIAL) {
106 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
108 partialcandidatevec.setExpand(from->sccNum, NULL);
110 orderconstraint->order = neworder;
111 neworder->addOrderConstraint(orderconstraint);
115 uint pcvsize=partialcandidatevec.getSize();
116 for(uint i=0;i<pcvsize;i++) {
117 Order * neworder=partialcandidatevec.get(i);
118 if (neworder != NULL){
119 neworder->type = TOTAL;
120 model_print("i=%u\t", i);