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 #include "polarityassignment.h"
  20
  21
  22 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
  23         : Transform(_solver)
  24 {
  25 }
  26
  27 DecomposeOrderTransform::~DecomposeOrderTransform() {
  28 }
  29
  30 void DecomposeOrderTransform::doTransform() {
  31         HashsetOrder *orders = solver->getActiveOrders()->copy();
  32         SetIteratorOrder *orderit = orders->iterator();
  33         while (orderit->hasNext()) {
  34                 Order *order = orderit->next();
  35
  36                 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
  37                         continue;
  38                 }
  39
  40                 DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
  41                 order->setOrderResolver(dor);
  42
  43                 OrderGraph *graph = buildOrderGraph(order);
  44                 if (order->type == SATC_PARTIAL) {
  45                         //Required to do SCC analysis for partial order graphs.  It
  46                         //makes sure we don't incorrectly optimize graphs with negative
  47                         //polarity edges
  48                         graph->completePartialOrderGraph();
  49                 }
  50
  51                 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
  52                 if (mustReachGlobal)
  53                         reachMustAnalysis(solver, graph, false);
  54
  55                 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
  56                 if (mustReachLocal) {
  57                         //This pair of analysis is also optional
  58                         if (order->type == SATC_PARTIAL) {
  59                                 localMustAnalysisPartial(solver, graph);
  60                         } else {
  61                                 localMustAnalysisTotal(solver, graph);
  62                         }
  63                 }
  64
  65                 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
  66
  67                 if (mustReachPrune) {
  68                         removeMustBeTrueNodes(graph, dor);
  69                 }
  70
  71                 bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
  72
  73                 if (pruneEdges) {
  74                         mustEdgePrune(graph, dor);
  75                 }
  76
  77                 //This is needed for splitorder
  78                 graph->computeStronglyConnectedComponentGraph();
  79                 decomposeOrder(order, graph, dor);
  80                 delete graph;
  81         }
  82         delete orderit;
  83         delete orders;
  84 }
  85
  86
  87 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
  88         Vector<Order *> partialcandidatevec;
  89         uint size = currOrder->constraints.getSize();
  90         for (uint i = 0; i < size; i++) {
  91                 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
  92                 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
  93                 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
  94                 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
  95                 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
  96                 if (from->removed || to->removed)
  97                         continue;
  98
  99                 if (from->sccNum != to->sccNum) {
 100                         if (edge != NULL) {
 101                                 if (edge->polPos) {
 102                                         dor->mustOrderEdge(from->getID(), to->getID());
 103                                         solver->replaceBooleanWithTrue(orderconstraint);
 104                                 } else if (edge->polNeg) {
 105                                         if (currOrder->type == SATC_TOTAL)
 106                                                 dor->mustOrderEdge(to->getID(), from->getID());
 107                                         solver->replaceBooleanWithFalse(orderconstraint);
 108                                 } else {
 109                                         //This case should only be possible if constraint isn't in AST
 110                                         //This can happen, so don't do anything
 111                                         ;
 112                                 }
 113                         } else {
 114                                 if (invedge != NULL) {
 115                                         if (invedge->polPos) {
 116                                                 dor->mustOrderEdge(to->getID(), from->getID());
 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                         neworder = dor->getOrder(from->sccNum);
 134                         if (neworder == NULL) {
 135                                 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
 136                                 neworder = solver->createOrder(currOrder->type, set);
 137                                 dor->setOrder(from->sccNum, neworder);
 138                                 if (currOrder->type == SATC_PARTIAL)
 139                                         partialcandidatevec.setExpand(from->sccNum, neworder);
 140                                 else
 141                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 142                         }
 143                         if (from->status != ADDEDTOSET) {
 144                                 from->status = ADDEDTOSET;
 145                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
 146                         }
 147                         if (to->status != ADDEDTOSET) {
 148                                 to->status = ADDEDTOSET;
 149                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
 150                         }
 151                         if (currOrder->type == SATC_PARTIAL) {
 152                                 if (edge->polNeg)
 153                                         partialcandidatevec.setExpand(from->sccNum, NULL);
 154                         }
 155                         BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
 156                         solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
 157                         updateEdgePolarity(neworderconstraint, orderconstraint);
 158                         dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
 159                 }
 160         }
 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, DecomposeOrderResolver *dor) {
 194         node->removed = true;
 195         SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 196         while (iterin->hasNext()) {
 197                 OrderEdge *inEdge = iterin->next();
 198                 OrderNode *srcNode = inEdge->source;
 199                 srcNode->outEdges.remove(inEdge);
 200                 dor->mustOrderEdge(srcNode->getID(), node->getID());
 201                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
 202                 solver->replaceBooleanWithTrue(be);
 203
 204                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 205                 while (iterout->hasNext()) {
 206                         OrderEdge *outEdge = iterout->next();
 207                         OrderNode *sinkNode = outEdge->sink;
 208                         //Adding new edge to new sink and src nodes ...
 209                         if (srcNode == sinkNode) {
 210                                 solver->setUnSAT();
 211                                 delete iterout;
 212                                 delete iterin;
 213                                 return;
 214                         }
 215                         //Add new order constraint
 216                         BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
 217                         updateEdgePolarity(orderconstraint, P_TRUE);
 218                         solver->addConstraint(orderconstraint);
 219
 220                         //Add new edge
 221                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 222                         newEdge->mustPos = true;
 223                         newEdge->polPos = true;
 224                         if (newEdge->mustNeg)
 225                                 solver->setUnSAT();
 226                         srcNode->outEdges.add(newEdge);
 227                         sinkNode->inEdges.add(newEdge);
 228                 }
 229                 delete iterout;
 230         }
 231         delete iterin;
 232
 233         //Clean up old edges...  Keep this later in case we don't have any in edges
 234         SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 235         while (iterout->hasNext()) {
 236                 OrderEdge *outEdge = iterout->next();
 237                 OrderNode *sinkNode = outEdge->sink;
 238                 dor->mustOrderEdge(node->getID(), sinkNode->getID());
 239                 sinkNode->inEdges.remove(outEdge);
 240                 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
 241                 solver->replaceBooleanWithTrue(be2);
 242         }
 243         delete iterout;
 244 }
 245
 246 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
 247         SetIteratorOrderNode *iterator = graph->getNodes();
 248         while (iterator->hasNext()) {
 249                 OrderNode *node = (OrderNode *)iterator->next();
 250                 if (node->removed)
 251                         continue;
 252                 if (isMustBeTrueNode(node)) {
 253                         bypassMustBeTrueNode(graph, node, dor);
 254                 }
 255         }
 256         delete iterator;
 257 }
 258
 259 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
 260         SetIteratorOrderNode *iterator = graph->getNodes();
 261         while (iterator->hasNext()) {
 262                 OrderNode *node = (OrderNode *)iterator->next();
 263                 if (node->removed)
 264                         continue;
 265                 attemptNodeMerge(graph, node, dor);
 266         }
 267         delete iterator;
 268 }
 269
 270 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 271         SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
 272         while (edgeit->hasNext()) {
 273                 OrderEdge *outedge = edgeit->next();
 274                 //Only eliminate must edges
 275                 if (!outedge->mustPos)
 276                         continue;
 277                 OrderNode *dstnode = outedge->sink;
 278                 uint numOutEdges = node->outEdges.getSize();
 279                 uint numInEdges = dstnode->inEdges.getSize();
 280                 /*
 281                    Need to avoid a situation where we create new reachability by
 282                    the merge.  This can only happen if there is an extra in edge to
 283                    the dstnode and an extra out edge to our node.
 284                  */
 285
 286                 if (numOutEdges == 1 || numInEdges == 1) {
 287                         /* Safe to do the Merge */
 288                         mergeNodes(graph, node, outedge, dstnode, dor);
 289
 290                         //Throw away the iterator and start over
 291                         delete edgeit;
 292                         edgeit = node->outEdges.iterator();
 293                 }
 294         }
 295         delete edgeit;
 296 }
 297
 298 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
 299         /* Fix up must edge between the two nodes */
 300         node->outEdges.remove(edge);
 301         dstnode->inEdges.remove(edge);
 302         dor->mustOrderEdge(node->getID(), dstnode->getID());
 303
 304         BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
 305         solver->replaceBooleanWithTrue(be);
 306
 307         /* Go through the incoming edges to the new node */
 308         SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
 309         while (inedgeit->hasNext()) {
 310                 OrderEdge *inedge = inedgeit->next();
 311                 OrderNode *source = inedge->source;
 312                 //remove it from the source node
 313                 source->outEdges.remove(inedge);
 314                 //save the remapping that we did
 315                 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
 316                 //create the new edge
 317                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
 318                 //update the flags
 319                 newedge->polPos |= inedge->polPos;
 320                 newedge->polNeg |= inedge->polNeg;
 321                 newedge->mustPos |= inedge->mustPos;
 322                 newedge->mustNeg |= inedge->mustNeg;
 323                 newedge->pseudoPos |= inedge->pseudoPos;
 324                 //add new edge to both
 325                 source->outEdges.add(newedge);
 326                 node->inEdges.add(newedge);
 327
 328                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
 329                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
 330                 updateEdgePolarity(benew, be);
 331                 solver->replaceBooleanWithBoolean(be, benew);
 332         }
 333         dstnode->inEdges.reset();
 334         delete inedgeit;
 335
 336         /* Go through the outgoing edges from the new node */
 337         SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
 338         while (outedgeit->hasNext()) {
 339                 OrderEdge *outedge = outedgeit->next();
 340                 OrderNode *sink = outedge->sink;
 341                 //remove it from the sink node
 342                 sink->inEdges.remove(outedge);
 343                 //save the remapping that we did
 344                 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
 345
 346                 //create the new edge
 347                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
 348                 //update the flags
 349                 newedge->polPos |= outedge->polPos;
 350                 newedge->polNeg |= outedge->polNeg;
 351                 newedge->mustPos |= outedge->mustPos;
 352                 newedge->mustNeg |= outedge->mustNeg;
 353                 newedge->pseudoPos |= outedge->pseudoPos;
 354                 //add new edge to both
 355                 sink->inEdges.add(newedge);
 356                 node->outEdges.add(newedge);
 357
 358                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
 359                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
 360                 updateEdgePolarity(benew, be);
 361                 solver->replaceBooleanWithBoolean(be, benew);
 362         }
 363         dstnode->outEdges.reset();
 364         delete outedgeit;
 365
 366
 367         /* Mark destination as removed */
 368         dstnode->removed = true;
 369 }