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