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