1 #include "orderdecompose.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 #include "orderanalysis.h"
14 #include "integerencoding.h"
16 void orderAnalysis(CSolver *This) {
17 Vector<Order *> *orders = This->getOrders();
18 uint size = orders->getSize();
19 for (uint i = 0; i < size; i++) {
20 Order *order = orders->get(i);
21 bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
25 OrderGraph *graph = buildOrderGraph(order);
26 if (order->type == PARTIAL) {
27 //Required to do SCC analysis for partial order graphs. It
28 //makes sure we don't incorrectly optimize graphs with negative
30 completePartialOrderGraph(graph);
34 bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
37 reachMustAnalysis(This, graph, false);
39 bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
42 //This pair of analysis is also optional
43 if (order->type == PARTIAL) {
44 localMustAnalysisPartial(This, graph);
46 localMustAnalysisTotal(This, graph);
50 bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
53 removeMustBeTrueNodes(This, graph);
55 //This is needed for splitorder
56 computeStronglyConnectedComponentGraph(graph);
57 decomposeOrder(This, order, graph);
61 OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
63 bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
64 if(!doIntegerEncoding)
66 uint size = order->constraints.getSize();
67 for(uint i=0; i<size; i++){
68 orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
74 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
75 Vector<Order *> ordervec;
76 Vector<Order *> partialcandidatevec;
77 uint size = order->constraints.getSize();
78 for (uint i = 0; i < size; i++) {
79 BooleanOrder *orderconstraint = order->constraints.get(i);
80 OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
81 OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
82 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
83 if (from->sccNum != to->sccNum) {
84 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
86 This->replaceBooleanWithTrue(orderconstraint);
87 } else if (edge->polNeg) {
88 This->replaceBooleanWithFalse(orderconstraint);
90 //This case should only be possible if constraint isn't in AST
94 //Build new order and change constraint's order
95 Order *neworder = NULL;
96 if (ordervec.getSize() > from->sccNum)
97 neworder = ordervec.get(from->sccNum);
98 if (neworder == NULL) {
99 MutableSet *set = This->createMutableSet(order->set->type);
100 neworder = This->createOrder(order->type, set);
101 ordervec.setExpand(from->sccNum, neworder);
102 if (order->type == PARTIAL)
103 partialcandidatevec.setExpand(from->sccNum, neworder);
105 partialcandidatevec.setExpand(from->sccNum, NULL);
107 if (from->status != ADDEDTOSET) {
108 from->status = ADDEDTOSET;
109 ((MutableSet *)neworder->set)->addElementMSet(from->id);
111 if (to->status != ADDEDTOSET) {
112 to->status = ADDEDTOSET;
113 ((MutableSet *)neworder->set)->addElementMSet(to->id);
115 if (order->type == PARTIAL) {
116 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
118 partialcandidatevec.setExpand(from->sccNum, NULL);
120 orderconstraint->order = neworder;
121 neworder->addOrderConstraint(orderconstraint);
125 uint pcvsize = partialcandidatevec.getSize();
126 for (uint i = 0; i < pcvsize; i++) {
127 Order *neworder = partialcandidatevec.get(i);
128 if (neworder != NULL) {
129 neworder->type = TOTAL;
130 model_print("i=%u\t", i);