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(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                                 addHashSetOrderEdge(srcnode->outEdges,newedge);
 209                                 addHashSetOrderEdge(node->inEdges,newedge);
 210                         }
 211                         deleteIterOrderNode(srciterator);
 212                 }
 213                 {
 214                         //Use source sets to compute mustPos edges
 215                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 216                         while (hasNextOrderEdge(iterator)) {
 217                                 OrderEdge *edge = nextOrderEdge(iterator);
 218                                 OrderNode *parent = edge->source;
 219                                 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
 220                                         edge->mustPos = true;
 221                                 }
 222                         }
 223                         deleteIterOrderEdge(iterator);
 224                 }
 225                 {
 226                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 227                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 228                         while (hasNextOrderEdge(iterator)) {
 229                                 OrderEdge *edge = nextOrderEdge(iterator);
 230                                 OrderNode *child = edge->sink;
 231                                 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
 232                                         edge->mustNeg = true;
 233                                 }
 234                         }
 235                         deleteIterOrderEdge(iterator);
 236                 }
 237         }
 238
 239         resetAndDeleteHashTableNodeToNodeSet(table);
 240 }
 241
 242 /* This function finds edges that would form a cycle with must edges
 243    and forces them to be mustNeg.  It also decides whether an edge
 244    must be true because of transitivity from other must be true
 245    edges. */
 246
 247 void reachMustAnalysis(OrderGraph *graph, bool computeTransitiveClosure) {
 248         VectorOrderNode finishNodes;
 249         initDefVectorOrderNode(&finishNodes);
 250         //Topologically sort the mustPos edge graph
 251         DFSMust(graph, &finishNodes);
 252         resetNodeInfoStatusSCC(graph);
 253
 254         //Find any backwards edges that complete cycles and force them to be mustNeg
 255         DFSClearContradictions(graph, &finishNodes, computeTransitiveClosure);
 256         deleteVectorArrayOrderNode(&finishNodes);
 257         resetNodeInfoStatusSCC(graph);
 258 }
 259
 260 /* This function finds edges that must be positive and forces the
 261    inverse edge to be negative (and clears its positive polarity if it
 262    had one). */
 263
 264 void localMustAnalysisTotal(OrderGraph *graph) {
 265         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 266         while (hasNextOrderEdge(iterator)) {
 267                 OrderEdge *edge = nextOrderEdge(iterator);
 268                 if (edge->mustPos) {
 269                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 270                         if (invEdge != NULL && !invEdge->mustPos && invEdge->polPos) {
 271                                 invEdge->polPos = false;
 272                         }
 273                         invEdge->mustNeg = true;
 274                 }
 275         }
 276         deleteIterOrderEdge(iterator);
 277 }
 278
 279 /** This finds edges that must be positive and forces the inverse edge
 280     to be negative.  It also clears the negative flag of this edge.
 281     It also finds edges that must be negative and clears the positive
 282     polarity. */
 283
 284 void localMustAnalysisPartial(OrderGraph *graph) {
 285         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 286         while (hasNextOrderEdge(iterator)) {
 287                 OrderEdge *edge = nextOrderEdge(iterator);
 288                 if (edge->mustPos) {
 289                         if (edge->polNeg && !edge->mustNeg) {
 290                                 edge->polNeg = false;
 291                         }
 292                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 293                         if (invEdge != NULL) {
 294                                 if (!invEdge->mustPos)
 295                                         invEdge->polPos = false;
 296                                 invEdge->mustNeg = true;
 297                         }
 298                 }
 299                 if (edge->mustNeg && !edge->mustPos) {
 300                         edge->polPos = false;
 301                 }
 302         }
 303         deleteIterOrderEdge(iterator);
 304 }
 305
 306 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 307         VectorOrder ordervec;
 308         initDefVectorOrder(&ordervec);
 309         uint size = getSizeVectorBooleanOrder(&order->constraints);
 310         for (uint i = 0; i < size; i++) {
 311                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 312                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 313                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 314                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 315                 if (from->sccNum < to->sccNum) {
 316                         //replace with true
 317                         replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
 318                 } else if (to->sccNum < from->sccNum) {
 319                         //replace with false
 320                         replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
 321                 } else {
 322                         //Build new order and change constraint's order
 323                         Order *neworder = NULL;
 324                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 325                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 326                         if (neworder == NULL) {
 327                                 Set *set = (Set *) allocMutableSet(order->set->type);
 328                                 neworder = allocOrder(order->type, set);
 329                                 pushVectorOrder(This->allOrders, neworder);
 330                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 331                         }
 332                         if (from->status != ADDEDTOSET) {
 333                                 from->status = ADDEDTOSET;
 334                                 addElementMSet((MutableSet *)neworder->set, from->id);
 335                         }
 336                         if (to->status != ADDEDTOSET) {
 337                                 to->status = ADDEDTOSET;
 338                                 addElementMSet((MutableSet *)neworder->set, to->id);
 339                         }
 340                         orderconstraint->order = neworder;
 341                         addOrderConstraint(neworder, orderconstraint);
 342                 }
 343         }
 344         deleteVectorArrayOrder(&ordervec);
 345 }
 346
 347 void orderAnalysis(CSolver *This) {
 348         uint size = getSizeVectorOrder(This->allOrders);
 349         for (uint i = 0; i < size; i++) {
 350                 Order *order = getVectorOrder(This->allOrders, i);
 351                 OrderGraph *graph = buildOrderGraph(order);
 352                 if (order->type == PARTIAL) {
 353                         //Required to do SCC analysis for partial order graphs.  It
 354                         //makes sure we don't incorrectly optimize graphs with negative
 355                         //polarity edges
 356                         completePartialOrderGraph(graph);
 357                 }
 358
 359                 //This analysis is completely optional
 360                 reachMustAnalysis(graph, false);
 361
 362                 //This pair of analysis is also optional
 363                 if (order->type == PARTIAL) {
 364                         localMustAnalysisPartial(graph);
 365                 } else {
 366                         localMustAnalysisTotal(graph);
 367                 }
 368
 369                 //This optimization is completely optional
 370                 removeMustBeTrueNodes(graph);
 371
 372                 //This is needed for splitorder
 373                 computeStronglyConnectedComponentGraph(graph);
 374
 375                 decomposeOrder(This, order, graph);
 376
 377                 deleteOrderGraph(graph);
 378         }
 379 }