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