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