1 #include "orderencoder.h"
5 #include "ordergraph.h"
10 NodeInfo* allocNodeInfo() {
11 NodeInfo* This = (NodeInfo*) ourmalloc(sizeof(NodeInfo));
13 This->status = NOTVISITED;
17 void deleteNodeInfo(NodeInfo* info) {
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));
30 void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
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);
44 deleteIterOrderNode(iterator);
47 void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
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);
63 void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
64 HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse) {
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;
78 pushVectorOrderNode(finishNodes, child);
81 deleteIterOrderEdge(iterator);
84 void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
85 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
86 while(hasNextOrderNode(iterator)){
87 putNodeInfo(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
89 deleteIterOrderNode(iterator);
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;
98 deleteIterOrderNode(iterator);
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 deleteVectorArrayOrderNode(&finishNodes);
113 void removeMustBeTrueNodes(OrderGraph* graph) {
114 //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
117 bool searchForNode(OrderNode *src, OrderNode *dst) {
119 VectorOrderNode stack;
120 initDefVectorOrderNode(&stack);
121 pushVectorOrderNode(&stack, src);
122 HashSetOrderNode* discovered = allocHashSetOrderNode(16, 0.3);
123 while(getSizeVectorOrderNode(&stack) != 0) {
124 OrderNode* node = lastVectorOrderNode(&stack); popVectorOrderNode(&stack);
125 HSIteratorOrderEdge *edgeit = iteratorOrderEdge(node->outEdges);
126 while(hasNextOrderEdge(edgeit)) {
127 OrderEdge* edge = nextOrderEdge(edgeit);
129 OrderNode *edge_dst = edge->sink;
132 if (addHashSetOrderNode(discovered, edge_dst)) {
133 pushVectorOrderNode(&stack, edge_dst);
137 deleteIterOrderEdge(edgeit);
140 deleteHashSetOrderNode(discovered);
141 deleteVectorArrayOrderNode(&stack);
145 void completePartialOrderGraph(OrderGraph* graph) {
146 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
147 while(hasNextOrderNode(iterator)) {
148 OrderNode* node = nextOrderNode(iterator);
149 HSIteratorOrderEdge *edgeit = iteratorOrderEdge(node->outEdges);
150 while(hasNextOrderEdge(edgeit)) {
151 OrderEdge* edge = nextOrderEdge(edgeit);
153 if (edge->polPos || searchForNode(node, edge->sink)) {
154 OrderEdge * newedge = getOrderEdgeFromOrderGraph(graph, edge->sink, edge->source);
155 newedge->pseudoPos = true;
159 deleteIterOrderEdge(edgeit);
161 deleteIterOrderNode(iterator);
164 void orderAnalysis(CSolver* This){
165 uint size = getSizeVectorOrder(This->allOrders);
166 for(uint i=0; i<size; i++){
167 Order* order = getVectorOrder(This->allOrders, i);
168 OrderGraph* graph = buildOrderGraph(order);
169 if (order->type==PARTIAL) {
170 completePartialOrderGraph(graph);
172 removeMustBeTrueNodes(graph);
173 computeStronglyConnectedComponentGraph(graph);
174 deleteOrderGraph(graph);