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