src/ASTTransform/orderdecompose.cc

   1 #include "orderdecompose.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 "integerencoding.h"
  15
  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);
  22                 if (!doDecompose)
  23                         continue;
  24
  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
  29                         //polarity edges
  30                         completePartialOrderGraph(graph);
  31                 }
  32
  33
  34                 bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
  35
  36                 if (mustReachGlobal)
  37                         reachMustAnalysis(This, graph, false);
  38
  39                 bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
  40
  41                 if (mustReachLocal) {
  42                         //This pair of analysis is also optional
  43                         if (order->type == PARTIAL) {
  44                                 localMustAnalysisPartial(This, graph);
  45                         } else {
  46                                 localMustAnalysisTotal(This, graph);
  47                         }
  48                 }
  49
  50                 bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
  51
  52                 if (mustReachPrune)
  53                         removeMustBeTrueNodes(This, graph);
  54
  55                 //This is needed for splitorder
  56                 computeStronglyConnectedComponentGraph(graph);
  57                 decomposeOrder(This, order, graph);
  58                 delete graph;
  59
  60                 /*
  61                    OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
  62
  63                    bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
  64                    if(!doIntegerEncoding)
  65                    continue;
  66                    uint size = order->constraints.getSize();
  67                    for(uint i=0; i<size; i++){
  68                    orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
  69                    }*/
  70
  71         }
  72 }
  73
  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);
  84                         if (edge->polPos) {
  85                                 This->replaceBooleanWithTrue(orderconstraint);
  86                         } else if (edge->polNeg) {
  87                                 This->replaceBooleanWithFalse(orderconstraint);
  88                         } else {
  89                                 //This case should only be possible if constraint isn't in AST
  90                                 ASSERT(0);
  91                         }
  92                 } else {
  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);
 103                                 else
 104                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 105                         }
 106                         if (from->status != ADDEDTOSET) {
 107                                 from->status = ADDEDTOSET;
 108                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 109                         }
 110                         if (to->status != ADDEDTOSET) {
 111                                 to->status = ADDEDTOSET;
 112                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 113                         }
 114                         if (order->type == PARTIAL) {
 115                                 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
 116                                 if (edge->polNeg)
 117                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 118                         }
 119                         orderconstraint->order = neworder;
 120                         neworder->addOrderConstraint(orderconstraint);
 121                 }
 122         }
 123
 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);
 130                 }
 131         }
 132 }
 133