src/Encoders/orderencoder.c

   1 #include "orderencoder.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "boolean.h"
   5 #include "ordergraph.h"
   6 #include "order.h"
   7 #include "ordernode.h"
   8 #include "rewriter.h"
   9 #include "mutableset.h"
  10 #include "tunable.h"
  11
  12 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
  13         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  14         while (hasNextOrderNode(iterator)) {
  15                 OrderNode *node = nextOrderNode(iterator);
  16                 if (node->status == NOTVISITED) {
  17                         node->status = VISITED;
  18                         DFSNodeVisit(node, finishNodes, false, 0);
  19                         node->status = FINISHED;
  20                         pushVectorOrderNode(finishNodes, node);
  21                 }
  22         }
  23         deleteIterOrderNode(iterator);
  24 }
  25
  26 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
  27         uint size = getSizeVectorOrderNode(finishNodes);
  28         uint sccNum = 1;
  29         for (int i = size - 1; i >= 0; i--) {
  30                 OrderNode *node = getVectorOrderNode(finishNodes, i);
  31                 if (node->status == NOTVISITED) {
  32                         node->status = VISITED;
  33                         DFSNodeVisit(node, NULL, true, sccNum);
  34                         node->sccNum = sccNum;
  35                         node->status = FINISHED;
  36                         sccNum++;
  37                 }
  38         }
  39 }
  40
  41 void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum) {
  42         HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
  43         while (hasNextOrderEdge(iterator)) {
  44                 OrderEdge *edge = nextOrderEdge(iterator);
  45                 if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
  46                         continue;
  47
  48                 OrderNode *child = isReverse ? edge->source : edge->sink;
  49
  50                 if (child->status == NOTVISITED) {
  51                         child->status = VISITED;
  52                         DFSNodeVisit(child, finishNodes, isReverse, sccNum);
  53                         child->status = FINISHED;
  54                         if (finishNodes != NULL)
  55                                 pushVectorOrderNode(finishNodes, child);
  56                         if (isReverse)
  57                                 child->sccNum = sccNum;
  58                 }
  59         }
  60         deleteIterOrderEdge(iterator);
  61 }
  62
  63 void resetNodeInfoStatusSCC(OrderGraph *graph) {
  64         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  65         while (hasNextOrderNode(iterator)) {
  66                 nextOrderNode(iterator)->status = NOTVISITED;
  67         }
  68         deleteIterOrderNode(iterator);
  69 }
  70
  71 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
  72         VectorOrderNode finishNodes;
  73         initDefVectorOrderNode(&finishNodes);
  74         DFS(graph, &finishNodes);
  75         resetNodeInfoStatusSCC(graph);
  76         DFSReverse(graph, &finishNodes);
  77         resetNodeInfoStatusSCC(graph);
  78         deleteVectorArrayOrderNode(&finishNodes);
  79 }
  80
  81 void removeMustBeTrueNodes(OrderGraph *graph) {
  82         //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
  83 }
  84
  85 /** This function computes a source set for every nodes, the set of
  86                 nodes that can reach that node via pospolarity edges.  It then
  87                 looks for negative polarity edges from nodes in the the source set
  88                 to determine whether we need to generate pseudoPos edges. */
  89
  90 void completePartialOrderGraph(OrderGraph *graph) {
  91         VectorOrderNode finishNodes;
  92         initDefVectorOrderNode(&finishNodes);
  93         DFS(graph, &finishNodes);
  94         resetNodeInfoStatusSCC(graph);
  95         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
  96
  97         VectorOrderNode sccNodes;
  98         initDefVectorOrderNode(&sccNodes);
  99
 100         uint size = getSizeVectorOrderNode(&finishNodes);
 101         uint sccNum = 1;
 102         for (int i = size - 1; i >= 0; i--) {
 103                 OrderNode *node = getVectorOrderNode(&finishNodes, i);
 104                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
 105                 putNodeToNodeSet(table, node, sources);
 106
 107                 if (node->status == NOTVISITED) {
 108                         //Need to do reverse traversal here...
 109                         node->status = VISITED;
 110                         DFSNodeVisit(node, &sccNodes, true, sccNum);
 111                         node->status = FINISHED;
 112                         node->sccNum = sccNum;
 113                         sccNum++;
 114                         pushVectorOrderNode(&sccNodes, node);
 115
 116                         //Compute in set for entire SCC
 117                         uint rSize = getSizeVectorOrderNode(&sccNodes);
 118                         for (int j = 0; j < rSize; j++) {
 119                                 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
 120                                 //Compute source sets
 121                                 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
 122                                 while (hasNextOrderEdge(iterator)) {
 123                                         OrderEdge *edge = nextOrderEdge(iterator);
 124                                         OrderNode *parent = edge->source;
 125                                         if (edge->polPos) {
 126                                                 addHashSetOrderNode(sources, parent);
 127                                                 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
 128                                                 addAllHashSetOrderNode(sources, parent_srcs);
 129                                         }
 130                                 }
 131                                 deleteIterOrderEdge(iterator);
 132                         }
 133                         for (int j=0; j < rSize; j++) {
 134                                 //Copy in set of entire SCC
 135                                 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
 136                                 HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
 137                                 putNodeToNodeSet(table, rnode, set);
 138
 139                                 //Use source sets to compute pseudoPos edges
 140                                 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
 141                                 while (hasNextOrderEdge(iterator)) {
 142                                         OrderEdge *edge = nextOrderEdge(iterator);
 143                                         OrderNode *parent = edge->source;
 144                                         ASSERT(parent != rnode);
 145                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
 146                                                         containsHashSetOrderNode(sources, parent)) {
 147                                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
 148                                                 newedge->pseudoPos = true;
 149                                         }
 150                                 }
 151                                 deleteIterOrderEdge(iterator);
 152                         }
 153
 154                         clearVectorOrderNode(&sccNodes);
 155                 }
 156         }
 157
 158         resetAndDeleteHashTableNodeToNodeSet(table);
 159         resetNodeInfoStatusSCC(graph);
 160         deleteVectorArrayOrderNode(&sccNodes);
 161         deleteVectorArrayOrderNode(&finishNodes);
 162 }
 163
 164 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 165         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 166         while (hasNextOrderNode(iterator)) {
 167                 OrderNode *node = nextOrderNode(iterator);
 168                 if (node->status == NOTVISITED) {
 169                         node->status = VISITED;
 170                         DFSMustNodeVisit(node, finishNodes);
 171                         node->status = FINISHED;
 172                         pushVectorOrderNode(finishNodes, node);
 173                 }
 174         }
 175         deleteIterOrderNode(iterator);
 176 }
 177
 178 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
 179         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 180         while (hasNextOrderEdge(iterator)) {
 181                 OrderEdge *edge = nextOrderEdge(iterator);
 182                 OrderNode *child = edge->sink;
 183
 184                 if (!edge->mustPos)     //Ignore edges that are not must Positive edges
 185                         continue;
 186
 187                 if (child->status == NOTVISITED) {
 188                         child->status = VISITED;
 189                         DFSMustNodeVisit(child, finishNodes);
 190                         child->status = FINISHED;
 191                         pushVectorOrderNode(finishNodes, child);
 192                 }
 193         }
 194         deleteIterOrderEdge(iterator);
 195 }
 196
 197
 198 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
 199         uint size = getSizeVectorOrderNode(finishNodes);
 200         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
 201
 202         for (int i = size - 1; i >= 0; i--) {
 203                 OrderNode *node = getVectorOrderNode(finishNodes, i);
 204                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
 205                 putNodeToNodeSet(table, node, sources);
 206
 207                 {
 208                         //Compute source sets
 209                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 210                         while (hasNextOrderEdge(iterator)) {
 211                                 OrderEdge *edge = nextOrderEdge(iterator);
 212                                 OrderNode *parent = edge->source;
 213                                 if (edge->mustPos) {
 214                                         addHashSetOrderNode(sources, parent);
 215                                         HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
 216                                         addAllHashSetOrderNode(sources, parent_srcs);
 217                                 }
 218                         }
 219                         deleteIterOrderEdge(iterator);
 220                 }
 221                 if (computeTransitiveClosure) {
 222                         //Compute full transitive closure for nodes
 223                         HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
 224                         while (hasNextOrderNode(srciterator)) {
 225                                 OrderNode *srcnode = nextOrderNode(srciterator);
 226                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
 227                                 newedge->mustPos = true;
 228                                 newedge->polPos = true;
 229                                 if (newedge->mustNeg)
 230                                         solver->unsat = true;
 231                                 addHashSetOrderEdge(srcnode->outEdges,newedge);
 232                                 addHashSetOrderEdge(node->inEdges,newedge);
 233                         }
 234                         deleteIterOrderNode(srciterator);
 235                 }
 236                 {
 237                         //Use source sets to compute mustPos edges
 238                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 239                         while (hasNextOrderEdge(iterator)) {
 240                                 OrderEdge *edge = nextOrderEdge(iterator);
 241                                 OrderNode *parent = edge->source;
 242                                 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
 243                                         edge->mustPos = true;
 244                                         edge->polPos = true;
 245                                         if (edge->mustNeg)
 246                                                 solver->unsat = true;
 247                                 }
 248                         }
 249                         deleteIterOrderEdge(iterator);
 250                 }
 251                 {
 252                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 253                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 254                         while (hasNextOrderEdge(iterator)) {
 255                                 OrderEdge *edge = nextOrderEdge(iterator);
 256                                 OrderNode *child = edge->sink;
 257                                 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
 258                                         edge->mustNeg = true;
 259                                         edge->polNeg = true;
 260                                         if (edge->mustPos)
 261                                                 solver->unsat = true;
 262                                 }
 263                         }
 264                         deleteIterOrderEdge(iterator);
 265                 }
 266         }
 267
 268         resetAndDeleteHashTableNodeToNodeSet(table);
 269 }
 270
 271 /* This function finds edges that would form a cycle with must edges
 272    and forces them to be mustNeg.  It also decides whether an edge
 273    must be true because of transitivity from other must be true
 274    edges. */
 275
 276 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
 277         VectorOrderNode finishNodes;
 278         initDefVectorOrderNode(&finishNodes);
 279         //Topologically sort the mustPos edge graph
 280         DFSMust(graph, &finishNodes);
 281         resetNodeInfoStatusSCC(graph);
 282
 283         //Find any backwards edges that complete cycles and force them to be mustNeg
 284         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 285         deleteVectorArrayOrderNode(&finishNodes);
 286 }
 287
 288 /* This function finds edges that must be positive and forces the
 289    inverse edge to be negative (and clears its positive polarity if it
 290    had one). */
 291
 292 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 293         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 294         while (hasNextOrderEdge(iterator)) {
 295                 OrderEdge *edge = nextOrderEdge(iterator);
 296                 if (edge->mustPos) {
 297                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 298                         if (invEdge != NULL) {
 299                                 if (!invEdge->mustPos) {
 300                                         invEdge->polPos = false;
 301                                 } else {
 302                                         solver->unsat = true;
 303                                 }
 304                                 invEdge->mustNeg = true;
 305                                 invEdge->polNeg = true;
 306                         }
 307                 }
 308         }
 309         deleteIterOrderEdge(iterator);
 310 }
 311
 312 /** This finds edges that must be positive and forces the inverse edge
 313     to be negative.  It also clears the negative flag of this edge.
 314     It also finds edges that must be negative and clears the positive
 315     polarity. */
 316
 317 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 318         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 319         while (hasNextOrderEdge(iterator)) {
 320                 OrderEdge *edge = nextOrderEdge(iterator);
 321                 if (edge->mustPos) {
 322                         if (!edge->mustNeg) {
 323                                 edge->polNeg = false;
 324                         } else
 325                                 solver->unsat = true;
 326
 327                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 328                         if (invEdge != NULL) {
 329                                 if (!invEdge->mustPos)
 330                                         invEdge->polPos = false;
 331                                 else
 332                                         solver->unsat = true;
 333                                 invEdge->mustNeg = true;
 334                                 invEdge->polNeg = true;
 335                         }
 336                 }
 337                 if (edge->mustNeg && !edge->mustPos) {
 338                         edge->polPos = false;
 339                 }
 340         }
 341         deleteIterOrderEdge(iterator);
 342 }
 343
 344 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 345         VectorOrder ordervec;
 346         initDefVectorOrder(&ordervec);
 347         uint size = getSizeVectorBooleanOrder(&order->constraints);
 348         for (uint i = 0; i < size; i++) {
 349                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 350                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 351                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 352                 if (from->sccNum != to->sccNum) {
 353                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 354                         if (edge->polPos) {
 355                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
 356                         } else if (edge->polNeg) {
 357                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
 358                         } else {
 359                                 //This case should only be possible if constraint isn't in AST
 360                                 ASSERT(0);
 361                         }
 362                 } else {
 363                         //Build new order and change constraint's order
 364                         Order *neworder = NULL;
 365                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 366                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 367                         if (neworder == NULL) {
 368                                 Set *set = (Set *) allocMutableSet(order->set->type);
 369                                 neworder = allocOrder(order->type, set);
 370                                 pushVectorOrder(This->allOrders, neworder);
 371                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 372                         }
 373                         if (from->status != ADDEDTOSET) {
 374                                 from->status = ADDEDTOSET;
 375                                 addElementMSet((MutableSet *)neworder->set, from->id);
 376                         }
 377                         if (to->status != ADDEDTOSET) {
 378                                 to->status = ADDEDTOSET;
 379                                 addElementMSet((MutableSet *)neworder->set, to->id);
 380                         }
 381                         orderconstraint->order = neworder;
 382                         addOrderConstraint(neworder, orderconstraint);
 383                 }
 384         }
 385         deleteVectorArrayOrder(&ordervec);
 386 }
 387
 388 void orderAnalysis(CSolver *This) {
 389         uint size = getSizeVectorOrder(This->allOrders);
 390         for (uint i = 0; i < size; i++) {
 391                 Order *order = getVectorOrder(This->allOrders, i);
 392                 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
 393                 if (!doDecompose)
 394                         continue;
 395
 396                 OrderGraph *graph = buildOrderGraph(order);
 397                 if (order->type == PARTIAL) {
 398                         //Required to do SCC analysis for partial order graphs.  It
 399                         //makes sure we don't incorrectly optimize graphs with negative
 400                         //polarity edges
 401                         completePartialOrderGraph(graph);
 402                 }
 403
 404
 405                 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
 406
 407                 if (mustReachGlobal)
 408                         reachMustAnalysis(This, graph, false);
 409
 410                 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
 411
 412                 if (mustReachLocal) {
 413                         //This pair of analysis is also optional
 414                         if (order->type == PARTIAL) {
 415                                 localMustAnalysisPartial(This, graph);
 416                         } else {
 417                                 localMustAnalysisTotal(This, graph);
 418                         }
 419                 }
 420
 421                 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
 422
 423                 if (mustReachPrune)
 424                         removeMustBeTrueNodes(graph);
 425
 426                 //This is needed for splitorder
 427                 computeStronglyConnectedComponentGraph(graph);
 428
 429                 decomposeOrder(This, order, graph);
 430
 431                 deleteOrderGraph(graph);
 432         }
 433 }