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         deleteHashTableNodeToNodeSet(table);
 164         resetNodeInfoStatusSCC(graph);
 165         deleteVectorArrayOrderNode(&sccNodes);
 166         deleteVectorArrayOrderNode(&finishNodes);
 167 }
 168
 169 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 170         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 171         while (hasNextOrderNode(iterator)) {
 172                 OrderNode *node = nextOrderNode(iterator);
 173                 if (node->status == NOTVISITED) {
 174                         node->status = VISITED;
 175                         DFSNodeVisit(node, finishNodes, false, true, 0);
 176                         node->status = FINISHED;
 177                         pushVectorOrderNode(finishNodes, node);
 178                 }
 179         }
 180         deleteIterOrderNode(iterator);
 181 }
 182
 183 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
 184         uint size = getSizeVectorOrderNode(finishNodes);
 185         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
 186
 187         for (int i = size - 1; i >= 0; i--) {
 188                 OrderNode *node = getVectorOrderNode(finishNodes, i);
 189                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
 190                 putNodeToNodeSet(table, node, sources);
 191
 192                 {
 193                         //Compute source sets
 194                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 195                         while (hasNextOrderEdge(iterator)) {
 196                                 OrderEdge *edge = nextOrderEdge(iterator);
 197                                 OrderNode *parent = edge->source;
 198                                 if (edge->mustPos) {
 199                                         addHashSetOrderNode(sources, parent);
 200                                         HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
 201                                         addAllHashSetOrderNode(sources, parent_srcs);
 202                                 }
 203                         }
 204                         deleteIterOrderEdge(iterator);
 205                 }
 206                 if (computeTransitiveClosure) {
 207                         //Compute full transitive closure for nodes
 208                         HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
 209                         while (hasNextOrderNode(srciterator)) {
 210                                 OrderNode *srcnode = nextOrderNode(srciterator);
 211                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
 212                                 newedge->mustPos = true;
 213                                 newedge->polPos = true;
 214                                 if (newedge->mustNeg)
 215                                         solver->unsat = true;
 216                                 addHashSetOrderEdge(srcnode->outEdges,newedge);
 217                                 addHashSetOrderEdge(node->inEdges,newedge);
 218                         }
 219                         deleteIterOrderNode(srciterator);
 220                 }
 221                 {
 222                         //Use source sets to compute mustPos edges
 223                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 224                         while (hasNextOrderEdge(iterator)) {
 225                                 OrderEdge *edge = nextOrderEdge(iterator);
 226                                 OrderNode *parent = edge->source;
 227                                 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
 228                                         edge->mustPos = true;
 229                                         edge->polPos = true;
 230                                         if (edge->mustNeg)
 231                                                 solver->unsat = true;
 232                                 }
 233                         }
 234                         deleteIterOrderEdge(iterator);
 235                 }
 236                 {
 237                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 238                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 239                         while (hasNextOrderEdge(iterator)) {
 240                                 OrderEdge *edge = nextOrderEdge(iterator);
 241                                 OrderNode *child = edge->sink;
 242                                 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
 243                                         edge->mustNeg = true;
 244                                         edge->polNeg = true;
 245                                         if (edge->mustPos)
 246                                                 solver->unsat = true;
 247                                 }
 248                         }
 249                         deleteIterOrderEdge(iterator);
 250                 }
 251         }
 252
 253         resetAndDeleteHashTableNodeToNodeSet(table);
 254         deleteHashTableNodeToNodeSet(table);
 255 }
 256
 257 /* This function finds edges that would form a cycle with must edges
 258    and forces them to be mustNeg.  It also decides whether an edge
 259    must be true because of transitivity from other must be true
 260    edges. */
 261
 262 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
 263         VectorOrderNode finishNodes;
 264         initDefVectorOrderNode(&finishNodes);
 265         //Topologically sort the mustPos edge graph
 266         DFSMust(graph, &finishNodes);
 267         resetNodeInfoStatusSCC(graph);
 268
 269         //Find any backwards edges that complete cycles and force them to be mustNeg
 270         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 271         deleteVectorArrayOrderNode(&finishNodes);
 272 }
 273
 274 /* This function finds edges that must be positive and forces the
 275    inverse edge to be negative (and clears its positive polarity if it
 276    had one). */
 277
 278 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 279         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 280         while (hasNextOrderEdge(iterator)) {
 281                 OrderEdge *edge = nextOrderEdge(iterator);
 282                 if (edge->mustPos) {
 283                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 284                         if (invEdge != NULL) {
 285                                 if (!invEdge->mustPos) {
 286                                         invEdge->polPos = false;
 287                                 } else {
 288                                         solver->unsat = true;
 289                                 }
 290                                 invEdge->mustNeg = true;
 291                                 invEdge->polNeg = true;
 292                         }
 293                 }
 294         }
 295         deleteIterOrderEdge(iterator);
 296 }
 297
 298 /** This finds edges that must be positive and forces the inverse edge
 299     to be negative.  It also clears the negative flag of this edge.
 300     It also finds edges that must be negative and clears the positive
 301     polarity. */
 302
 303 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 304         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 305         while (hasNextOrderEdge(iterator)) {
 306                 OrderEdge *edge = nextOrderEdge(iterator);
 307                 if (edge->mustPos) {
 308                         if (!edge->mustNeg) {
 309                                 edge->polNeg = false;
 310                         } else
 311                                 solver->unsat = true;
 312
 313                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 314                         if (invEdge != NULL) {
 315                                 if (!invEdge->mustPos)
 316                                         invEdge->polPos = false;
 317                                 else
 318                                         solver->unsat = true;
 319                                 invEdge->mustNeg = true;
 320                                 invEdge->polNeg = true;
 321                         }
 322                 }
 323                 if (edge->mustNeg && !edge->mustPos) {
 324                         edge->polPos = false;
 325                 }
 326         }
 327         deleteIterOrderEdge(iterator);
 328 }
 329
 330 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 331         VectorOrder ordervec;
 332         VectorOrder partialcandidatevec;
 333         initDefVectorOrder(&ordervec);
 334         initDefVectorOrder(&partialcandidatevec);
 335         uint size = getSizeVectorBooleanOrder(&order->constraints);
 336         for (uint i = 0; i < size; i++) {
 337                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 338                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 339                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 340                 if (from->sccNum != to->sccNum) {
 341                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 342                         if (edge->polPos) {
 343                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
 344                         } else if (edge->polNeg) {
 345                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
 346                         } else {
 347                                 //This case should only be possible if constraint isn't in AST
 348                                 ASSERT(0);
 349                         }
 350                 } else {
 351                         //Build new order and change constraint's order
 352                         Order *neworder = NULL;
 353                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 354                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 355                         if (neworder == NULL) {
 356                                 Set *set = (Set *) allocMutableSet(order->set->type);
 357                                 neworder = allocOrder(order->type, set);
 358                                 pushVectorOrder(This->allOrders, neworder);
 359                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 360                                 if (order->type == PARTIAL)
 361                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder);
 362                                 else
 363                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
 364                         }
 365                         if (from->status != ADDEDTOSET) {
 366                                 from->status = ADDEDTOSET;
 367                                 addElementMSet((MutableSet *)neworder->set, from->id);
 368                         }
 369                         if (to->status != ADDEDTOSET) {
 370                                 to->status = ADDEDTOSET;
 371                                 addElementMSet((MutableSet *)neworder->set, to->id);
 372                         }
 373                         if (order->type == PARTIAL) {
 374                                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 375                                 if (edge->polNeg)
 376                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
 377                         }
 378                         orderconstraint->order = neworder;
 379                         addOrderConstraint(neworder, orderconstraint);
 380                 }
 381         }
 382
 383         uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
 384         for(uint i=0;i<pcvsize;i++) {
 385                 Order * neworder=getVectorOrder(&partialcandidatevec, i);
 386                 if (neworder != NULL)
 387                         neworder->type = TOTAL;
 388         }
 389
 390         deleteVectorArrayOrder(&ordervec);
 391         deleteVectorArrayOrder(&partialcandidatevec);
 392 }
 393
 394 void orderAnalysis(CSolver *This) {
 395         uint size = getSizeVectorOrder(This->allOrders);
 396         for (uint i = 0; i < size; i++) {
 397                 Order *order = getVectorOrder(This->allOrders, i);
 398                 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
 399                 if (!doDecompose)
 400                         continue;
 401
 402                 OrderGraph *graph = buildOrderGraph(order);
 403                 if (order->type == PARTIAL) {
 404                         //Required to do SCC analysis for partial order graphs.  It
 405                         //makes sure we don't incorrectly optimize graphs with negative
 406                         //polarity edges
 407                         completePartialOrderGraph(graph);
 408                 }
 409
 410
 411                 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
 412
 413                 if (mustReachGlobal)
 414                         reachMustAnalysis(This, graph, false);
 415
 416                 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
 417
 418                 if (mustReachLocal) {
 419                         //This pair of analysis is also optional
 420                         if (order->type == PARTIAL) {
 421                                 localMustAnalysisPartial(This, graph);
 422                         } else {
 423                                 localMustAnalysisTotal(This, graph);
 424                         }
 425                 }
 426
 427                 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
 428
 429                 if (mustReachPrune)
 430                         removeMustBeTrueNodes(graph);
 431
 432                 //This is needed for splitorder
 433                 computeStronglyConnectedComponentGraph(graph);
 434
 435                 decomposeOrder(This, order, graph);
 436
 437                 deleteOrderGraph(graph);
 438         }
 439 }