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
  66                 if (mustReachPrune) {
  67                         removeMustBeTrueNodes(graph, dor);
  68                 }
  69
  70                 bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
  71
  72                 if (pruneEdges) {
  73                         mustEdgePrune(graph, dor);
  74                 }
  75
  76                 //This is needed for splitorder
  77                 graph->computeStronglyConnectedComponentGraph();
  78                 decomposeOrder(order, graph, dor);
  79                 delete graph;
  80         }
  81         delete orderit;
  82         delete orders;
  83 }
  84
  85
  86 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
  87         Vector<Order *> partialcandidatevec;
  88         uint size = currOrder->constraints.getSize();
  89         for (uint i = 0; i < size; i++) {
  90                 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
  91                 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
  92                 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
  93                 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
  94                 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
  95                 if (from->removed || to->removed)
  96                         continue;
  97
  98                 if (from->sccNum != to->sccNum) {
  99                         if (edge != NULL) {
 100                                 if (edge->polPos) {
 101                                         dor->mustOrderEdge(from->getID(), to->getID());
 102                                         solver->replaceBooleanWithTrue(orderconstraint);
 103                                 } else if (edge->polNeg) {
 104                                         if (currOrder->type == SATC_TOTAL)
 105                                                 dor->mustOrderEdge(to->getID(), from->getID());
 106                                         solver->replaceBooleanWithFalse(orderconstraint);
 107                                 } else {
 108                                         //This case should only be possible if constraint isn't in AST
 109                                         //This can happen, so don't do anything
 110                                         ;
 111                                 }
 112                         } else {
 113                                 if (invedge != NULL) {
 114                                         if (invedge->polPos) {
 115                                                 dor->mustOrderEdge(to->getID(), from->getID());
 116                                                 solver->replaceBooleanWithFalse(orderconstraint);
 117                                         } else if (edge->polNeg) {
 118                                                 //This case shouldn't happen...  If we have a partial order,
 119                                                 //then we should have our own edge...If we have a total
 120                                                 //order, then this edge should be positive...
 121                                                 ASSERT(0);
 122                                         } else {
 123                                                 //This case should only be possible if constraint isn't in AST
 124                                                 //This can happen, so don't do anything
 125                                                 ;
 126                                         }
 127                                 }
 128                         }
 129                 } else {
 130                         //Build new order and change constraint's order
 131                         Order *neworder = NULL;
 132                         neworder = dor->getOrder(from->sccNum);
 133                         if (neworder == NULL) {
 134                                 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
 135                                 neworder = solver->createOrder(currOrder->type, set);
 136                                 dor->setOrder(from->sccNum, neworder);
 137                                 if (currOrder->type == SATC_PARTIAL)
 138                                         partialcandidatevec.setExpand(from->sccNum, neworder);
 139                                 else
 140                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 141                         }
 142                         if (from->status != ADDEDTOSET) {
 143                                 from->status = ADDEDTOSET;
 144                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 145                         }
 146                         if (to->status != ADDEDTOSET) {
 147                                 to->status = ADDEDTOSET;
 148                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 149                         }
 150                         if (currOrder->type == SATC_PARTIAL) {
 151                                 if (edge->polNeg)
 152                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 153                         }
 154                         BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
 155                         solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
 156                         dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
 157                 }
 158         }
 159         solver->getActiveOrders()->remove(currOrder);
 160         uint pcvsize = partialcandidatevec.getSize();
 161         for (uint i = 0; i < pcvsize; i++) {
 162                 Order *neworder = partialcandidatevec.get(i);
 163                 if (neworder != NULL) {
 164                         neworder->type = SATC_TOTAL;
 165                 }
 166         }
 167 }
 168
 169 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
 170         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 171         while (iterator->hasNext()) {
 172                 OrderEdge *edge = iterator->next();
 173                 if (!edge->mustPos) {
 174                         delete iterator;
 175                         return false;
 176                 }
 177         }
 178         delete iterator;
 179         iterator = node->outEdges.iterator();
 180         while (iterator->hasNext()) {
 181                 OrderEdge *edge = iterator->next();
 182                 if (!edge->mustPos) {
 183                         delete iterator;
 184                         return false;
 185                 }
 186         }
 187         delete iterator;
 188         return true;
 189 }
 190
 191 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 192         node->removed = true;
 193         SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 194         while (iterin->hasNext()) {
 195                 OrderEdge *inEdge = iterin->next();
 196                 OrderNode *srcNode = inEdge->source;
 197                 srcNode->outEdges.remove(inEdge);
 198                 dor->mustOrderEdge(srcNode->getID(), node->getID());
 199                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
 200                 solver->replaceBooleanWithTrue(be);
 201
 202                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 203                 while (iterout->hasNext()) {
 204                         OrderEdge *outEdge = iterout->next();
 205                         OrderNode *sinkNode = outEdge->sink;
 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         //Clean up old edges...  Keep this later in case we don't have any in edges
 231         SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 232         while (iterout->hasNext()) {
 233                 OrderEdge *outEdge = iterout->next();
 234                 OrderNode *sinkNode = outEdge->sink;
 235                 dor->mustOrderEdge(node->getID(), sinkNode->getID());
 236                 sinkNode->inEdges.remove(outEdge);
 237                 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
 238                 solver->replaceBooleanWithTrue(be2);
 239         }
 240         delete iterout;
 241 }
 242
 243 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
 244         SetIteratorOrderNode *iterator = graph->getNodes();
 245         while (iterator->hasNext()) {
 246                 OrderNode *node = (OrderNode *)iterator->next();
 247                 if (node->removed)
 248                         continue;
 249                 if (isMustBeTrueNode(node)) {
 250                         bypassMustBeTrueNode(graph, node, dor);
 251                 }
 252         }
 253         delete iterator;
 254 }
 255
 256 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
 257         SetIteratorOrderNode *iterator = graph->getNodes();
 258         while (iterator->hasNext()) {
 259                 OrderNode *node = (OrderNode *)iterator->next();
 260                 if (node->removed)
 261                         continue;
 262                 attemptNodeMerge(graph, node, dor);
 263         }
 264         delete iterator;
 265 }
 266
 267 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 268         SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
 269         while (edgeit->hasNext()) {
 270                 OrderEdge *outedge = edgeit->next();
 271                 //Only eliminate must edges
 272                 if (!outedge->mustPos)
 273                         continue;
 274                 OrderNode *dstnode = outedge->sink;
 275                 uint numOutEdges = node->outEdges.getSize();
 276                 uint numInEdges = dstnode->inEdges.getSize();
 277                 /*
 278                    Need to avoid a situation where we create new reachability by
 279                    the merge.  This can only happen if there is an extra in edge to
 280                    the dstnode and an extra out edge to our node.
 281                  */
 282
 283                 if (numOutEdges == 1 || numInEdges == 1) {
 284                         /* Safe to do the Merge */
 285                         mergeNodes(graph, node, outedge, dstnode, dor);
 286
 287                         //Throw away the iterator and start over
 288                         delete edgeit;
 289                         edgeit = node->outEdges.iterator();
 290                 }
 291         }
 292         delete edgeit;
 293 }
 294
 295 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
 296         /* Fix up must edge between the two nodes */
 297         node->outEdges.remove(edge);
 298         dstnode->inEdges.remove(edge);
 299         dor->mustOrderEdge(node->getID(), dstnode->getID());
 300
 301         BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
 302         solver->replaceBooleanWithTrue(be);
 303
 304         /* Go through the incoming edges to the new node */
 305         SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
 306         while (inedgeit->hasNext()) {
 307                 OrderEdge *inedge = inedgeit->next();
 308                 OrderNode *source = inedge->source;
 309                 //remove it from the source node
 310                 source->outEdges.remove(inedge);
 311                 //save the remapping that we did
 312                 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
 313                 //create the new edge
 314                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
 315                 //update the flags
 316                 newedge->polPos |= inedge->polPos;
 317                 newedge->polNeg |= inedge->polNeg;
 318                 newedge->mustPos |= inedge->mustPos;
 319                 newedge->mustNeg |= inedge->mustNeg;
 320                 newedge->pseudoPos |= inedge->pseudoPos;
 321                 //add new edge to both
 322                 source->outEdges.add(newedge);
 323                 node->inEdges.add(newedge);
 324
 325                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
 326                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
 327                 solver->replaceBooleanWithBoolean(be, benew);
 328         }
 329         dstnode->inEdges.reset();
 330         delete inedgeit;
 331
 332         /* Go through the outgoing edges from the new node */
 333         SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
 334         while (outedgeit->hasNext()) {
 335                 OrderEdge *outedge = outedgeit->next();
 336                 OrderNode *sink = outedge->sink;
 337                 //remove it from the sink node
 338                 sink->inEdges.remove(outedge);
 339                 //save the remapping that we did
 340                 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
 341
 342                 //create the new edge
 343                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
 344                 //update the flags
 345                 newedge->polPos |= outedge->polPos;
 346                 newedge->polNeg |= outedge->polNeg;
 347                 newedge->mustPos |= outedge->mustPos;
 348                 newedge->mustNeg |= outedge->mustNeg;
 349                 newedge->pseudoPos |= outedge->pseudoPos;
 350                 //add new edge to both
 351                 sink->inEdges.add(newedge);
 352                 node->outEdges.add(newedge);
 353
 354                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
 355                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
 356                 solver->replaceBooleanWithBoolean(be, benew);
 357         }
 358         dstnode->outEdges.reset();
 359         delete outedgeit;
 360
 361
 362         /* Mark destination as removed */
 363         dstnode->removed = true;
 364 }