From: Hamed Date: Wed, 9 Aug 2017 11:59:02 +0000 (-0700) Subject: Computing SCC ... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=7ee793fb359c5903b3b9f1888fd3183f15520400 Computing SCC ... --- diff --git a/src/Collections/structs.c b/src/Collections/structs.c index 78a1447..2c149c5 100644 --- 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 451ac07..2a885e7 100644 --- 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 f9b099d..5e1edf6 100644 --- 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; igraphs, i); + removeMustBeTrueNodes(graph); computeStronglyConnectedComponentGraph(graph); } } diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h index 67e6103..58ea3d8 100644 --- 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 d438ad4..8de7eb0 100644 --- 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 67b3fc2..3427b7a 100644 --- a/src/Encoders/ordergraph.h +++ b/src/Encoders/ordergraph.h @@ -14,6 +14,7 @@ struct OrderGraph{ HashSetOrderNode* nodes; HashSetOrderEdge* edges; + VectorOrderNode scc; }; OrderGraph* allocOrderGraph();