src/ASTTransform/decomposeordertransform.cc

   1 /*
   2  * File:   ordertransform.cc
   3  * Author: hamed
   4  *
   5  * Created on August 28, 2017, 10:35 AM
   6  */
   7
   8 #include "decomposeordertransform.h"
   9 #include "order.h"
  10 #include "orderedge.h"
  11 #include "ordernode.h"
  12 #include "boolean.h"
  13 #include "mutableset.h"
  14 #include "ordergraph.h"
  15 #include "csolver.h"
  16 #include "decomposeorderresolver.h"
  17 #include "tunable.h"
  18 #include "orderanalysis.h"
  19
  20
  21 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
  22         : Transform(_solver)
  23 {
  24 }
  25
  26 DecomposeOrderTransform::~DecomposeOrderTransform() {
  27 }
  28
  29 void DecomposeOrderTransform::doTransform() {
  30         HashsetOrder *orders = solver->getActiveOrders()->copy();
  31         SetIteratorOrder * orderit=orders->iterator();
  32         while(orderit->hasNext()) {
  33                 Order *order = orderit->next();
  34
  35                 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
  36                         continue;
  37                 }
  38
  39                 OrderGraph *graph = buildOrderGraph(order);
  40                 if (order->type == SATC_PARTIAL) {
  41                         //Required to do SCC analysis for partial order graphs.  It
  42                         //makes sure we don't incorrectly optimize graphs with negative
  43                         //polarity edges
  44                         completePartialOrderGraph(graph);
  45                 }
  46
  47                 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
  48
  49                 if (mustReachGlobal)
  50                         reachMustAnalysis(solver, graph, false);
  51
  52                 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
  53
  54                 if (mustReachLocal) {
  55                         //This pair of analysis is also optional
  56                         if (order->type == SATC_PARTIAL) {
  57                                 localMustAnalysisPartial(solver, graph);
  58                         } else {
  59                                 localMustAnalysisTotal(solver, graph);
  60                         }
  61                 }
  62
  63
  64                 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
  65
  66                 if (mustReachPrune)
  67                         removeMustBeTrueNodes(solver, graph);
  68
  69                 //This is needed for splitorder
  70                 computeStronglyConnectedComponentGraph(graph);
  71                 decomposeOrder(order, graph);
  72         }
  73         delete orderit;
  74         delete orders;
  75 }
  76
  77
  78 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
  79         Vector<Order *> ordervec;
  80         Vector<Order *> partialcandidatevec;
  81         uint size = currOrder->constraints.getSize();
  82         for (uint i = 0; i < size; i++) {
  83                 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
  84                 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
  85                 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
  86                 if (from->sccNum != to->sccNum) {
  87                         OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
  88                         if (edge != NULL) {
  89                                 if (edge->polPos) {
  90                                         solver->replaceBooleanWithTrue(orderconstraint);
  91                                 } else if (edge->polNeg) {
  92                                         solver->replaceBooleanWithFalse(orderconstraint);
  93                                 } else {
  94                                         //This case should only be possible if constraint isn't in AST
  95                                         //This can happen, so don't do anything
  96                                         ;
  97                                 }
  98                         } else {
  99                                 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
 100                                 if (invedge != NULL) {
 101                                         if (invedge->polPos) {
 102                                                 solver->replaceBooleanWithFalse(orderconstraint);
 103                                         } else if (edge->polNeg) {
 104                                                 //This case shouldn't happen...  If we have a partial order,
 105                                                 //then we should have our own edge...If we have a total
 106                                                 //order, then this edge should be positive...
 107                                                 ASSERT(0);
 108                                         } else {
 109                                                 //This case should only be possible if constraint isn't in AST
 110                                                 //This can happen, so don't do anything
 111                                                 ;
 112                                         }
 113                                 }
 114                         }
 115                 } else {
 116                         //Build new order and change constraint's order
 117                         Order *neworder = NULL;
 118                         if (ordervec.getSize() > from->sccNum)
 119                                 neworder = ordervec.get(from->sccNum);
 120                         if (neworder == NULL) {
 121                                 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
 122                                 neworder = solver->createOrder(currOrder->type, set);
 123                                 ordervec.setExpand(from->sccNum, neworder);
 124                                 if (currOrder->type == SATC_PARTIAL)
 125                                         partialcandidatevec.setExpand(from->sccNum, neworder);
 126                                 else
 127                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 128                         }
 129                         if (from->status != ADDEDTOSET) {
 130                                 from->status = ADDEDTOSET;
 131                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 132                         }
 133                         if (to->status != ADDEDTOSET) {
 134                                 to->status = ADDEDTOSET;
 135                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 136                         }
 137                         if (currOrder->type == SATC_PARTIAL) {
 138                                 OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
 139                                 if (edge->polNeg)
 140                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 141                         }
 142                         orderconstraint->order = neworder;
 143                         neworder->addOrderConstraint(orderconstraint);
 144                 }
 145         }
 146         currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
 147         solver->getActiveOrders()->remove(currOrder);
 148         uint pcvsize = partialcandidatevec.getSize();
 149         for (uint i = 0; i < pcvsize; i++) {
 150                 Order *neworder = partialcandidatevec.get(i);
 151                 if (neworder != NULL) {
 152                         neworder->type = SATC_TOTAL;
 153                 }
 154         }
 155 }