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 if (from->sccNum != to->sccNum) {
83 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
85 This->replaceBooleanWithTrue(orderconstraint);
86 } else if (edge->polNeg) {
87 This->replaceBooleanWithFalse(orderconstraint);
89 //This case should only be possible if constraint isn't in AST
93 //Build new order and change constraint's order
94 Order *neworder = NULL;
95 if (ordervec.getSize() > from->sccNum)
96 neworder = ordervec.get(from->sccNum);
97 if (neworder == NULL) {
98 MutableSet *set = This->createMutableSet(order->set->type);
99 neworder = This->createOrder(order->type, set);
100 ordervec.setExpand(from->sccNum, neworder);
101 if (order->type == PARTIAL)
102 partialcandidatevec.setExpand(from->sccNum, neworder);
104 partialcandidatevec.setExpand(from->sccNum, NULL);
106 if (from->status != ADDEDTOSET) {
107 from->status = ADDEDTOSET;
108 ((MutableSet *)neworder->set)->addElementMSet(from->id);
110 if (to->status != ADDEDTOSET) {
111 to->status = ADDEDTOSET;
112 ((MutableSet *)neworder->set)->addElementMSet(to->id);
114 if (order->type == PARTIAL) {
115 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
117 partialcandidatevec.setExpand(from->sccNum, NULL);
119 orderconstraint->order = neworder;
120 neworder->addOrderConstraint(orderconstraint);
124 uint pcvsize = partialcandidatevec.getSize();
125 for (uint i = 0; i < pcvsize; i++) {
126 Order *neworder = partialcandidatevec.get(i);
127 if (neworder != NULL) {
128 neworder->type = TOTAL;
129 model_print("i=%u\t", i);