5 #include "ordergraph.h"
9 #include "mutableset.h"
12 #include "orderencoder.h"
14 #include "transform.h"
16 #include "integerencoding.h"
17 #include "decomposeordertransform.h"
19 void orderAnalysis(CSolver *This) {
20 Vector<Order *> *orders = This->getOrders();
21 uint size = orders->getSize();
22 for (uint i = 0; i < size; i++) {
23 Order *order = orders->get(i);
24 DecomposeOrderTransform* decompose = new DecomposeOrderTransform(This, order, DECOMPOSEORDER, &onoff);
25 if (!decompose->canExecuteTransform())
28 OrderGraph *graph = buildOrderGraph(order);
29 if (order->type == PARTIAL) {
30 //Required to do SCC analysis for partial order graphs. It
31 //makes sure we don't incorrectly optimize graphs with negative
33 completePartialOrderGraph(graph);
37 bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
40 reachMustAnalysis(This, graph, false);
42 bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
45 //This pair of analysis is also optional
46 if (order->type == PARTIAL) {
47 localMustAnalysisPartial(This, graph);
49 localMustAnalysisTotal(This, graph);
53 bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
56 removeMustBeTrueNodes(This, graph);
58 //This is needed for splitorder
59 computeStronglyConnectedComponentGraph(graph);
60 decompose->setOrderGraph(graph);
61 decompose->doTransform();
66 IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order, ORDERINTEGERENCODING, &offon);
67 if(!integerEncoding->canExecuteTransform())
69 integerEncoding->doTransform();
70 delete integerEncoding;