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
  10 OrderGraph *buildOrderGraph(Order *order) {
  11         OrderGraph *orderGraph = allocOrderGraph(order);
  12         uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
  13         for (uint j = 0; j < constrSize; j++) {
  14                 addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
  15         }
  16         return orderGraph;
  17 }
  18
  19 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
  20         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  21         while (hasNextOrderNode(iterator)) {
  22                 OrderNode *node = nextOrderNode(iterator);
  23                 if (node->status == NOTVISITED) {
  24                         node->status = VISITED;
  25                         DFSNodeVisit(node, finishNodes, false, 0);
  26                         node->status = FINISHED;
  27                         pushVectorOrderNode(finishNodes, node);
  28                 }
  29         }
  30         deleteIterOrderNode(iterator);
  31 }
  32
  33 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
  34         uint size = getSizeVectorOrderNode(finishNodes);
  35         uint sccNum = 1;
  36         for (int i = size - 1; i >= 0; i--) {
  37                 OrderNode *node = getVectorOrderNode(finishNodes, i);
  38                 if (node->status == NOTVISITED) {
  39                         node->status = VISITED;
  40                         DFSNodeVisit(node, NULL, true, sccNum);
  41                         node->sccNum = sccNum;
  42                         node->status = FINISHED;
  43                         sccNum++;
  44                 }
  45         }
  46 }
  47
  48 void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum) {
  49         HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
  50         while (hasNextOrderEdge(iterator)) {
  51                 OrderEdge *edge = nextOrderEdge(iterator);
  52                 if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
  53                         continue;
  54
  55                 OrderNode *child = isReverse ? edge->source : edge->sink;
  56
  57                 if (child->status == NOTVISITED) {
  58                         child->status = VISITED;
  59                         DFSNodeVisit(child, finishNodes, isReverse, sccNum);
  60                         child->status = FINISHED;
  61                         if (!isReverse)
  62                                 pushVectorOrderNode(finishNodes, child);
  63                         else
  64                                 child->sccNum = sccNum;
  65                 }
  66         }
  67         deleteIterOrderEdge(iterator);
  68 }
  69
  70 void resetNodeInfoStatusSCC(OrderGraph *graph) {
  71         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  72         while (hasNextOrderNode(iterator)) {
  73                 nextOrderNode(iterator)->status = NOTVISITED;
  74         }
  75         deleteIterOrderNode(iterator);
  76 }
  77
  78 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
  79         VectorOrderNode finishNodes;
  80         initDefVectorOrderNode(&finishNodes);
  81         DFS(graph, &finishNodes);
  82         resetNodeInfoStatusSCC(graph);
  83         DFSReverse(graph, &finishNodes);
  84         resetNodeInfoStatusSCC(graph);
  85         deleteVectorArrayOrderNode(&finishNodes);
  86 }
  87
  88 void removeMustBeTrueNodes(OrderGraph *graph) {
  89         //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
  90 }
  91
  92 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node) {
  93         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
  94         while (hasNextOrderEdge(iterator)) {
  95                 OrderEdge *inEdge = nextOrderEdge(iterator);
  96                 if (inEdge->polNeg) {
  97                         OrderNode *src = inEdge->source;
  98                         if (src->status == VISITED) {
  99                                 //Make a pseudoEdge to point backwards
 100                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
 101                                 newedge->pseudoPos = true;
 102                         }
 103                 }
 104         }
 105         deleteIterOrderEdge(iterator);
 106         iterator = iteratorOrderEdge(node->outEdges);
 107         while (hasNextOrderEdge(iterator)) {
 108                 OrderEdge *edge = nextOrderEdge(iterator);
 109                 if (!edge->polPos)//Ignore edges that do not have positive polarity
 110                         continue;
 111
 112                 OrderNode *child = edge->sink;
 113                 if (child->status == NOTVISITED) {
 114                         child->status = VISITED;
 115                         DFSPseudoNodeVisit(graph, child);
 116                         child->status = FINISHED;
 117                 }
 118         }
 119         deleteIterOrderEdge(iterator);
 120 }
 121
 122 void completePartialOrderGraph(OrderGraph *graph) {
 123         VectorOrderNode finishNodes;
 124         initDefVectorOrderNode(&finishNodes);
 125         DFS(graph, &finishNodes);
 126         resetNodeInfoStatusSCC(graph);
 127
 128         uint size = getSizeVectorOrderNode(&finishNodes);
 129         for (int i = size - 1; i >= 0; i--) {
 130                 OrderNode *node = getVectorOrderNode(&finishNodes, i);
 131                 if (node->status == NOTVISITED) {
 132                         node->status = VISITED;
 133                         DFSPseudoNodeVisit(graph, node);
 134                         node->status = FINISHED;
 135                 }
 136         }
 137
 138         resetNodeInfoStatusSCC(graph);
 139         deleteVectorArrayOrderNode(&finishNodes);
 140 }
 141
 142 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 143         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 144         while (hasNextOrderNode(iterator)) {
 145                 OrderNode *node = nextOrderNode(iterator);
 146                 if (node->status == NOTVISITED) {
 147                         node->status = VISITED;
 148                         DFSMustNodeVisit(node, finishNodes, false);
 149                         node->status = FINISHED;
 150                         pushVectorOrderNode(finishNodes, node);
 151                 }
 152         }
 153         deleteIterOrderNode(iterator);
 154 }
 155
 156 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges) {
 157         //First compute implication of transitive closure on must pos edges
 158         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 159         while (hasNextOrderEdge(iterator)) {
 160                 OrderEdge *edge = nextOrderEdge(iterator);
 161                 OrderNode *parent = edge->source;
 162                 if (parent->status == VISITED) {
 163                         edge->mustPos = true;
 164                 }
 165         }
 166         deleteIterOrderEdge(iterator);
 167
 168         //Next compute implication of transitive closure on must neg edges
 169         iterator = iteratorOrderEdge(node->outEdges);
 170         while (hasNextOrderEdge(iterator)) {
 171                 OrderEdge *edge = nextOrderEdge(iterator);
 172                 OrderNode *child = edge->sink;
 173
 174                 if (clearBackEdges && child->status == VISITED) {
 175                         //We have a backedge, so note that this edge must be negative
 176                         edge->mustNeg = true;
 177                 }
 178
 179                 if (!edge->mustPos)     //Ignore edges that are not must Positive edges
 180                         continue;
 181
 182                 if (child->status == NOTVISITED) {
 183                         child->status = VISITED;
 184                         DFSMustNodeVisit(child, finishNodes, clearBackEdges);
 185                         child->status = FINISHED;
 186                         pushVectorOrderNode(finishNodes, child);
 187                 }
 188         }
 189         deleteIterOrderEdge(iterator);
 190 }
 191
 192 void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes) {
 193         uint size = getSizeVectorOrderNode(finishNodes);
 194         for (int i = size - 1; i >= 0; i--) {
 195                 OrderNode *node = getVectorOrderNode(finishNodes, i);
 196                 if (node->status == NOTVISITED) {
 197                         node->status = VISITED;
 198                         DFSMustNodeVisit(node, NULL, true);
 199                         node->status = FINISHED;
 200                 }
 201         }
 202 }
 203
 204 /* This function finds edges that would form a cycle with must edges
 205    and forces them to be mustNeg.  It also decides whether an edge
 206    must be true because of transitivity from other must be true
 207    edges. */
 208
 209 void reachMustAnalysis(OrderGraph *graph) {
 210         VectorOrderNode finishNodes;
 211         initDefVectorOrderNode(&finishNodes);
 212         //Topologically sort the mustPos edge graph
 213         DFSMust(graph, &finishNodes);
 214         resetNodeInfoStatusSCC(graph);
 215
 216         //Find any backwards edges that complete cycles and force them to be mustNeg
 217         DFSClearContradictions(graph, &finishNodes);
 218         deleteVectorArrayOrderNode(&finishNodes);
 219         resetNodeInfoStatusSCC(graph);
 220 }
 221
 222 /* This function finds edges that must be positive and forces the
 223    inverse edge to be negative (and clears its positive polarity if it
 224    had one). */
 225
 226 void localMustAnalysisTotal(OrderGraph *graph) {
 227         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 228         while (hasNextOrderEdge(iterator)) {
 229                 OrderEdge *edge = nextOrderEdge(iterator);
 230                 if (edge->mustPos) {
 231                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 232                         if (invEdge != NULL && !invEdge->mustPos && invEdge->polPos) {
 233                                 invEdge->polPos = false;
 234                         }
 235                         invEdge->mustNeg = true;
 236                 }
 237         }
 238         deleteIterOrderEdge(iterator);
 239 }
 240
 241 /** This finds edges that must be positive and forces the inverse edge
 242     to be negative.  It also clears the negative flag of this edge.
 243     It also finds edges that must be negative and clears the positive
 244     polarity. */
 245
 246 void localMustAnalysisPartial(OrderGraph *graph) {
 247         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 248         while (hasNextOrderEdge(iterator)) {
 249                 OrderEdge *edge = nextOrderEdge(iterator);
 250                 if (edge->mustPos) {
 251                         if (edge->polNeg && !edge->mustNeg) {
 252                                 edge->polNeg = false;
 253                         }
 254                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 255                         if (invEdge != NULL && !invEdge->mustPos) {
 256                                 invEdge->polPos = false;
 257                         }
 258                         invEdge->mustNeg = true;
 259                 }
 260                 if (edge->mustNeg && !edge->mustPos) {
 261                         edge->polPos = false;
 262                 }
 263         }
 264         deleteIterOrderEdge(iterator);
 265 }
 266
 267 void decomposeOrder(Order *order, OrderGraph *graph) {
 268         uint size = getSizeVectorBooleanOrder(&order->constraints);
 269         for (uint i = 0; i < size; i++) {
 270                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 271                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 272                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 273                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 274                 if (from->sccNum < to->sccNum) {
 275                         //replace with true
 276                         replaceBooleanWithTrue((Boolean *)orderconstraint);
 277                 } else if (to->sccNum < from->sccNum) {
 278                         //replace with false
 279                         replaceBooleanWithFalse((Boolean *)orderconstraint);
 280                 } else {
 281                         //Build new order and change constraint's order
 282
 283                 }
 284         }
 285 }
 286
 287 void orderAnalysis(CSolver *This) {
 288         uint size = getSizeVectorOrder(This->allOrders);
 289         for (uint i = 0; i < size; i++) {
 290                 Order *order = getVectorOrder(This->allOrders, i);
 291                 OrderGraph *graph = buildOrderGraph(order);
 292                 if (order->type == PARTIAL) {
 293                         //Required to do SCC analysis for partial order graphs.  It
 294                         //makes sure we don't incorrectly optimize graphs with negative
 295                         //polarity edges
 296                         completePartialOrderGraph(graph);
 297                 }
 298
 299                 //This analysis is completely optional
 300                 reachMustAnalysis(graph);
 301
 302                 //This pair of analysis is also optional
 303                 if (order->type == PARTIAL) {
 304                         localMustAnalysisPartial(graph);
 305                 } else {
 306                         localMustAnalysisTotal(graph);
 307                 }
 308
 309                 //This optimization is completely optional
 310                 removeMustBeTrueNodes(graph);
 311
 312                 //This is needed for splitorder
 313                 computeStronglyConnectedComponentGraph(graph);
 314
 315                 decomposeOrder(order, graph);
 316
 317                 deleteOrderGraph(graph);
 318         }
 319 }