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->finishTime = 0;
  13         This->status = NOTVISITED;
  14         return This;
  15 }
  16
  17 void deleteNodeInfo(NodeInfo* info){
  18         ourfree(info);
  19 }
  20
  21 OrderEncoder* allocOrderEncoder(){
  22         OrderEncoder* This = (OrderEncoder*) ourmalloc(sizeof(OrderEncoder));
  23         initDefVectorOrderGraph( &This->graphs );
  24         return This;
  25 }
  26
  27 void deleteOrderEncoder(OrderEncoder* This){
  28         uint size = getSizeVectorOrderGraph(&This->graphs);
  29         for(uint i=0; i<size; i++){
  30                 deleteOrderGraph(getVectorOrderGraph(&This->graphs, i));
  31         }
  32         ourfree(This);
  33 }
  34
  35 OrderEncoder* buildOrderGraphs(CSolver* This) {
  36         uint size = getSizeVectorOrder(This->allOrders);
  37         OrderEncoder* oEncoder = allocOrderEncoder();
  38         for(uint i=0; i<size; i++){
  39                 Order* order = getVectorOrder(This->allOrders, i);
  40                 OrderGraph *orderGraph=buildOrderGraph(order);
  41                 pushVectorOrderGraph(&oEncoder->graphs, orderGraph);
  42         }
  43         return oEncoder;
  44 }
  45
  46 OrderGraph* buildOrderGraph(Order *order) {
  47         OrderGraph* orderGraph = allocOrderGraph();
  48         uint constrSize = getSizeVectorBoolean(&order->constraints);
  49         for(uint j=0; j<constrSize; j++){
  50                 addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
  51         }
  52         return orderGraph;
  53 }
  54
  55 void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo){
  56         uint timer=0;
  57         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
  58         while(hasNextOrderNode(iterator)){
  59                 OrderNode* node = nextOrderNode(iterator);
  60                 NodeInfo* info= getNodeInfo(nodeToInfo, node);
  61                 if(info->status == NOTVISITED){
  62                         info->status = VISITED;
  63                         DFSNodeVisit(node, finishNodes, nodeToInfo, &timer, false);
  64                         info->status = FINISHED;
  65                         info->finishTime = timer;
  66                         pushVectorOrderNode(finishNodes, node);
  67                 }
  68         }
  69         deleteIterOrderNode(iterator);
  70 }
  71
  72 void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo){
  73         uint timer=0;
  74         uint size = getSizeVectorOrderNode(finishNodes);
  75         for(int i=size-1; i>=0; i--){
  76                 OrderNode* node = getVectorOrderNode(finishNodes, i);
  77                 NodeInfo* info= getNodeInfo(nodeToInfo, node);
  78                 if(info->status == NOTVISITED){
  79                         info->status = VISITED;
  80                         DFSNodeVisit(node, NULL, nodeToInfo, &timer, true);
  81                         info->status = FINISHED;
  82                         info->finishTime = timer;
  83                         pushVectorOrderNode(&graph->scc, node);
  84                 }
  85         }
  86 }
  87
  88 void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
  89         HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse){
  90         (*timer)++;
  91         model_print("Timer in DFSNodeVisit:%u\n", *timer);
  92         HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
  93         while(hasNextOrderEdge(iterator)){
  94                 OrderEdge* edge = nextOrderEdge(iterator);
  95                 OrderNode* child = isReverse? edge->source: edge->sink;
  96                 NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
  97                 if(childInfo->status == NOTVISITED){
  98                         childInfo->status = VISITED;
  99                         DFSNodeVisit(child, finishNodes, nodeToInfo, timer, isReverse);
 100                         childInfo->status = FINISHED;
 101                         childInfo->finishTime = *timer;
 102                         if(!isReverse)
 103                                 pushVectorOrderNode(finishNodes, child);
 104                 }
 105         }
 106         deleteIterOrderEdge(iterator);
 107 }
 108
 109 void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
 110         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
 111         while(hasNextOrderNode(iterator)){
 112                 putNodeInfo(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
 113         }
 114         deleteIterOrderNode(iterator);
 115 }
 116
 117 void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
 118         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
 119         while(hasNextOrderNode(iterator)){
 120                 NodeInfo* info= getNodeInfo(nodeToInfo, nextOrderNode(iterator));
 121                 info->status = NOTVISITED;
 122         }
 123         deleteIterOrderNode(iterator);
 124 }
 125
 126 void computeStronglyConnectedComponentGraph(OrderGraph* graph){
 127         VectorOrderNode finishNodes;
 128         initDefVectorOrderNode(& finishNodes);
 129         HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
 130         initializeNodeInfoSCC(graph, nodeToInfo);
 131         DFS(graph, &finishNodes, nodeToInfo);
 132         resetNodeInfoStatusSCC(graph, nodeToInfo);
 133         DFSReverse(graph, &finishNodes, nodeToInfo);
 134         deleteHashTableNodeInfo(nodeToInfo);
 135 }
 136
 137 void removeMustBeTrueNodes(OrderGraph* graph){
 138         //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
 139 }
 140
 141 void orderAnalysis(CSolver* solver){
 142         OrderEncoder* oEncoder = buildOrderGraphs(solver);
 143         uint size = getSizeVectorOrderGraph(&oEncoder->graphs);
 144         for(uint i=0; i<size; i++){
 145                 OrderGraph* graph = getVectorOrderGraph(&oEncoder->graphs, i);
 146                 removeMustBeTrueNodes(graph);
 147                 computeStronglyConnectedComponentGraph(graph);
 148         }
 149 }
 150