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