Computing SCC ...

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 78a1447e9551ccf4cdd6b2e2ee60ba6ef85a5fb9..2c149c5a71bdb16151bdeea805206f689aff85d0 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -82,7 +82,7 @@ static inline bool node_info_equals(OrderNode * key1, OrderNode * key2) {
 }
 
 HashTableImpl(OrderPair, OrderPair *, OrderPair *, order_pair_hash_Function, order_pair_equals, ourfree);
-HashTableImpl(Node, OrderNode *, NodeInfo *, node_info_hash_function, node_info_equals, ourfree);
+HashTableImpl(NodeInfo, OrderNode *, NodeInfo *, node_info_hash_function, node_info_equals, ourfree);
 
 HashSetImpl(TableEntry, TableEntry*, table_entry_hash_Function, table_entry_equals);
 HashSetImpl(OrderNode, OrderNode*, order_node_hash_Function, order_node_equals);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 451ac07c0579337d297688a758f8e479a34545fb..2a885e77083baa27dce319a318c3a0516396e8ba 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -25,7 +25,7 @@ VectorDef(OrderGraph, OrderGraph*);
 
 HashTableDef(Void, void *, void *);
 HashTableDef(OrderPair, OrderPair *, OrderPair *);
-HashTableDef(Node, OrderNode*, NodeInfo*);
+HashTableDef(NodeInfo, OrderNode*, NodeInfo*);
 
 HashSetDef(Void, void *);
 HashSetDef(TableEntry, TableEntry*);

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index f9b099d8695a5cfdac0ad692f0a5abb0f13dd930..5e1edf6e4d2234e5d265aad9bf6619c3a95ad19b 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -5,6 +5,7 @@
 #include "boolean.h"
 #include "ordergraph.h"
 #include "order.h"
+#include "ordernode.h"
 
 
 NodeInfo* allocNodeInfo(){
@@ -47,28 +48,73 @@ OrderEncoder* buildOrderGraphs(CSolver* This){
        return oEncoder;
 }
 
-void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNode* nodeToInfo, bool isReverse){
+void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo){
        uint timer=0;
        HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
        while(hasNextOrderNode(iterator)){
                OrderNode* node = nextOrderNode(iterator);
-               NodeInfo* info= getNode(nodeToInfo, node);
+               NodeInfo* info= getNodeInfo(nodeToInfo, node);
                if(info->status == NOTVISITED){
                        info->status = VISITED;
-                       //TODO ...
+                       DFSNodeVisit(node, finishNodes, nodeToInfo, &timer, false);
+                       info->status = FINISHED;
+                       info->finishTime = timer;
+                       pushVectorOrderNode(finishNodes, node);
                }
        }
        deleteIterOrderNode(iterator);
 }
 
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNode* nodeToInfo, uint* timer, bool isReverse){
-       NodeInfo* info= getNode(nodeToInfo, node);
+void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo){
+       uint timer=0;
+       uint size = getSizeVectorOrderNode(finishNodes);
+       for(int i=size-1; i>=0; i--){
+               OrderNode* node = getVectorOrderNode(finishNodes, i);
+               NodeInfo* info= getNodeInfo(nodeToInfo, node);
+               if(info->status == NOTVISITED){
+                       info->status = VISITED;
+                       DFSNodeVisit(node, NULL, nodeToInfo, &timer, true);
+                       info->status = FINISHED;
+                       info->finishTime = timer;
+                       pushVectorOrderNode(&graph->scc, node); 
+               }
+       }
+}
+
+void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
+       HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse){
+       (*timer)++;
+       model_print("Timer in DFSNodeVisit:%u\n", *timer);
+       HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
+       while(hasNextOrderEdge(iterator)){
+               OrderEdge* edge = nextOrderEdge(iterator);
+               OrderNode* child = isReverse? edge->source: edge->sink;
+               NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
+               if(childInfo->status == NOTVISITED){
+                       childInfo->status = VISITED;
+                       DFSNodeVisit(child, finishNodes, nodeToInfo, timer, isReverse);
+                       childInfo->status = FINISHED;
+                       childInfo->finishTime = *timer;
+                       if(!isReverse)
+                               pushVectorOrderNode(finishNodes, child); 
+               }
+       }
+       deleteIterOrderEdge(iterator);
 }
 
-void initializeNodeInfoSCC(OrderGraph* graph, HashTableNode* nodeToInfo){
+void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
        HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
        while(hasNextOrderNode(iterator)){
-               putNode(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
+               putNodeInfo(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
+       }
+       deleteIterOrderNode(iterator);
+}
+
+void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
+       HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
+       while(hasNextOrderNode(iterator)){
+               NodeInfo* info= getNodeInfo(nodeToInfo, nextOrderNode(iterator));
+               info->status = NOTVISITED;
        }
        deleteIterOrderNode(iterator);
 }
@@ -76,10 +122,16 @@ void initializeNodeInfoSCC(OrderGraph* graph, HashTableNode* nodeToInfo){
 void computeStronglyConnectedComponentGraph(OrderGraph* graph){
        VectorOrderNode finishNodes;
        initDefVectorOrderNode(& finishNodes);
-       HashTableNode* nodeToInfo = allocHashTableNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
        initializeNodeInfoSCC(graph, nodeToInfo);
-       // TODO
-       deleteHashTableNode(nodeToInfo);
+       DFS(graph, &finishNodes, nodeToInfo);
+       resetNodeInfoStatusSCC(graph, nodeToInfo);
+       DFSReverse(graph, &finishNodes, nodeToInfo);
+       deleteHashTableNodeInfo(nodeToInfo);
+}
+
+void removeMustBeTrueNodes(OrderGraph* graph){
+       //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
 }
 
 void orderAnalysis(CSolver* solver){
@@ -87,6 +139,7 @@ void orderAnalysis(CSolver* solver){
        uint size = getSizeVectorOrderGraph(&oEncoder->graphs);
        for(uint i=0; i<size; i++){
                OrderGraph* graph = getVectorOrderGraph(&oEncoder->graphs, i);
+               removeMustBeTrueNodes(graph);
                computeStronglyConnectedComponentGraph(graph);
        }
 }

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index 67e6103994c2f5c39cc73845c7d12b2e8a31fb04..58ea3d8f2703fc44b7243cab3b0d7cd7ae6234f4 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -31,9 +31,10 @@ void deleteOrderEncoder(OrderEncoder* This);
 OrderEncoder* buildOrderGraphs(CSolver* This);
 void computeStronglyConnectedComponentGraph(OrderGraph* graph);
 void orderAnalysis(CSolver* solver);
-void initializeNodeInfoSCC(OrderGraph* graph, HashTableNode* nodeToInfo);
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNode* nodeToInfo, uint* timer, bool isReverse);
-void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNode* nodeToInfo, bool isReverse);
+void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo);
+void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse);
+void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo);
+void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo);
 
 #endif /* ORDERGRAPHBUILDER_H */
 

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index d438ad422e4572617b5c893c54326876ab4b9b09..8de7eb0d2a9ea69bb8b0e6dd29c41370cde72e54 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -6,6 +6,7 @@
 OrderGraph* allocOrderGraph(){
        OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
        This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       initDefVectorOrderNode(&This->scc);
        return This;
 }
 

diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 67b3fc2f87abac05d7f0dec65b1853a1d6184a53..3427b7a97999ab9719574502902a3931e90f073d 100644 (file)
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -14,6 +14,7 @@
 struct OrderGraph{
        HashSetOrderNode* nodes;
        HashSetOrderEdge* edges;
+       VectorOrderNode scc;
 };
 
 OrderGraph* allocOrderGraph();