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 Signal.t
val after_check_sat : unit Signal.t
val filter_absurd_trails : (Trail.t -> bool) -> unit
val check_satisfiability : E.generate_rule
type cut_res = private {
cut_src : Literals.t list;
cut_pos : E.C.t list;
cut_neg : E.C.t list;
cut_lit : BLit.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 : Literals.t list -> ProofStep.t -> Avatar_intf.S.cut_res
val on_input_lemma : Avatar_intf.S.cut_res Signal.t
val convert_lemma : E.clause_conversion_rule
val register : unit -> unit
end