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 "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                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
  83                 if (from->sccNum != to->sccNum) {
  84                         OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
  85                         if (edge->polPos) {
  86                                 This->replaceBooleanWithTrue(orderconstraint);
  87                         } else if (edge->polNeg) {
  88                                 This->replaceBooleanWithFalse(orderconstraint);
  89                         } else {
  90                                 //This case should only be possible if constraint isn't in AST
  91                                 ASSERT(0);
  92                         }
  93                 } else {
  94                         //Build new order and change constraint's order
  95                         Order *neworder = NULL;
  96                         if (ordervec.getSize() > from->sccNum)
  97                                 neworder = ordervec.get(from->sccNum);
  98                         if (neworder == NULL) {
  99                                 MutableSet *set = This->createMutableSet(order->set->type);
 100                                 neworder = This->createOrder(order->type, set);
 101                                 ordervec.setExpand(from->sccNum, neworder);
 102                                 if (order->type == PARTIAL)
 103                                         partialcandidatevec.setExpand(from->sccNum, neworder);
 104                                 else
 105                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 106                         }
 107                         if (from->status != ADDEDTOSET) {
 108                                 from->status = ADDEDTOSET;
 109                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 110                         }
 111                         if (to->status != ADDEDTOSET) {
 112                                 to->status = ADDEDTOSET;
 113                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 114                         }
 115                         if (order->type == PARTIAL) {
 116                                 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
 117                                 if (edge->polNeg)
 118                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 119                         }
 120                         orderconstraint->order = neworder;
 121                         neworder->addOrderConstraint(orderconstraint);
 122                 }
 123         }
 124
 125         uint pcvsize = partialcandidatevec.getSize();
 126         for (uint i = 0; i < pcvsize; i++) {
 127                 Order *neworder = partialcandidatevec.get(i);
 128                 if (neworder != NULL) {
 129                         neworder->type = TOTAL;
 130                         model_print("i=%u\t", i);
 131                 }
 132         }
 133 }
 134