sig
  type env
  val make_env : Cfg.cfg -> Env.env
  val get_cfg : Env.env -> Cfg.cfg
  val get_symbol_table : Env.env -> Term.symbol_table
  val get_predicate_table : Env.env -> Predicate.predicate_table
  val get_negative_units : Env.env -> NegativeUnits.store
  val get_rules : Env.env -> Term.term list
  val get_current_result : Env.env -> Tableau.result
  val set_current_result : Env.env -> Tableau.result -> unit
  val ensure_ready_to_assert : Env.env -> Term.symbol -> Predicate.predicate
  val ensure_ready_to_run : Env.env -> Term.symbol -> Predicate.predicate
  type statement_type = Meta | Unit | Rule | Disjunction | False
  val classify_statement_functor :
    Env.env -> Term.symbol -> Env.statement_type
  val lookup_predicate : Env.env -> string -> int -> Predicate.predicate
  val find_predicate : Env.env -> string -> int -> Predicate.predicate
  val add_rule : Env.env -> Term.term -> unit
  val add_disjunction : Env.env -> Term.term -> unit
  val add_false : Env.env -> unit
  val abolish_predicate : Env.env -> string -> int -> unit
  val clear_rules : Env.env -> unit
  val begin_shared_input : Env.env -> unit
  val end_shared_input : Env.env -> unit
  val unit_for_env : Env.env -> Term.term -> Term.term
end