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 (!isReverse)
  63                                 pushVectorOrderNode(finishNodes, child);
  64                         else
  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 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node) {
  94         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
  95         while (hasNextOrderEdge(iterator)) {
  96                 OrderEdge *inEdge = nextOrderEdge(iterator);
  97                 if (inEdge->polNeg) {
  98                         OrderNode *src = inEdge->source;
  99                         if (src->status == VISITED) {
 100                                 //Make a pseudoEdge to point backwards
 101                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
 102                                 newedge->pseudoPos = true;
 103                         }
 104                 }
 105         }
 106         deleteIterOrderEdge(iterator);
 107         iterator = iteratorOrderEdge(node->outEdges);
 108         while (hasNextOrderEdge(iterator)) {
 109                 OrderEdge *edge = nextOrderEdge(iterator);
 110                 if (!edge->polPos)//Ignore edges that do not have positive polarity
 111                         continue;
 112
 113                 OrderNode *child = edge->sink;
 114                 if (child->status == NOTVISITED) {
 115                         child->status = VISITED;
 116                         DFSPseudoNodeVisit(graph, child);
 117                         child->status = FINISHED;
 118                 }
 119         }
 120         deleteIterOrderEdge(iterator);
 121 }
 122
 123 void completePartialOrderGraph(OrderGraph *graph) {
 124         VectorOrderNode finishNodes;
 125         initDefVectorOrderNode(&finishNodes);
 126         DFS(graph, &finishNodes);
 127         resetNodeInfoStatusSCC(graph);
 128
 129         uint size = getSizeVectorOrderNode(&finishNodes);
 130         for (int i = size - 1; i >= 0; i--) {
 131                 OrderNode *node = getVectorOrderNode(&finishNodes, i);
 132                 if (node->status == NOTVISITED) {
 133                         node->status = VISITED;
 134                         DFSPseudoNodeVisit(graph, node);
 135                         node->status = FINISHED;
 136                 }
 137         }
 138
 139         resetNodeInfoStatusSCC(graph);
 140         deleteVectorArrayOrderNode(&finishNodes);
 141 }
 142
 143 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 144         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 145         while (hasNextOrderNode(iterator)) {
 146                 OrderNode *node = nextOrderNode(iterator);
 147                 if (node->status == NOTVISITED) {
 148                         node->status = VISITED;
 149                         DFSMustNodeVisit(node, finishNodes);
 150                         node->status = FINISHED;
 151                         pushVectorOrderNode(finishNodes, node);
 152                 }
 153         }
 154         deleteIterOrderNode(iterator);
 155 }
 156
 157 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
 158         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 159         while (hasNextOrderEdge(iterator)) {
 160                 OrderEdge *edge = nextOrderEdge(iterator);
 161                 OrderNode *child = edge->sink;
 162
 163                 if (!edge->mustPos)     //Ignore edges that are not must Positive edges
 164                         continue;
 165
 166                 if (child->status == NOTVISITED) {
 167                         child->status = VISITED;
 168                         DFSMustNodeVisit(child, finishNodes);
 169                         child->status = FINISHED;
 170                         pushVectorOrderNode(finishNodes, child);
 171                 }
 172         }
 173         deleteIterOrderEdge(iterator);
 174 }
 175
 176
 177 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
 178         uint size = getSizeVectorOrderNode(finishNodes);
 179         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
 180
 181         for (int i = size - 1; i >= 0; i--) {
 182                 OrderNode *node = getVectorOrderNode(finishNodes, i);
 183                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
 184                 putNodeToNodeSet(table, node, sources);
 185
 186                 {
 187                         //Compute source sets
 188                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 189                         while (hasNextOrderEdge(iterator)) {
 190                                 OrderEdge *edge = nextOrderEdge(iterator);
 191                                 OrderNode *parent = edge->source;
 192                                 if (edge->mustPos) {
 193                                         addHashSetOrderNode(sources, parent);
 194                                         HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
 195                                         addAllHashSetOrderNode(sources, parent_srcs);
 196                                 }
 197                         }
 198                         deleteIterOrderEdge(iterator);
 199                 }
 200                 if (computeTransitiveClosure) {
 201                         //Compute full transitive closure for nodes
 202                         HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
 203                         while (hasNextOrderNode(srciterator)) {
 204                                 OrderNode *srcnode = nextOrderNode(srciterator);
 205                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
 206                                 newedge->mustPos = true;
 207                                 newedge->polPos = true;
 208                                 if (newedge->mustNeg)
 209                                         solver->unsat = true;
 210                                 addHashSetOrderEdge(srcnode->outEdges,newedge);
 211                                 addHashSetOrderEdge(node->inEdges,newedge);
 212                         }
 213                         deleteIterOrderNode(srciterator);
 214                 }
 215                 {
 216                         //Use source sets to compute mustPos edges
 217                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 218                         while (hasNextOrderEdge(iterator)) {
 219                                 OrderEdge *edge = nextOrderEdge(iterator);
 220                                 OrderNode *parent = edge->source;
 221                                 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
 222                                         edge->mustPos = true;
 223                                         edge->polPos = true;
 224                                         if (edge->mustNeg)
 225                                                 solver->unsat = true;
 226                                 }
 227                         }
 228                         deleteIterOrderEdge(iterator);
 229                 }
 230                 {
 231                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 232                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 233                         while (hasNextOrderEdge(iterator)) {
 234                                 OrderEdge *edge = nextOrderEdge(iterator);
 235                                 OrderNode *child = edge->sink;
 236                                 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
 237                                         edge->mustNeg = true;
 238                                         edge->polNeg = true;
 239                                         if (edge->mustPos)
 240                                                 solver->unsat = true;
 241                                 }
 242                         }
 243                         deleteIterOrderEdge(iterator);
 244                 }
 245         }
 246
 247         resetAndDeleteHashTableNodeToNodeSet(table);
 248 }
 249
 250 /* This function finds edges that would form a cycle with must edges
 251    and forces them to be mustNeg.  It also decides whether an edge
 252    must be true because of transitivity from other must be true
 253    edges. */
 254
 255 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
 256         VectorOrderNode finishNodes;
 257         initDefVectorOrderNode(&finishNodes);
 258         //Topologically sort the mustPos edge graph
 259         DFSMust(graph, &finishNodes);
 260         resetNodeInfoStatusSCC(graph);
 261
 262         //Find any backwards edges that complete cycles and force them to be mustNeg
 263         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 264         deleteVectorArrayOrderNode(&finishNodes);
 265         resetNodeInfoStatusSCC(graph);
 266 }
 267
 268 /* This function finds edges that must be positive and forces the
 269    inverse edge to be negative (and clears its positive polarity if it
 270    had one). */
 271
 272 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 273         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 274         while (hasNextOrderEdge(iterator)) {
 275                 OrderEdge *edge = nextOrderEdge(iterator);
 276                 if (edge->mustPos) {
 277                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 278                         if (invEdge != NULL) {
 279                                 if (!invEdge->mustPos) {
 280                                         invEdge->polPos = false;
 281                                 } else {
 282                                         solver->unsat = true;
 283                                 }
 284                                 invEdge->mustNeg = true;
 285                                 invEdge->polNeg = true;
 286                         }
 287                 }
 288         }
 289         deleteIterOrderEdge(iterator);
 290 }
 291
 292 /** This finds edges that must be positive and forces the inverse edge
 293     to be negative.  It also clears the negative flag of this edge.
 294     It also finds edges that must be negative and clears the positive
 295     polarity. */
 296
 297 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 298         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 299         while (hasNextOrderEdge(iterator)) {
 300                 OrderEdge *edge = nextOrderEdge(iterator);
 301                 if (edge->mustPos) {
 302                         if (!edge->mustNeg) {
 303                                 edge->polNeg = false;
 304                         }
 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                                 invEdge->mustNeg = true;
 312                                 invEdge->polNeg = true;
 313                         }
 314                 }
 315                 if (edge->mustNeg && !edge->mustPos) {
 316                         edge->polPos = false;
 317                 }
 318         }
 319         deleteIterOrderEdge(iterator);
 320 }
 321
 322 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 323         VectorOrder ordervec;
 324         initDefVectorOrder(&ordervec);
 325         uint size = getSizeVectorBooleanOrder(&order->constraints);
 326         for (uint i = 0; i < size; i++) {
 327                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 328                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 329                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 330                 if (from->sccNum != to->sccNum) {
 331                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 332                         if (edge->polPos) {
 333                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
 334                         } else if (edge->polNeg) {
 335                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
 336                         } else {
 337                                 //This case should only be possible if constraint isn't in AST
 338                                 ASSERT(0);
 339                         }
 340                 } else {
 341                         //Build new order and change constraint's order
 342                         Order *neworder = NULL;
 343                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 344                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 345                         if (neworder == NULL) {
 346                                 Set *set = (Set *) allocMutableSet(order->set->type);
 347                                 neworder = allocOrder(order->type, set);
 348                                 pushVectorOrder(This->allOrders, neworder);
 349                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 350                         }
 351                         if (from->status != ADDEDTOSET) {
 352                                 from->status = ADDEDTOSET;
 353                                 addElementMSet((MutableSet *)neworder->set, from->id);
 354                         }
 355                         if (to->status != ADDEDTOSET) {
 356                                 to->status = ADDEDTOSET;
 357                                 addElementMSet((MutableSet *)neworder->set, to->id);
 358                         }
 359                         orderconstraint->order = neworder;
 360                         addOrderConstraint(neworder, orderconstraint);
 361                 }
 362         }
 363         deleteVectorArrayOrder(&ordervec);
 364 }
 365
 366 void orderAnalysis(CSolver *This) {
 367         uint size = getSizeVectorOrder(This->allOrders);
 368         for (uint i = 0; i < size; i++) {
 369                 Order *order = getVectorOrder(This->allOrders, i);
 370                 OrderGraph *graph = buildOrderGraph(order);
 371                 if (order->type == PARTIAL) {
 372                         //Required to do SCC analysis for partial order graphs.  It
 373                         //makes sure we don't incorrectly optimize graphs with negative
 374                         //polarity edges
 375                         completePartialOrderGraph(graph);
 376                 }
 377
 378                 //This analysis is completely optional
 379                 reachMustAnalysis(This, graph, false);
 380
 381                 //This pair of analysis is also optional
 382                 if (order->type == PARTIAL) {
 383                         localMustAnalysisPartial(This, graph);
 384                 } else {
 385                         localMustAnalysisTotal(This, graph);
 386                 }
 387
 388                 //This optimization is completely optional
 389                 removeMustBeTrueNodes(graph);
 390
 391                 //This is needed for splitorder
 392                 computeStronglyConnectedComponentGraph(graph);
 393
 394                 decomposeOrder(This, order, graph);
 395
 396                 deleteOrderGraph(graph);
 397         }
 398 }