sig
  module HSA :
    sig
      type key = Types.SAtom.t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_opt : 'a t -> key -> 'a option
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  module MA :
    sig
      type key = Types.Atom.t
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val min_binding_opt : 'a t -> (key * 'a) option
      val max_binding : 'a t -> key * 'a
      val max_binding_opt : 'a t -> (key * 'a) option
      val choose : 'a t -> key * 'a
      val choose_opt : 'a t -> (key * 'a) option
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val find_opt : key -> 'a t -> 'a option
      val find_first : (key -> bool) -> 'a t -> key * 'a
      val find_first_opt : (key -> bool) -> 'a t -> (key * 'a) option
      val find_last : (key -> bool) -> 'a t -> key * 'a
      val find_last_opt : (key -> bool) -> 'a t -> (key * 'a) option
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
    end
  type inst_trans = {
    i_reqs : Types.SAtom.t;
    i_udnfs : Types.SAtom.t list list;
    i_actions : Types.SAtom.t;
    i_touched_terms : Types.Term.Set.t;
  }
  type possible_result =
      Reach of
        (Types.SAtom.t * Ast.transition_info * Variable.subst * Types.SAtom.t)
        list
    | Spurious of Ast.trace
    | Unreach
  val all_var_terms : Variable.t list -> Ast.t_system -> Types.Term.Set.t
  val search : Hstring.t list -> Ast.t_system -> unit Forward.HSA.t
  val search_stateless :
    Hstring.t list ->
    Ast.t_system -> (Types.SAtom.t * Types.Term.Set.t) Forward.MA.t
  val instantiate_transitions :
    Variable.t list ->
    Variable.t list -> Ast.transition list -> Forward.inst_trans list
  val abstract_others : Types.SAtom.t -> Hstring.t list -> Types.SAtom.t
  val reachable_on_trace_from_init :
    Ast.t_system -> Node.t -> Ast.trace -> Forward.possible_result
  val spurious : Node.t -> bool
  val spurious_error_trace : Ast.t_system -> Node.t -> bool
  val spurious_due_to_cfm : Ast.t_system -> Node.t -> bool
  val replay_history :
    Ast.t_system ->
    Node.t ->
    (Types.SAtom.t * Ast.transition_info * Variable.subst * Types.SAtom.t)
    list option
  val conflicting_from_trace :
    Ast.t_system -> Ast.trace -> Types.SAtom.t list
  val uguard_dnf :
    Variable.subst ->
    Variable.t list ->
    Variable.t list ->
    (Variable.t * Types.SAtom.t list) list -> Types.SAtom.t list list
end