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