src/ASTTransform/decomposeordertransform.cc

   1 /*
   2  * File:   ordertransform.cc
   3  * Author: hamed
   4  *
   5  * Created on August 28, 2017, 10:35 AM
   6  */
   7
   8 #include "decomposeordertransform.h"
   9 #include "order.h"
  10 #include "orderedge.h"
  11 #include "ordernode.h"
  12 #include "boolean.h"
  13 #include "mutableset.h"
  14 #include "ordergraph.h"
  15 #include "csolver.h"
  16 #include "decomposeorderresolver.h"
  17 #include "tunable.h"
  18 #include "orderanalysis.h"
  19
  20
  21 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
  22         : Transform(_solver)
  23 {
  24 }
  25
  26 DecomposeOrderTransform::~DecomposeOrderTransform() {
  27 }
  28
  29 void DecomposeOrderTransform::doTransform() {
  30         HashsetOrder *orders = solver->getActiveOrders()->copy();
  31         SetIteratorOrder *orderit = orders->iterator();
  32         while (orderit->hasNext()) {
  33                 Order *order = orderit->next();
  34
  35                 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
  36                         continue;
  37                 }
  38
  39                 OrderGraph *graph = buildOrderGraph(order);
  40                 if (order->type == SATC_PARTIAL) {
  41                         //Required to do SCC analysis for partial order graphs.  It
  42                         //makes sure we don't incorrectly optimize graphs with negative
  43                         //polarity edges
  44                         completePartialOrderGraph(graph);
  45                 }
  46
  47                 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
  48
  49                 if (mustReachGlobal)
  50                         reachMustAnalysis(solver, graph, false);
  51
  52                 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
  53
  54                 if (mustReachLocal) {
  55                         //This pair of analysis is also optional
  56                         if (order->type == SATC_PARTIAL) {
  57                                 localMustAnalysisPartial(solver, graph);
  58                         } else {
  59                                 localMustAnalysisTotal(solver, graph);
  60                         }
  61                 }
  62
  63
  64                 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
  65                 HashsetOrderEdge *edgesRemoved = NULL;
  66
  67                 if (mustReachPrune) {
  68                         edgesRemoved = new HashsetOrderEdge();
  69                         removeMustBeTrueNodes(graph, edgesRemoved);
  70                 }
  71
  72                 //This is needed for splitorder
  73                 computeStronglyConnectedComponentGraph(graph);
  74                 decomposeOrder(order, graph, edgesRemoved);
  75                 if (edgesRemoved != NULL)
  76                         delete edgesRemoved;
  77         }
  78         delete orderit;
  79         delete orders;
  80 }
  81
  82
  83 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved) {
  84         Vector<Order *> ordervec;
  85         Vector<Order *> partialcandidatevec;
  86         uint size = currOrder->constraints.getSize();
  87         for (uint i = 0; i < size; i++) {
  88                 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
  89                 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
  90                 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
  91                 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
  92                 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
  93                 if (edgesRemoved != NULL) {
  94                         if (edgesRemoved->contains(edge)) {
  95                                 solver->replaceBooleanWithTrue(orderconstraint);
  96                                 continue;
  97                         } else if (edgesRemoved->contains(invedge)) {
  98                                 solver->replaceBooleanWithFalse(orderconstraint);
  99                                 continue;
 100                         }
 101                 }
 102
 103                 if (from->sccNum != to->sccNum) {
 104                         if (edge != NULL) {
 105                                 if (edge->polPos) {
 106                                         solver->replaceBooleanWithTrue(orderconstraint);
 107                                 } else if (edge->polNeg) {
 108                                         solver->replaceBooleanWithFalse(orderconstraint);
 109                                 } else {
 110                                         //This case should only be possible if constraint isn't in AST
 111                                         //This can happen, so don't do anything
 112                                         ;
 113                                 }
 114                         } else {
 115                                 if (invedge != NULL) {
 116                                         if (invedge->polPos) {
 117                                                 solver->replaceBooleanWithFalse(orderconstraint);
 118                                         } else if (edge->polNeg) {
 119                                                 //This case shouldn't happen...  If we have a partial order,
 120                                                 //then we should have our own edge...If we have a total
 121                                                 //order, then this edge should be positive...
 122                                                 ASSERT(0);
 123                                         } else {
 124                                                 //This case should only be possible if constraint isn't in AST
 125                                                 //This can happen, so don't do anything
 126                                                 ;
 127                                         }
 128                                 }
 129                         }
 130                 } else {
 131                         //Build new order and change constraint's order
 132                         Order *neworder = NULL;
 133                         if (ordervec.getSize() > from->sccNum)
 134                                 neworder = ordervec.get(from->sccNum);
 135                         if (neworder == NULL) {
 136                                 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
 137                                 neworder = solver->createOrder(currOrder->type, set);
 138                                 ordervec.setExpand(from->sccNum, neworder);
 139                                 if (currOrder->type == SATC_PARTIAL)
 140                                         partialcandidatevec.setExpand(from->sccNum, neworder);
 141                                 else
 142                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 143                         }
 144                         if (from->status != ADDEDTOSET) {
 145                                 from->status = ADDEDTOSET;
 146                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 147                         }
 148                         if (to->status != ADDEDTOSET) {
 149                                 to->status = ADDEDTOSET;
 150                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 151                         }
 152                         if (currOrder->type == SATC_PARTIAL) {
 153                                 if (edge->polNeg)
 154                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 155                         }
 156                         orderconstraint->order = neworder;
 157                         neworder->addOrderConstraint(orderconstraint);
 158                 }
 159         }
 160         currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
 161         solver->getActiveOrders()->remove(currOrder);
 162         uint pcvsize = partialcandidatevec.getSize();
 163         for (uint i = 0; i < pcvsize; i++) {
 164                 Order *neworder = partialcandidatevec.get(i);
 165                 if (neworder != NULL) {
 166                         neworder->type = SATC_TOTAL;
 167                 }
 168         }
 169 }
 170
 171 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
 172         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 173         while (iterator->hasNext()) {
 174                 OrderEdge *edge = iterator->next();
 175                 if (!edge->mustPos) {
 176                         delete iterator;
 177                         return false;
 178                 }
 179         }
 180         delete iterator;
 181         iterator = node->outEdges.iterator();
 182         while (iterator->hasNext()) {
 183                 OrderEdge *edge = iterator->next();
 184                 if (!edge->mustPos) {
 185                         delete iterator;
 186                         return false;
 187                 }
 188         }
 189         delete iterator;
 190         return true;
 191 }
 192
 193 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
 194         SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 195         while (iterin->hasNext()) {
 196                 OrderEdge *inEdge = iterin->next();
 197                 OrderNode *srcNode = inEdge->source;
 198                 srcNode->outEdges.remove(inEdge);
 199                 edgesRemoved->add(inEdge);
 200                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 201                 while (iterout->hasNext()) {
 202                         OrderEdge *outEdge = iterout->next();
 203                         OrderNode *sinkNode = outEdge->sink;
 204                         sinkNode->inEdges.remove(outEdge);
 205                         edgesRemoved->add(outEdge);
 206                         //Adding new edge to new sink and src nodes ...
 207                         if (srcNode == sinkNode) {
 208                                 solver->setUnSAT();
 209                                 delete iterout;
 210                                 delete iterin;
 211                                 return;
 212                         }
 213                         //Add new order constraint
 214                         BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
 215                         solver->addConstraint(orderconstraint);
 216
 217                         //Add new edge
 218                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 219                         newEdge->mustPos = true;
 220                         newEdge->polPos = true;
 221                         if (newEdge->mustNeg)
 222                                 solver->setUnSAT();
 223                         srcNode->outEdges.add(newEdge);
 224                         sinkNode->inEdges.add(newEdge);
 225                 }
 226                 delete iterout;
 227         }
 228         delete iterin;
 229 }
 230
 231 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
 232         SetIteratorOrderNode *iterator = graph->getNodes();
 233         while (iterator->hasNext()) {
 234                 OrderNode *node = iterator->next();
 235                 if (isMustBeTrueNode(node)) {
 236                         bypassMustBeTrueNode(graph, node, edgesRemoved);
 237                 }
 238         }
 239         delete iterator;
 240 }