removing true nodes from the OrderGraph
[satune.git] / src / Encoders / orderencoder.h
index c48a0f7d3e6e50e841ab4ce596d986f7c0077a6e..f9b4d5f2edb0fe2fdefcf35ee8b92be437a0edc6 100644 (file)
 #include "structs.h"
 #include "mymemory.h"
 
-OrderGraph *buildOrderGraph(Order *order);
 void computeStronglyConnectedComponentGraph(OrderGraph *graph);
 void orderAnalysis(CSolver *solver);
 void initializeNodeInfoSCC(OrderGraph *graph);
-void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum);
+void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes);
 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes);
 void completePartialOrderGraph(OrderGraph *graph);
 void resetNodeInfoStatusSCC(OrderGraph *graph);
-void removeMustBeTrueNodes(OrderGraph *graph);
-void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node);
+bool isMustBeTrueNode(OrderNode* node);
+void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node);
+void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph);
 void completePartialOrderGraph(OrderGraph *graph);
 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes);
-void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges);
-void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes);
-void reachMustAnalysis(OrderGraph *graph);
-void localMustAnalysisTotal(OrderGraph *graph);
-void localMustAnalysisPartial(OrderGraph *graph);
+void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure);
+void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
+void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
+void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
 void orderAnalysis(CSolver *This);
-void decomposeOrder(Order *order, OrderGraph *graph);
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
 
 #endif/* ORDERGRAPHBUILDER_H */