sig
  module type PriorityNodeQueue =
    sig
      type t
      val create : unit -> Bwd.PriorityNodeQueue.t
      val pop : Bwd.PriorityNodeQueue.t -> Node.t
      val push : Node.t -> Bwd.PriorityNodeQueue.t -> unit
      val push_list : Node.t list -> Bwd.PriorityNodeQueue.t -> unit
      val clear : Bwd.PriorityNodeQueue.t -> unit
      val length : Bwd.PriorityNodeQueue.t -> int
      val is_empty : Bwd.PriorityNodeQueue.t -> bool
    end
  type result =
      Safe of Node.t list * Node.t list
    | Unsafe of Node.t * Node.t list
  module type Strategy =
    sig
      val search :
        ?invariants:Node.t list ->
        ?candidates:Node.t list -> Ast.t_system -> Bwd.result
    end
  module Make : functor (Q : PriorityNodeQueue) -> Strategy
  module BFS : Strategy
  module DFS : Strategy
  module BFSH : Strategy
  module DFSH : Strategy
  module BFSA : Strategy
  module DFSA : Strategy
  module Selected : Strategy
end