Up  

Module type Avatar.S

module type S = Avatar_intf.S
module E: Env.S 
module Solver: Sat_solver.S 
module BLit: BBox.Lit
val split : E.multi_simpl_rule
Split a clause into components
val check_empty : E.unary_inf_rule
Forbid empty clauses with trails, i.e. adds the negation of their trails to the SAT-solver
val before_check_sat : unit Logtk.Signal.t
val after_check_sat : unit Logtk.Signal.t
val filter_absurd_trails : (Trail.t -> bool) -> unit
filter_trails f calls f on every trail associated with the empty clause. If f returns false, the trail is ignored, otherwise it's negated and sent to the SAT solver
val check_satisfiability : E.generate_rule
Checks that the SAT context is still valid
type cut_res = private {
   cut_form : Cut_form.t; (*
the lemma itself
*)
   cut_pos : E.C.t list; (*
clauses true if lemma is true
*)
   cut_lit : BLit.t; (*
lit that is true if lemma is true
*)
   cut_depth : int; (*
if the lemma is used to prove another lemma
*)
   cut_proof : Logtk.Proof.Step.t; (*
where does the lemma come from?
*)
   cut_proof_parent : Logtk.Proof.Parent.t; (*
how to justify sth from the lemma
*)
   cut_reason : unit CCFormat.printer option; (*
Informal reason why the lemma was added
*)
}
This represents a cut on a formula, where we obtain a list of clauses cut_pos representing the formula itself with the trail lemma, and a boolean literal cut_lit that is true iff the trail is true.

Other modules, when a cut is introduced, will try to disprove the lemma (e.g. by induction or theory reasoning).

val cut_form : cut_res -> Cut_form.t
val cut_pos : cut_res -> E.C.t list
val cut_lit : cut_res -> BLit.t
val cut_depth : cut_res -> int
val cut_proof : cut_res -> Logtk.Proof.Step.t
val cut_proof_parent : cut_res -> Logtk.Proof.Parent.t
val pp_cut_res : cut_res CCFormat.printer
val cut_res_clauses : cut_res -> E.C.t Sequence.t
val print_lemmas : unit CCFormat.printer
print the current list of lemmas, and their status
val introduce_cut : ?reason:unit CCFormat.printer ->
       ?penalty:int ->
       ?depth:int -> Cut_form.t -> Logtk.Proof.Step.t -> cut_res
Introduce a cut on the given clause(s). Pure.
reason : some comment on why the lemma was added
val add_prove_lemma : (cut_res -> E.C.t list E.conversion_result) -> unit
Add a mean of proving lemmas
val add_lemma : cut_res -> unit
Add the given cut to the list of lemmas. Modifies the global list of lemmas. It will call the functions added by Avatar_intf.S.add_prove_lemma to try and prove this one.
val add_imply : cut_res list ->
       cut_res -> Logtk.Proof.Step.t -> unit
add_imply l res means that the conjunction of lemmas in l implies that the lemma res is proven
val on_input_lemma : cut_res Logtk.Signal.t
Triggered every time a cut is introduced for an input lemma (i.e. every time a statement of the form `lemma F` is translated)
val on_lemma : cut_res Logtk.Signal.t
Triggered every time a cut is introduced, by any means. In particular it is triggered at least as often as Avatar_intf.S.on_input_lemma
val convert_lemma : E.clause_conversion_rule
Intercepts input lemmas and converts them into clauses. Triggers Avatar_intf.S.on_input_lemma with the resulting cut
val register : split:bool -> unit -> unit
Register inference rules to the environment
split : if true, the clause splitting rule is added. Otherwise Avatar is only used for other things such as induction.