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