sig
  val search : Variable.t list -> Ast.t_system -> unit
  val resume_search_from : Variable.t list -> Ast.t_system -> unit
  val replay_trace_and_expand :
    Variable.t list -> Ast.t_system -> Node.t -> unit
  val smallest_to_resist_on_trace : Node.t list -> Node.t list
  type env
  type state = private int array
  val print_state :
    Enumerative.env -> Format.formatter -> Enumerative.state -> unit
  val empty_env : Enumerative.env
  val mk_env : int -> Ast.t_system -> Enumerative.env
  val int_of_term : Enumerative.env -> Types.term -> int
  val next_id : Enumerative.env -> int
  val new_undef_state : Enumerative.env -> Enumerative.state
  val empty_state : Enumerative.state
  val register_state : Enumerative.env -> Enumerative.state -> unit
  val size_of_env : Enumerative.env -> int
  val no_scan_states : Enumerative.env -> unit
  val print_last : Enumerative.env -> unit
  val init : Ast.t_system -> unit
  val first_good_candidate : Node.t list -> Node.t option
end