src/ASTTransform/transformer.cc

   1 #include "transformer.h"
   2 #include "common.h"
   3 #include "order.h"
   4 #include "boolean.h"
   5 #include "ordergraph.h"
   6 #include "ordernode.h"
   7 #include "rewriter.h"
   8 #include "orderedge.h"
   9 #include "mutableset.h"
  10 #include "ops.h"
  11 #include "csolver.h"
  12 #include "orderanalysis.h"
  13 #include "tunable.h"
  14 #include "transform.h"
  15 #include "element.h"
  16 #include "integerencoding.h"
  17 #include "decomposeordertransform.h"
  18
  19 Transformer::Transformer(CSolver *_solver):
  20         integerEncoding(new IntegerEncodingTransform(_solver)),
  21         decomposeOrder(new DecomposeOrderTransform(_solver)),
  22         solver(_solver)
  23 {
  24 }
  25
  26 Transformer::~Transformer(){
  27         delete integerEncoding;
  28         delete decomposeOrder;
  29 }
  30
  31 void Transformer::orderAnalysis() {
  32         Vector<Order *> *orders = solver->getOrders();
  33         uint size = orders->getSize();
  34         for (uint i = 0; i < size; i++) {
  35                 Order *order = orders->get(i);
  36                 decomposeOrder->setCurrentOrder(order);
  37                 if (!decomposeOrder->canExecuteTransform()){
  38                         continue;
  39                 }
  40
  41                 OrderGraph *graph = buildOrderGraph(order);
  42                 if (order->type == SATC_PARTIAL) {
  43                         //Required to do SCC analysis for partial order graphs.  It
  44                         //makes sure we don't incorrectly optimize graphs with negative
  45                         //polarity edges
  46                         completePartialOrderGraph(graph);
  47                 }
  48
  49
  50                 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
  51
  52                 if (mustReachGlobal)
  53                         reachMustAnalysis(solver, graph, false);
  54
  55                 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
  56
  57                 if (mustReachLocal) {
  58                         //This pair of analysis is also optional
  59                         if (order->type == SATC_PARTIAL) {
  60                                 localMustAnalysisPartial(solver, graph);
  61                         } else {
  62                                 localMustAnalysisTotal(solver, graph);
  63                         }
  64                 }
  65
  66                 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
  67
  68                 if (mustReachPrune)
  69                         removeMustBeTrueNodes(solver, graph);
  70
  71                 //This is needed for splitorder
  72                 computeStronglyConnectedComponentGraph(graph);
  73                 decomposeOrder->setOrderGraph(graph);
  74                 decomposeOrder->doTransform();
  75                 delete graph;
  76
  77                 integerEncoding->setCurrentOrder(order);
  78                 if(!integerEncoding->canExecuteTransform()){
  79                         continue;
  80                 }
  81                 integerEncoding->doTransform();
  82         }
  83 }
  84
  85