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, false);
 150                         node->status = FINISHED;
 151                         pushVectorOrderNode(finishNodes, node);
 152                 }
 153         }
 154         deleteIterOrderNode(iterator);
 155 }
 156
 157 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges) {
 158         //First compute implication of transitive closure on must pos edges
 159         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 160         while (hasNextOrderEdge(iterator)) {
 161                 OrderEdge *edge = nextOrderEdge(iterator);
 162                 OrderNode *parent = edge->source;
 163                 if (parent->status == VISITED) {
 164                         edge->mustPos = true;
 165                 }
 166         }
 167         deleteIterOrderEdge(iterator);
 168
 169         //Next compute implication of transitive closure on must neg edges
 170         iterator = iteratorOrderEdge(node->outEdges);
 171         while (hasNextOrderEdge(iterator)) {
 172                 OrderEdge *edge = nextOrderEdge(iterator);
 173                 OrderNode *child = edge->sink;
 174
 175                 if (clearBackEdges && child->status == VISITED) {
 176                         //We have a backedge, so note that this edge must be negative
 177                         edge->mustNeg = true;
 178                 }
 179
 180                 if (!edge->mustPos)     //Ignore edges that are not must Positive edges
 181                         continue;
 182
 183                 if (child->status == NOTVISITED) {
 184                         child->status = VISITED;
 185                         DFSMustNodeVisit(child, finishNodes, clearBackEdges);
 186                         child->status = FINISHED;
 187                         pushVectorOrderNode(finishNodes, child);
 188                 }
 189         }
 190         deleteIterOrderEdge(iterator);
 191 }
 192
 193 void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes) {
 194         uint size = getSizeVectorOrderNode(finishNodes);
 195         for (int i = size - 1; i >= 0; i--) {
 196                 OrderNode *node = getVectorOrderNode(finishNodes, i);
 197                 if (node->status == NOTVISITED) {
 198                         node->status = VISITED;
 199                         DFSMustNodeVisit(node, NULL, true);
 200                         node->status = FINISHED;
 201                 }
 202         }
 203 }
 204
 205 /* This function finds edges that would form a cycle with must edges
 206    and forces them to be mustNeg.  It also decides whether an edge
 207    must be true because of transitivity from other must be true
 208    edges. */
 209
 210 void reachMustAnalysis(OrderGraph *graph) {
 211         VectorOrderNode finishNodes;
 212         initDefVectorOrderNode(&finishNodes);
 213         //Topologically sort the mustPos edge graph
 214         DFSMust(graph, &finishNodes);
 215         resetNodeInfoStatusSCC(graph);
 216
 217         //Find any backwards edges that complete cycles and force them to be mustNeg
 218         DFSClearContradictions(graph, &finishNodes);
 219         deleteVectorArrayOrderNode(&finishNodes);
 220         resetNodeInfoStatusSCC(graph);
 221 }
 222
 223 /* This function finds edges that must be positive and forces the
 224    inverse edge to be negative (and clears its positive polarity if it
 225    had one). */
 226
 227 void localMustAnalysisTotal(OrderGraph *graph) {
 228         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 229         while (hasNextOrderEdge(iterator)) {
 230                 OrderEdge *edge = nextOrderEdge(iterator);
 231                 if (edge->mustPos) {
 232                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 233                         if (invEdge != NULL && !invEdge->mustPos && invEdge->polPos) {
 234                                 invEdge->polPos = false;
 235                         }
 236                         invEdge->mustNeg = true;
 237                 }
 238         }
 239         deleteIterOrderEdge(iterator);
 240 }
 241
 242 /** This finds edges that must be positive and forces the inverse edge
 243     to be negative.  It also clears the negative flag of this edge.
 244     It also finds edges that must be negative and clears the positive
 245     polarity. */
 246
 247 void localMustAnalysisPartial(OrderGraph *graph) {
 248         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 249         while (hasNextOrderEdge(iterator)) {
 250                 OrderEdge *edge = nextOrderEdge(iterator);
 251                 if (edge->mustPos) {
 252                         if (edge->polNeg && !edge->mustNeg) {
 253                                 edge->polNeg = false;
 254                         }
 255                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 256                         if (invEdge != NULL && !invEdge->mustPos) {
 257                                 invEdge->polPos = false;
 258                         }
 259                         invEdge->mustNeg = true;
 260                 }
 261                 if (edge->mustNeg && !edge->mustPos) {
 262                         edge->polPos = false;
 263                 }
 264         }
 265         deleteIterOrderEdge(iterator);
 266 }
 267
 268 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 269         VectorOrder ordervec;
 270         initDefVectorOrder(&ordervec);
 271         uint size = getSizeVectorBooleanOrder(&order->constraints);
 272         for (uint i = 0; i < size; i++) {
 273                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 274                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 275                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 276                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 277                 if (from->sccNum < to->sccNum) {
 278                         //replace with true
 279                         replaceBooleanWithTrue((Boolean *)orderconstraint);
 280                 } else if (to->sccNum < from->sccNum) {
 281                         //replace with false
 282                         replaceBooleanWithFalse((Boolean *)orderconstraint);
 283                 } else {
 284                         //Build new order and change constraint's order
 285                         Order * neworder = NULL;
 286                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 287                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 288                         if (neworder == NULL) {
 289                                 Set * set = (Set *) allocMutableSet(order->set->type);
 290                                 neworder = allocOrder(order->type, set);
 291                                 pushVectorOrder(This->allOrders, neworder);
 292                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 293                         }
 294                         if (from->status != ADDEDTOSET) {
 295                                 from->status = ADDEDTOSET;
 296                                 addElementMSet((MutableSet *)neworder->set, from->id);
 297                         }
 298                         if (to->status != ADDEDTOSET) {
 299                                 to->status = ADDEDTOSET;
 300                                 addElementMSet((MutableSet *)neworder->set, to->id);
 301                         }
 302                         orderconstraint->order = neworder;
 303                         addOrderConstraint(neworder, orderconstraint);
 304                 }
 305         }
 306         deleteVectorArrayOrder(&ordervec);
 307 }
 308
 309 void orderAnalysis(CSolver *This) {
 310         uint size = getSizeVectorOrder(This->allOrders);
 311         for (uint i = 0; i < size; i++) {
 312                 Order *order = getVectorOrder(This->allOrders, i);
 313                 OrderGraph *graph = buildOrderGraph(order);
 314                 if (order->type == PARTIAL) {
 315                         //Required to do SCC analysis for partial order graphs.  It
 316                         //makes sure we don't incorrectly optimize graphs with negative
 317                         //polarity edges
 318                         completePartialOrderGraph(graph);
 319                 }
 320
 321                 //This analysis is completely optional
 322                 reachMustAnalysis(graph);
 323
 324                 //This pair of analysis is also optional
 325                 if (order->type == PARTIAL) {
 326                         localMustAnalysisPartial(graph);
 327                 } else {
 328                         localMustAnalysisTotal(graph);
 329                 }
 330
 331                 //This optimization is completely optional
 332                 removeMustBeTrueNodes(graph);
 333
 334                 //This is needed for splitorder
 335                 computeStronglyConnectedComponentGraph(graph);
 336
 337                 decomposeOrder(This, order, graph);
 338
 339                 deleteOrderGraph(graph);
 340         }
 341 }