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                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
 341                 if (from->sccNum != to->sccNum) {
 342                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 343                         if (edge->polPos) {
 344                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
 345                         } else if (edge->polNeg) {
 346                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
 347                         } else {
 348                                 //This case should only be possible if constraint isn't in AST
 349                                 ASSERT(0);
 350                         }
 351                 } else {
 352                         //Build new order and change constraint's order
 353                         Order *neworder = NULL;
 354                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 355                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 356                         if (neworder == NULL) {
 357                                 Set *set = (Set *) allocMutableSet(order->set->type);
 358                                 neworder = allocOrder(order->type, set);
 359                                 pushVectorOrder(This->allOrders, neworder);
 360                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 361                                 if (order->type == PARTIAL)
 362                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder);
 363                                 else
 364                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
 365                         }
 366                         if (from->status != ADDEDTOSET) {
 367                                 from->status = ADDEDTOSET;
 368                                 addElementMSet((MutableSet *)neworder->set, from->id);
 369                         }
 370                         if (to->status != ADDEDTOSET) {
 371                                 to->status = ADDEDTOSET;
 372                                 addElementMSet((MutableSet *)neworder->set, to->id);
 373                         }
 374                         if (order->type == PARTIAL) {
 375                                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 376                                 if (edge->polNeg)
 377                                         setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
 378                         }
 379                         orderconstraint->order = neworder;
 380                         addOrderConstraint(neworder, orderconstraint);
 381                 }
 382         }
 383
 384         uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
 385         for(uint i=0;i<pcvsize;i++) {
 386                 Order * neworder=getVectorOrder(&partialcandidatevec, i);
 387                 if (neworder != NULL){
 388                         neworder->type = TOTAL;
 389                         model_print("i=%u\t", i);
 390                 }
 391         }
 392
 393         deleteVectorArrayOrder(&ordervec);
 394         deleteVectorArrayOrder(&partialcandidatevec);
 395 }
 396
 397 void orderAnalysis(CSolver *This) {
 398         uint size = getSizeVectorOrder(This->allOrders);
 399         for (uint i = 0; i < size; i++) {
 400                 Order *order = getVectorOrder(This->allOrders, i);
 401                 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
 402                 if (!doDecompose)
 403                         continue;
 404
 405                 OrderGraph *graph = buildOrderGraph(order);
 406                 if (order->type == PARTIAL) {
 407                         //Required to do SCC analysis for partial order graphs.  It
 408                         //makes sure we don't incorrectly optimize graphs with negative
 409                         //polarity edges
 410                         completePartialOrderGraph(graph);
 411                 }
 412
 413
 414                 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
 415
 416                 if (mustReachGlobal)
 417                         reachMustAnalysis(This, graph, false);
 418
 419                 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
 420
 421                 if (mustReachLocal) {
 422                         //This pair of analysis is also optional
 423                         if (order->type == PARTIAL) {
 424                                 localMustAnalysisPartial(This, graph);
 425                         } else {
 426                                 localMustAnalysisTotal(This, graph);
 427                         }
 428                 }
 429
 430                 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
 431
 432                 if (mustReachPrune)
 433                         removeMustBeTrueNodes(graph);
 434
 435                 //This is needed for splitorder
 436                 computeStronglyConnectedComponentGraph(graph);
 437
 438                 decomposeOrder(This, order, graph);
 439
 440                 deleteOrderGraph(graph);
 441         }
 442 }