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 "orderencoder.h"
  13 #include "tunable.h"
  14
  15 void orderAnalysis(CSolver *This) {
  16         uint size = This->allOrders.getSize();
  17         for (uint i = 0; i < size; i++) {
  18                 Order *order = This->allOrders.get(i);
  19                 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
  20                 if (!doDecompose)
  21                         continue;
  22
  23                 OrderGraph *graph = buildOrderGraph(order);
  24                 if (order->type == PARTIAL) {
  25                         //Required to do SCC analysis for partial order graphs.  It
  26                         //makes sure we don't incorrectly optimize graphs with negative
  27                         //polarity edges
  28                         completePartialOrderGraph(graph);
  29                 }
  30
  31
  32                 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
  33
  34                 if (mustReachGlobal)
  35                         reachMustAnalysis(This, graph, false);
  36
  37                 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
  38
  39                 if (mustReachLocal) {
  40                         //This pair of analysis is also optional
  41                         if (order->type == PARTIAL) {
  42                                 localMustAnalysisPartial(This, graph);
  43                         } else {
  44                                 localMustAnalysisTotal(This, graph);
  45                         }
  46                 }
  47
  48                 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
  49
  50                 if (mustReachPrune)
  51                         removeMustBeTrueNodes(This, graph);
  52
  53                 //This is needed for splitorder
  54                 computeStronglyConnectedComponentGraph(graph);
  55
  56                 decomposeOrder(This, order, graph);
  57
  58                 deleteOrderGraph(graph);
  59         }
  60 }
  61
  62 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
  63         Vector<Order *> ordervec;
  64         Vector<Order *> partialcandidatevec;
  65         uint size = order->constraints.getSize();
  66         for (uint i = 0; i < size; i++) {
  67                 BooleanOrder *orderconstraint = order->constraints.get(i);
  68                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
  69                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
  70                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
  71                 if (from->sccNum != to->sccNum) {
  72                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
  73                         if (edge->polPos) {
  74                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
  75                         } else if (edge->polNeg) {
  76                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
  77                         } else {
  78                                 //This case should only be possible if constraint isn't in AST
  79                                 ASSERT(0);
  80                         }
  81                 } else {
  82                         //Build new order and change constraint's order
  83                         Order *neworder = NULL;
  84                         if (ordervec.getSize() > from->sccNum)
  85                                 neworder = ordervec.get(from->sccNum);
  86                         if (neworder == NULL) {
  87                                 MutableSet *set = new MutableSet(order->set->type);
  88                                 This->allSets.push(set);
  89                                 neworder = new Order(order->type, set);
  90                                 This->allOrders.push(neworder);
  91                                 ordervec.setExpand(from->sccNum, neworder);
  92                                 if (order->type == PARTIAL)
  93                                         partialcandidatevec.setExpand(from->sccNum, neworder);
  94                                 else
  95                                         partialcandidatevec.setExpand(from->sccNum, NULL);
  96                         }
  97                         if (from->status != ADDEDTOSET) {
  98                                 from->status = ADDEDTOSET;
  99                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 100                         }
 101                         if (to->status != ADDEDTOSET) {
 102                                 to->status = ADDEDTOSET;
 103                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 104                         }
 105                         if (order->type == PARTIAL) {
 106                                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 107                                 if (edge->polNeg)
 108                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 109                         }
 110                         orderconstraint->order = neworder;
 111                         neworder->addOrderConstraint(orderconstraint);
 112                 }
 113         }
 114
 115         uint pcvsize=partialcandidatevec.getSize();
 116         for(uint i=0;i<pcvsize;i++) {
 117                 Order * neworder=partialcandidatevec.get(i);
 118                 if (neworder != NULL){
 119                         neworder->type = TOTAL;
 120                         model_print("i=%u\t", i);
 121                 }
 122         }
 123 }
 124