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 : Proof.Step.t;
cut_proof_parent : 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 -> Proof.Step.t
val cut_proof_parent : Avatar_intf.S.cut_res -> 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 -> 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 -> 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