1 #include "orderencoder.h"
5 #include "ordergraph.h"
10 NodeInfo* allocNodeInfo() {
11 NodeInfo* This = (NodeInfo*) ourmalloc(sizeof(NodeInfo));
12 This->status = NOTVISITED;
16 void deleteNodeInfo(NodeInfo* info) {
20 OrderGraph* buildOrderGraph(Order *order) {
21 OrderGraph* orderGraph = allocOrderGraph(order);
22 uint constrSize = getSizeVectorBoolean(&order->constraints);
23 for(uint j=0; j<constrSize; j++){
24 addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
29 void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
30 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
31 while(hasNextOrderNode(iterator)){
32 OrderNode* node = nextOrderNode(iterator);
33 NodeInfo* info= getNodeInfo(nodeToInfo, node);
34 if(info->status == NOTVISITED){
35 info->status = VISITED;
36 DFSNodeVisit(node, finishNodes, nodeToInfo, false);
37 info->status = FINISHED;
38 pushVectorOrderNode(finishNodes, node);
41 deleteIterOrderNode(iterator);
44 void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
45 uint size = getSizeVectorOrderNode(finishNodes);
46 for(int i=size-1; i>=0; i--){
47 OrderNode* node = getVectorOrderNode(finishNodes, i);
48 NodeInfo* info= getNodeInfo(nodeToInfo, node);
49 if(info->status == NOTVISITED){
50 info->status = VISITED;
51 DFSNodeVisit(node, NULL, nodeToInfo, true);
52 info->status = FINISHED;
53 pushVectorOrderNode(&graph->scc, node);
58 void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo, bool isReverse) {
59 HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
60 while(hasNextOrderEdge(iterator)){
61 OrderEdge* edge = nextOrderEdge(iterator);
62 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
65 OrderNode* child = isReverse? edge->source: edge->sink;
67 NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
68 if(childInfo->status == NOTVISITED){
69 childInfo->status = VISITED;
70 DFSNodeVisit(child, finishNodes, nodeToInfo, isReverse);
71 childInfo->status = FINISHED;
73 pushVectorOrderNode(finishNodes, child);
76 deleteIterOrderEdge(iterator);
79 void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
80 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
81 while(hasNextOrderNode(iterator)){
82 putNodeInfo(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
84 deleteIterOrderNode(iterator);
87 void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
88 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
89 while(hasNextOrderNode(iterator)){
90 NodeInfo* info= getNodeInfo(nodeToInfo, nextOrderNode(iterator));
91 info->status = NOTVISITED;
93 deleteIterOrderNode(iterator);
96 void computeStronglyConnectedComponentGraph(OrderGraph* graph) {
97 VectorOrderNode finishNodes;
98 initDefVectorOrderNode(& finishNodes);
99 HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
100 initializeNodeInfoSCC(graph, nodeToInfo);
101 DFS(graph, &finishNodes, nodeToInfo);
102 resetNodeInfoStatusSCC(graph, nodeToInfo);
103 DFSReverse(graph, &finishNodes, nodeToInfo);
104 deleteHashTableNodeInfo(nodeToInfo);
105 deleteVectorArrayOrderNode(&finishNodes);
108 void removeMustBeTrueNodes(OrderGraph* graph) {
109 //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
112 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode* node, HashTableNodeInfo* nodeToInfo) {
113 HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges);
114 while(hasNextOrderEdge(iterator)){
115 OrderEdge* inEdge = nextOrderEdge(iterator);
116 if (inEdge->polNeg) {
117 OrderNode* src = inEdge->source;
118 NodeInfo* srcInfo = getNodeInfo(nodeToInfo, src);
119 if (srcInfo->status==VISITED) {
120 //Make a pseudoEdge to point backwards
121 OrderEdge * newedge = getOrderEdgeFromOrderGraph(graph, inEdge->sink, inEdge->source);
122 newedge->pseudoPos = true;
126 deleteIterOrderEdge(iterator);
127 iterator = iteratorOrderEdge(node->outEdges);
128 while(hasNextOrderEdge(iterator)){
129 OrderEdge* edge = nextOrderEdge(iterator);
130 if (!edge->polPos) //Ignore edges that do not have positive polarity
133 OrderNode* child = edge->sink;
134 NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
135 if(childInfo->status == NOTVISITED){
136 childInfo->status = VISITED;
137 DFSPseudoNodeVisit(graph, child, nodeToInfo);
138 childInfo->status = FINISHED;
141 deleteIterOrderEdge(iterator);
144 void completePartialOrderGraph(OrderGraph* graph) {
145 VectorOrderNode finishNodes;
146 initDefVectorOrderNode(& finishNodes);
147 HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
148 initializeNodeInfoSCC(graph, nodeToInfo);
149 DFS(graph, &finishNodes, nodeToInfo);
150 resetNodeInfoStatusSCC(graph, nodeToInfo);
152 uint size = getSizeVectorOrderNode(&finishNodes);
153 for(int i=size-1; i>=0; i--){
154 OrderNode* node = getVectorOrderNode(&finishNodes, i);
155 NodeInfo* info= getNodeInfo(nodeToInfo, node);
156 if(info->status == NOTVISITED){
157 info->status = VISITED;
158 DFSPseudoNodeVisit(graph, node, nodeToInfo);
159 info->status = FINISHED;
163 deleteHashTableNodeInfo(nodeToInfo);
164 deleteVectorArrayOrderNode(&finishNodes);
167 void DFSMust(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
168 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
169 while(hasNextOrderNode(iterator)){
170 OrderNode* node = nextOrderNode(iterator);
171 NodeInfo* info= getNodeInfo(nodeToInfo, node);
172 if(info->status == NOTVISITED){
173 info->status = VISITED;
174 DFSMustNodeVisit(node, finishNodes, nodeToInfo, false);
175 info->status = FINISHED;
176 pushVectorOrderNode(finishNodes, node);
179 deleteIterOrderNode(iterator);
182 void DFSMustNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
183 HashTableNodeInfo* nodeToInfo, bool clearBackEdges) {
184 HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->outEdges);
185 while(hasNextOrderEdge(iterator)){
186 OrderEdge* edge = nextOrderEdge(iterator);
187 OrderNode* child = edge->sink;
188 NodeInfo* childInfo = getNodeInfo(nodeToInfo, child);
190 if (clearBackEdges && childInfo->status==VISITED) {
191 //We have a backedge, so note that this edge must be negative
192 edge->mustNeg = true;
195 if (!edge->mustPos) //Ignore edges that are not must Positive edges
198 if(childInfo->status == NOTVISITED){
199 childInfo->status = VISITED;
200 DFSMustNodeVisit(child, finishNodes, nodeToInfo, clearBackEdges);
201 childInfo->status = FINISHED;
202 pushVectorOrderNode(finishNodes, child);
205 deleteIterOrderEdge(iterator);
208 void DFSClearContradictions(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
209 uint size=getSizeVectorOrderNode(finishNodes);
210 for(int i=size-1; i>=0; i--){
211 OrderNode* node=getVectorOrderNode(finishNodes, i);
212 NodeInfo* info=getNodeInfo(nodeToInfo, node);
213 if(info->status == NOTVISITED){
214 info->status = VISITED;
215 DFSMustNodeVisit(node, NULL, nodeToInfo, true);
216 info->status = FINISHED;
221 /* This function finds edges that would form a cycle with must edges
222 and forces them to be mustNeg. */
224 void reachMustAnalysis(OrderGraph *graph) {
225 HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
226 VectorOrderNode finishNodes;
227 initDefVectorOrderNode(& finishNodes);
228 //Topologically sort the mustPos edge graph
229 DFSMust(graph, &finishNodes, nodeToInfo);
230 resetNodeInfoStatusSCC(graph, nodeToInfo);
232 //Find any backwards edges that complete cycles and force them to be mustNeg
233 DFSClearContradictions(graph, &finishNodes, nodeToInfo);
234 deleteVectorArrayOrderNode(&finishNodes);
235 deleteHashTableNodeInfo(nodeToInfo);
238 /* This function finds edges that must be positive and forces the
239 inverse edge to be negative (and clears its positive polarity if it
242 void localMustAnalysisTotal(OrderGraph *graph) {
243 HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
244 while(hasNextOrderEdge(iterator)) {
245 OrderEdge *edge = nextOrderEdge(iterator);
246 if (edge -> mustPos) {
247 OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
248 if (invEdge!= NULL && !invEdge -> mustPos && invEdge->polPos) {
249 invEdge->polPos = false;
251 invEdge->mustNeg = true;
254 deleteIterOrderEdge(iterator);
257 /** This finds edges that must be positive and forces the inverse edge
258 to be negative. It also clears the negative flag of this edge.
259 It also finds edges that must be negative and clears the positive
262 void localMustAnalysisPartial(OrderGraph *graph) {
263 HSIteratorOrderEdge* iterator = iteratorOrderEdge(graph->edges);
264 while(hasNextOrderEdge(iterator)) {
265 OrderEdge *edge = nextOrderEdge(iterator);
266 if (edge -> mustPos) {
267 if (edge->polNeg && !edge->mustNeg) {
268 edge->polNeg = false;
270 OrderEdge *invEdge=getInverseOrderEdge(graph, edge);
271 if (invEdge != NULL && !invEdge -> mustPos) {
272 invEdge->polPos = false;
274 invEdge->mustNeg = true;
276 if (edge->mustNeg && !edge->mustPos) {
277 edge->polPos = false;
280 deleteIterOrderEdge(iterator);
283 void orderAnalysis(CSolver* This) {
284 uint size = getSizeVectorOrder(This->allOrders);
285 for(uint i=0; i<size; i++){
286 Order* order = getVectorOrder(This->allOrders, i);
287 OrderGraph* graph = buildOrderGraph(order);
288 if (order->type==PARTIAL) {
289 //Required to do SCC analysis for partial order graphs. It
290 //makes sure we don't incorrectly optimize graphs with negative
292 completePartialOrderGraph(graph);
295 //This analysis is completely optional
296 reachMustAnalysis(graph);
298 //This pair of analysis is also optional
299 if (order->type==PARTIAL) {
300 localMustAnalysisPartial(graph);
302 localMustAnalysisTotal(graph);
305 //This analysis is completely optional
306 removeMustBeTrueNodes(graph);
309 computeStronglyConnectedComponentGraph(graph);
310 deleteOrderGraph(graph);