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         model_print("Removing %llu\n", node->getID());
 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                         solver->addConstraint(orderconstraint);
 218
 219                         //Add new edge
 220                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 221                         newEdge->mustPos = true;
 222                         newEdge->polPos = true;
 223                         if (newEdge->mustNeg)
 224                                 solver->setUnSAT();
 225                         srcNode->outEdges.add(newEdge);
 226                         sinkNode->inEdges.add(newEdge);
 227                 }
 228                 delete iterout;
 229         }
 230         delete iterin;
 231
 232         //Clean up old edges...  Keep this later in case we don't have any in edges
 233         SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 234         while (iterout->hasNext()) {
 235                 OrderEdge *outEdge = iterout->next();
 236                 OrderNode *sinkNode = outEdge->sink;
 237                 dor->mustOrderEdge(node->getID(), sinkNode->getID());
 238                 sinkNode->inEdges.remove(outEdge);
 239                 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
 240                 solver->replaceBooleanWithTrue(be2);
 241         }
 242         delete iterout;
 243 }
 244
 245 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
 246         SetIteratorOrderNode *iterator = graph->getNodes();
 247         while (iterator->hasNext()) {
 248                 OrderNode *node = iterator->next();
 249                 if (node->removed)
 250                         continue;
 251                 if (isMustBeTrueNode(node)) {
 252                         bypassMustBeTrueNode(graph, node, dor);
 253                 }
 254         }
 255         delete iterator;
 256 }
 257
 258 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
 259         SetIteratorOrderNode *iterator = graph->getNodes();
 260         while (iterator->hasNext()) {
 261                 OrderNode *node = iterator->next();
 262                 if (node->removed)
 263                         continue;
 264                 attemptNodeMerge(graph, node, dor);
 265         }
 266         delete iterator;
 267 }
 268
 269 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
 270         SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
 271         while (edgeit->hasNext()) {
 272                 OrderEdge *outedge = edgeit->next();
 273                 //Only eliminate must edges
 274                 if (!outedge->mustPos)
 275                         continue;
 276                 OrderNode *dstnode = outedge->sink;
 277                 uint numOutEdges = node->outEdges.getSize();
 278                 uint numInEdges = dstnode->inEdges.getSize();
 279                 /*
 280                    Need to avoid a situation where we create new reachability by
 281                    the merge.  This can only happen if there is an extra in edge to
 282                    the dstnode and an extra out edge to our node.
 283                  */
 284
 285                 if (numOutEdges == 1 || numInEdges == 1) {
 286                         /* Safe to do the Merge */
 287                         mergeNodes(graph, node, outedge, dstnode, dor);
 288
 289                         //Throw away the iterator and start over
 290                         delete edgeit;
 291                         edgeit = node->outEdges.iterator();
 292                 }
 293         }
 294         delete edgeit;
 295 }
 296
 297 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
 298         /* Fix up must edge between the two nodes */
 299         node->outEdges.remove(edge);
 300         dstnode->inEdges.remove(edge);
 301         dor->mustOrderEdge(node->getID(), dstnode->getID());
 302
 303         BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
 304         solver->replaceBooleanWithTrue(be);
 305
 306         /* Go through the incoming edges to the new node */
 307         SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
 308         while (inedgeit->hasNext()) {
 309                 OrderEdge *inedge = inedgeit->next();
 310                 OrderNode *source = inedge->source;
 311                 //remove it from the source node
 312                 source->outEdges.remove(inedge);
 313                 //save the remapping that we did
 314                 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
 315                 //create the new edge
 316                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
 317                 //update the flags
 318                 newedge->polPos |= inedge->polPos;
 319                 newedge->polNeg |= inedge->polNeg;
 320                 newedge->mustPos |= inedge->mustPos;
 321                 newedge->mustNeg |= inedge->mustNeg;
 322                 newedge->pseudoPos |= inedge->pseudoPos;
 323                 //add new edge to both
 324                 source->outEdges.add(newedge);
 325                 node->inEdges.add(newedge);
 326
 327                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
 328                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
 329                 solver->replaceBooleanWithBoolean(be, benew);
 330         }
 331         dstnode->inEdges.reset();
 332         delete inedgeit;
 333
 334         /* Go through the outgoing edges from the new node */
 335         SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
 336         while (outedgeit->hasNext()) {
 337                 OrderEdge *outedge = outedgeit->next();
 338                 OrderNode *sink = outedge->sink;
 339                 //remove it from the sink node
 340                 sink->inEdges.remove(outedge);
 341                 //save the remapping that we did
 342                 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
 343                 //create the new edge
 344                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
 345                 //update the flags
 346                 newedge->polPos |= outedge->polPos;
 347                 newedge->polNeg |= outedge->polNeg;
 348                 newedge->mustPos |= outedge->mustPos;
 349                 newedge->mustNeg |= outedge->mustNeg;
 350                 newedge->pseudoPos |= outedge->pseudoPos;
 351                 //add new edge to both
 352                 sink->inEdges.add(newedge);
 353                 node->outEdges.add(newedge);
 354
 355                 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
 356                 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
 357                 solver->replaceBooleanWithBoolean(be, benew);
 358         }
 359         dstnode->outEdges.reset();
 360         delete outedgeit;
 361
 362
 363         /* Mark destination as removed */
 364         dstnode->removed = true;
 365 }