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