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
   9
  10 OrderGraph* buildOrderGraph(Order *order) {
  11         OrderGraph* orderGraph = allocOrderGraph(order);
  12         uint constrSize = getSizeVectorBoolean(&order->constraints);
  13         for(uint j=0; j<constrSize; j++){
  14                 addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&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);
  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         for(int i=size-1; i>=0; i--){
  36                 OrderNode* node = getVectorOrderNode(finishNodes, i);
  37                 if(node->status == NOTVISITED){
  38                         node->status = VISITED;
  39                         DFSNodeVisit(node, NULL, true);
  40                         node->status = FINISHED;
  41                         pushVectorOrderNode(&graph->scc, node);
  42                 }
  43         }
  44 }
  45
  46 void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse) {
  47         HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
  48         while(hasNextOrderEdge(iterator)){
  49                 OrderEdge* edge = nextOrderEdge(iterator);
  50                 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
  51                         continue;
  52
  53                 OrderNode* child = isReverse? edge->source: edge->sink;
  54
  55                 if(child->status == NOTVISITED){
  56                         child->status = VISITED;
  57                         DFSNodeVisit(child, finishNodes, isReverse);
  58                         child->status = FINISHED;
  59                         if(!isReverse)
  60                                 pushVectorOrderNode(finishNodes, child);
  61                 }
  62         }
  63         deleteIterOrderEdge(iterator);
  64 }
  65
  66 void resetNodeInfoStatusSCC(OrderGraph* graph) {
  67         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
  68         while(hasNextOrderNode(iterator)){
  69                 nextOrderNode(iterator)->status = NOTVISITED;
  70         }
  71         deleteIterOrderNode(iterator);
  72 }
  73
  74 void computeStronglyConnectedComponentGraph(OrderGraph* graph) {
  75         VectorOrderNode finishNodes;
  76         initDefVectorOrderNode(& finishNodes);
  77         DFS(graph, &finishNodes);
  78         resetNodeInfoStatusSCC(graph);
  79         DFSReverse(graph, &finishNodes);
  80         resetNodeInfoStatusSCC(graph);
  81         deleteVectorArrayOrderNode(&finishNodes);
  82 }
  83
  84 void removeMustBeTrueNodes(OrderGraph* graph) {
  85         //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
  86 }
  87
  88 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode* node) {
  89         HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges);
  90         while(hasNextOrderEdge(iterator)){
  91                 OrderEdge* inEdge = nextOrderEdge(iterator);
  92                 if (inEdge->polNeg) {
  93                         OrderNode* src = inEdge->source;
  94                         if (src->status==VISITED) {
  95                                 //Make a pseudoEdge to point backwards
  96                                 OrderEdge * newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
  97                                 newedge->pseudoPos = true;
  98                         }
  99                 }
 100         }
 101         deleteIterOrderEdge(iterator);
 102         iterator = iteratorOrderEdge(node->outEdges);
 103         while(hasNextOrderEdge(iterator)){
 104                 OrderEdge* edge = nextOrderEdge(iterator);
 105                 if (!edge->polPos) //Ignore edges that do not have positive polarity
 106                         continue;
 107
 108                 OrderNode* child = edge->sink;
 109                 if(child->status == NOTVISITED){
 110                         child->status = VISITED;
 111                         DFSPseudoNodeVisit(graph, child);
 112                         child->status = FINISHED;
 113                 }
 114         }
 115         deleteIterOrderEdge(iterator);
 116 }
 117
 118 void completePartialOrderGraph(OrderGraph* graph) {
 119         VectorOrderNode finishNodes;
 120         initDefVectorOrderNode(& finishNodes);
 121         DFS(graph, &finishNodes);
 122         resetNodeInfoStatusSCC(graph);
 123
 124         uint size = getSizeVectorOrderNode(&finishNodes);
 125         for(int i=size-1; i>=0; i--){
 126                 OrderNode* node = getVectorOrderNode(&finishNodes, i);
 127                 if(node->status == NOTVISITED){
 128                         node->status = VISITED;
 129                         DFSPseudoNodeVisit(graph, node);
 130                         node->status = FINISHED;
 131                 }
 132         }
 133
 134         resetNodeInfoStatusSCC(graph);
 135         deleteVectorArrayOrderNode(&finishNodes);
 136 }
 137
 138 void DFSMust(OrderGraph* graph, VectorOrderNode* finishNodes) {
 139         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
 140         while(hasNextOrderNode(iterator)){
 141                 OrderNode* node = nextOrderNode(iterator);
 142                 if(node->status == NOTVISITED){
 143                         node->status = VISITED;
 144                         DFSMustNodeVisit(node, finishNodes, false);
 145                         node->status = FINISHED;
 146                         pushVectorOrderNode(finishNodes, node);
 147                 }
 148         }
 149         deleteIterOrderNode(iterator);
 150 }
 151
 152 void DFSMustNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool clearBackEdges) {
 153         HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->outEdges);
 154         while(hasNextOrderEdge(iterator)){
 155                 OrderEdge* edge = nextOrderEdge(iterator);
 156                 OrderNode* child = edge->sink;
 157
 158                 if (clearBackEdges && child->status==VISITED) {
 159                         //We have a backedge, so note that this edge must be negative
 160                         edge->mustNeg = true;
 161                 }
 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, clearBackEdges);
 169                         child->status = FINISHED;
 170                         pushVectorOrderNode(finishNodes, child);
 171                 }
 172         }
 173         deleteIterOrderEdge(iterator);
 174 }
 175
 176 void DFSClearContradictions(OrderGraph* graph, VectorOrderNode* finishNodes) {
 177         uint size=getSizeVectorOrderNode(finishNodes);
 178         for(int i=size-1; i>=0; i--){
 179                 OrderNode* node=getVectorOrderNode(finishNodes, i);
 180                 if(node->status == NOTVISITED){
 181                         node->status = VISITED;
 182                         DFSMustNodeVisit(node, NULL, true);
 183                         node->status = FINISHED;
 184                 }
 185         }
 186 }
 187
 188 /* This function finds edges that would form a cycle with must edges
 189          and forces them to be mustNeg. */
 190
 191 void reachMustAnalysis(OrderGraph *graph) {
 192         VectorOrderNode finishNodes;
 193         initDefVectorOrderNode(& finishNodes);
 194         //Topologically sort the mustPos edge graph
 195         DFSMust(graph, &finishNodes);
 196         resetNodeInfoStatusSCC(graph);
 197
 198         //Find any backwards edges that complete cycles and force them to be mustNeg
 199         DFSClearContradictions(graph, &finishNodes);
 200         deleteVectorArrayOrderNode(&finishNodes);
 201         resetNodeInfoStatusSCC(graph);
 202 }
 203
 204 /* This function finds edges that must be positive and forces the
 205          inverse edge to be negative (and clears its positive polarity if it
 206          had one). */
 207
 208 void localMustAnalysisTotal(OrderGraph *graph) {
 209         HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
 210         while(hasNextOrderEdge(iterator)) {
 211                 OrderEdge *edge = nextOrderEdge(iterator);
 212                 if (edge -> mustPos) {
 213                         OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
 214                         if (invEdge!= NULL && !invEdge -> mustPos && invEdge->polPos) {
 215                                 invEdge->polPos = false;
 216                         }
 217                         invEdge->mustNeg = true;
 218                 }
 219         }
 220         deleteIterOrderEdge(iterator);
 221 }
 222
 223 /** This finds edges that must be positive and forces the inverse edge
 224                 to be negative.  It also clears the negative flag of this edge.
 225                 It also finds edges that must be negative and clears the positive
 226                 polarity. */
 227
 228 void localMustAnalysisPartial(OrderGraph *graph) {
 229         HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
 230         while(hasNextOrderEdge(iterator)) {
 231                 OrderEdge *edge = nextOrderEdge(iterator);
 232                 if (edge -> mustPos) {
 233                         if (edge->polNeg && !edge->mustNeg) {
 234                                 edge->polNeg = false;
 235                         }
 236                         OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
 237                         if (invEdge != NULL && !invEdge -> mustPos) {
 238                                 invEdge->polPos = false;
 239                         }
 240                         invEdge->mustNeg = true;
 241                 }
 242                 if (edge->mustNeg && !edge->mustPos) {
 243                         edge->polPos = false;
 244                 }
 245         }
 246         deleteIterOrderEdge(iterator);
 247 }
 248
 249 void orderAnalysis(CSolver* This) {
 250         uint size = getSizeVectorOrder(This->allOrders);
 251         for(uint i=0; i<size; i++){
 252                 Order* order = getVectorOrder(This->allOrders, i);
 253                 OrderGraph* graph = buildOrderGraph(order);
 254                 if (order->type==PARTIAL) {
 255                         //Required to do SCC analysis for partial order graphs.  It
 256                         //makes sure we don't incorrectly optimize graphs with negative
 257                         //polarity edges
 258                         completePartialOrderGraph(graph);
 259                 }
 260
 261                 //This analysis is completely optional
 262                 reachMustAnalysis(graph);
 263
 264                 //This pair of analysis is also optional
 265                 if (order->type==PARTIAL) {
 266                         localMustAnalysisPartial(graph);
 267                 } else {
 268                         localMustAnalysisTotal(graph);
 269                 }
 270
 271                 //This analysis is completely optional
 272                 removeMustBeTrueNodes(graph);
 273
 274                 computeStronglyConnectedComponentGraph(graph);
 275                 deleteOrderGraph(graph);
 276         }
 277 }