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
 157                         dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
 158                 }
 159         }
 160         solver->getActiveOrders()->remove(currOrder);
 161         uint pcvsize = partialcandidatevec.getSize();
 162         for (uint i = 0; i < pcvsize; i++) {
 163                 Order *neworder = partialcandidatevec.get(i);
 164                 if (neworder != NULL) {
 165                         neworder->type = SATC_TOTAL;
 166                 }
 167         }
 168 }
 169
 170 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
 171         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 172         while (iterator->hasNext()) {
 173                 OrderEdge *edge = iterator->next();
 174                 if (!edge->mustPos) {
 175                         delete iterator;
 176                         return false;
 177                 }
 178         }
 179         delete iterator;
 180         iterator = node->outEdges.iterator();
 181         while (iterator->hasNext()) {
 182                 OrderEdge *edge = iterator->next();
 183                 if (!edge->mustPos) {
 184                         delete iterator;
 185                         return false;
 186                 }
 187         }
 188         delete iterator;
 189         return true;
 190 }
 191
 192 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 193         node->removed = true;
 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                 dor->mustOrderEdge(srcNode->getID(), node->getID());
 200                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
 201                 solver->replaceBooleanWithTrue(be);
 202
 203                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 204                 while (iterout->hasNext()) {
 205                         OrderEdge *outEdge = iterout->next();
 206                         OrderNode *sinkNode = outEdge->sink;
 207                         //Adding new edge to new sink and src nodes ...
 208                         if (srcNode == sinkNode) {
 209                                 solver->setUnSAT();
 210                                 delete iterout;
 211                                 delete iterin;
 212                                 return;
 213                         }
 214                         //Add new order constraint
 215                         BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
 216                         solver->addConstraint(orderconstraint);
 217
 218                         //Add new edge
 219                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 220                         newEdge->mustPos = true;
 221                         newEdge->polPos = true;
 222                         if (newEdge->mustNeg)
 223                                 solver->setUnSAT();
 224                         srcNode->outEdges.add(newEdge);
 225                         sinkNode->inEdges.add(newEdge);
 226                 }
 227                 delete iterout;
 228         }
 229         delete iterin;
 230
 231         //Clean up old edges...  Keep this later in case we don't have any in edges
 232         SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 233         while (iterout->hasNext()) {
 234                 OrderEdge *outEdge = iterout->next();
 235                 OrderNode *sinkNode = outEdge->sink;
 236                 dor->mustOrderEdge(node->getID(), sinkNode->getID());
 237                 sinkNode->inEdges.remove(outEdge);
 238                 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
 239                 solver->replaceBooleanWithTrue(be2);
 240         }
 241         delete iterout;
 242 }
 243
 244 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
 245         SetIteratorOrderNode *iterator = graph->getNodes();
 246         while (iterator->hasNext()) {
 247                 OrderNode *node = (OrderNode*)iterator->next();
 248                 if (node->removed)
 249                         continue;
 250                 if (isMustBeTrueNode(node)) {
 251                         bypassMustBeTrueNode(graph, node, dor);
 252                 }
 253         }
 254         delete iterator;
 255 }
 256
 257 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
 258         SetIteratorOrderNode *iterator = graph->getNodes();
 259         while (iterator->hasNext()) {
 260                 OrderNode *node = (OrderNode*)iterator->next();
 261                 if (node->removed)
 262                         continue;
 263                 attemptNodeMerge(graph, node, dor);
 264         }
 265         delete iterator;
 266 }
 267
 268 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 269         SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
 270         while (edgeit->hasNext()) {
 271                 OrderEdge *outedge = edgeit->next();
 272                 //Only eliminate must edges
 273                 if (!outedge->mustPos)
 274                         continue;
 275                 OrderNode *dstnode = outedge->sink;
 276                 uint numOutEdges = node->outEdges.getSize();
 277                 uint numInEdges = dstnode->inEdges.getSize();
 278                 /*
 279                    Need to avoid a situation where we create new reachability by
 280                    the merge.  This can only happen if there is an extra in edge to
 281                    the dstnode and an extra out edge to our node.
 282                  */
 283
 284                 if (numOutEdges == 1 || numInEdges == 1) {
 285                         /* Safe to do the Merge */
 286                         mergeNodes(graph, node, outedge, dstnode, dor);
 287
 288                         //Throw away the iterator and start over
 289                         delete edgeit;
 290                         edgeit = node->outEdges.iterator();
 291                 }
 292         }
 293         delete edgeit;
 294 }
 295
 296 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
 297         /* Fix up must edge between the two nodes */
 298         node->outEdges.remove(edge);
 299         dstnode->inEdges.remove(edge);
 300         dor->mustOrderEdge(node->getID(), dstnode->getID());
 301
 302         BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
 303         solver->replaceBooleanWithTrue(be);
 304
 305         /* Go through the incoming edges to the new node */
 306         SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
 307         while (inedgeit->hasNext()) {
 308                 OrderEdge *inedge = inedgeit->next();
 309                 OrderNode *source = inedge->source;
 310                 //remove it from the source node
 311                 source->outEdges.remove(inedge);
 312                 //save the remapping that we did
 313                 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
 314                 //create the new edge
 315                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
 316                 //update the flags
 317                 newedge->polPos |= inedge->polPos;
 318                 newedge->polNeg |= inedge->polNeg;
 319                 newedge->mustPos |= inedge->mustPos;
 320                 newedge->mustNeg |= inedge->mustNeg;
 321                 newedge->pseudoPos |= inedge->pseudoPos;
 322                 //add new edge to both
 323                 source->outEdges.add(newedge);
 324                 node->inEdges.add(newedge);
 325
 326                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
 327                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
 328                 solver->replaceBooleanWithBoolean(be, benew);
 329         }
 330         dstnode->inEdges.reset();
 331         delete inedgeit;
 332
 333         /* Go through the outgoing edges from the new node */
 334         SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
 335         while (outedgeit->hasNext()) {
 336                 OrderEdge *outedge = outedgeit->next();
 337                 OrderNode *sink = outedge->sink;
 338                 //remove it from the sink node
 339                 sink->inEdges.remove(outedge);
 340                 //save the remapping that we did
 341                 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
 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 }