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