void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure);
void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);