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 = 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         HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->outEdges);
 158         while(hasNextOrderEdge(iterator)){
 159                 OrderEdge* edge = nextOrderEdge(iterator);
 160                 OrderNode* child = edge->sink;
 161
 162                 if (clearBackEdges && child->status==VISITED) {
 163                         //We have a backedge, so note that this edge must be negative
 164                         edge->mustNeg = true;
 165                 }
 166
 167                 if (!edge->mustPos) //Ignore edges that are not must Positive edges
 168                         continue;
 169
 170                 if(child->status == NOTVISITED){
 171                         child->status = VISITED;
 172                         DFSMustNodeVisit(child, finishNodes, clearBackEdges);
 173                         child->status = FINISHED;
 174                         pushVectorOrderNode(finishNodes, child);
 175                 }
 176         }
 177         deleteIterOrderEdge(iterator);
 178 }
 179
 180 void DFSClearContradictions(OrderGraph* graph, VectorOrderNode* finishNodes) {
 181         uint size=getSizeVectorOrderNode(finishNodes);
 182         for(int i=size-1; i>=0; i--){
 183                 OrderNode* node=getVectorOrderNode(finishNodes, i);
 184                 if(node->status == NOTVISITED){
 185                         node->status = VISITED;
 186                         DFSMustNodeVisit(node, NULL, true);
 187                         node->status = FINISHED;
 188                 }
 189         }
 190 }
 191
 192 /* This function finds edges that would form a cycle with must edges
 193          and forces them to be mustNeg. */
 194
 195 void reachMustAnalysis(OrderGraph *graph) {
 196         VectorOrderNode finishNodes;
 197         initDefVectorOrderNode(& finishNodes);
 198         //Topologically sort the mustPos edge graph
 199         DFSMust(graph, &finishNodes);
 200         resetNodeInfoStatusSCC(graph);
 201
 202         //Find any backwards edges that complete cycles and force them to be mustNeg
 203         DFSClearContradictions(graph, &finishNodes);
 204         deleteVectorArrayOrderNode(&finishNodes);
 205         resetNodeInfoStatusSCC(graph);
 206 }
 207
 208 /* This function finds edges that must be positive and forces the
 209          inverse edge to be negative (and clears its positive polarity if it
 210          had one). */
 211
 212 void localMustAnalysisTotal(OrderGraph *graph) {
 213         HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
 214         while(hasNextOrderEdge(iterator)) {
 215                 OrderEdge *edge = nextOrderEdge(iterator);
 216                 if (edge -> mustPos) {
 217                         OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
 218                         if (invEdge!= NULL && !invEdge -> mustPos && invEdge->polPos) {
 219                                 invEdge->polPos = false;
 220                         }
 221                         invEdge->mustNeg = true;
 222                 }
 223         }
 224         deleteIterOrderEdge(iterator);
 225 }
 226
 227 /** This finds edges that must be positive and forces the inverse edge
 228                 to be negative.  It also clears the negative flag of this edge.
 229                 It also finds edges that must be negative and clears the positive
 230                 polarity. */
 231
 232 void localMustAnalysisPartial(OrderGraph *graph) {
 233         HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
 234         while(hasNextOrderEdge(iterator)) {
 235                 OrderEdge *edge = nextOrderEdge(iterator);
 236                 if (edge -> mustPos) {
 237                         if (edge->polNeg && !edge->mustNeg) {
 238                                 edge->polNeg = false;
 239                         }
 240                         OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
 241                         if (invEdge != NULL && !invEdge -> mustPos) {
 242                                 invEdge->polPos = false;
 243                         }
 244                         invEdge->mustNeg = true;
 245                 }
 246                 if (edge->mustNeg && !edge->mustPos) {
 247                         edge->polPos = false;
 248                 }
 249         }
 250         deleteIterOrderEdge(iterator);
 251 }
 252
 253 void decomposeOrder(Order *order, OrderGraph *graph) {
 254         uint size=getSizeVectorBooleanOrder(&order->constraints);
 255         for(uint i=0;i<size;i++) {
 256         }
 257 }
 258
 259 void orderAnalysis(CSolver* This) {
 260         uint size = getSizeVectorOrder(This->allOrders);
 261         for(uint i=0; i<size; i++){
 262                 Order* order = getVectorOrder(This->allOrders, i);
 263                 OrderGraph* graph = buildOrderGraph(order);
 264                 if (order->type==PARTIAL) {
 265                         //Required to do SCC analysis for partial order graphs.  It
 266                         //makes sure we don't incorrectly optimize graphs with negative
 267                         //polarity edges
 268                         completePartialOrderGraph(graph);
 269                 }
 270
 271                 //This analysis is completely optional
 272                 reachMustAnalysis(graph);
 273
 274                 //This pair of analysis is also optional
 275                 if (order->type==PARTIAL) {
 276                         localMustAnalysisPartial(graph);
 277                 } else {
 278                         localMustAnalysisTotal(graph);
 279                 }
 280
 281                 //This optimization is completely optional
 282                 removeMustBeTrueNodes(graph);
 283
 284                 //This is needed for splitorder
 285                 computeStronglyConnectedComponentGraph(graph);
 286
 287                 decomposeOrder(order, graph);
 288
 289                 deleteOrderGraph(graph);
 290         }
 291 }