1 #include "transformer.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 #include "orderanalysis.h"
14 #include "transform.h"
16 #include "integerencoding.h"
17 #include "decomposeordertransform.h"
19 Transformer::Transformer(CSolver *_solver):
20 integerEncoding(new IntegerEncodingTransform(_solver)),
25 Transformer::~Transformer(){
26 delete integerEncoding;
29 void Transformer::orderAnalysis() {
30 Vector<Order *> *orders = solver->getOrders();
31 uint size = orders->getSize();
32 for (uint i = 0; i < size; i++) {
33 Order *order = orders->get(i);
34 DecomposeOrderTransform* decompose = new DecomposeOrderTransform(solver, order);
35 if (!decompose->canExecuteTransform()){
40 OrderGraph *graph = buildOrderGraph(order);
41 if (order->type == SATC_PARTIAL) {
42 //Required to do SCC analysis for partial order graphs. It
43 //makes sure we don't incorrectly optimize graphs with negative
45 completePartialOrderGraph(graph);
49 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
52 reachMustAnalysis(solver, graph, false);
54 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
57 //This pair of analysis is also optional
58 if (order->type == SATC_PARTIAL) {
59 localMustAnalysisPartial(solver, graph);
61 localMustAnalysisTotal(solver, graph);
65 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
68 removeMustBeTrueNodes(solver, graph);
70 //This is needed for splitorder
71 computeStronglyConnectedComponentGraph(graph);
72 decompose->setOrderGraph(graph);
73 decompose->doTransform();
77 integerEncoding->setCurrentOrder(order);
78 if(!integerEncoding->canExecuteTransform()){
81 integerEncoding->doTransform();