sig
  module E : Env.S
  module Solver : Sat_solver.S
  module BLit = BBox.Lit
  val split : E.multi_simpl_rule
  val check_empty : E.unary_inf_rule
  val before_check_sat : unit Logtk.Signal.t
  val after_check_sat : unit Logtk.Signal.t
  val filter_absurd_trails : (Trail.t -> bool) -> unit
  val check_satisfiability : E.generate_rule
  type cut_res = private {
    cut_form : Cut_form.t;
    cut_pos : E.C.t list;
    cut_lit : BLit.t;
    cut_depth : int;
    cut_proof : Logtk.Proof.Step.t;
    cut_proof_parent : Logtk.Proof.Parent.t;
    cut_reason : unit CCFormat.printer option;
  }
  val cut_form : Avatar_intf.S.cut_res -> Cut_form.t
  val cut_pos : Avatar_intf.S.cut_res -> E.C.t list
  val cut_lit : Avatar_intf.S.cut_res -> BLit.t
  val cut_depth : Avatar_intf.S.cut_res -> int
  val cut_proof : Avatar_intf.S.cut_res -> Logtk.Proof.Step.t
  val cut_proof_parent : Avatar_intf.S.cut_res -> Logtk.Proof.Parent.t
  val pp_cut_res : Avatar_intf.S.cut_res CCFormat.printer
  val cut_res_clauses : Avatar_intf.S.cut_res -> E.C.t Sequence.t
  val print_lemmas : unit CCFormat.printer
  val introduce_cut :
    ?reason:unit CCFormat.printer ->
    ?penalty:int ->
    ?depth:int -> Cut_form.t -> Logtk.Proof.Step.t -> Avatar_intf.S.cut_res
  val add_prove_lemma :
    (Avatar_intf.S.cut_res -> E.C.t list E.conversion_result) -> unit
  val add_lemma : Avatar_intf.S.cut_res -> unit
  val add_imply :
    Avatar_intf.S.cut_res list ->
    Avatar_intf.S.cut_res -> Logtk.Proof.Step.t -> unit
  val on_input_lemma : Avatar_intf.S.cut_res Logtk.Signal.t
  val on_lemma : Avatar_intf.S.cut_res Logtk.Signal.t
  val convert_lemma : E.clause_conversion_rule
  val register : split:bool -> unit -> unit
end