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