Functor Avatar.Make

module Make: functor (E : Env.S) -> functor (Sat : Sat_solver.S) -> S 
    with module E = E
     and module Solver = Sat

Parameters:

`E`	:	`Env.S`
`Sat`	:	`Sat_solver.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

split : if true, the clause splitting rule is added. Otherwise Avatar is only used for other things such as induction.