package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d
doc/libzipperposition.calculi/Libzipperposition_calculi/Avatar/Make/index.html
Module Avatar.MakeSource
Parameters
module E : Libzipperposition.Env.Smodule Sat : Libzipperposition.Sat_solver.SSignature
module E = Emodule Solver = SatSplit a clause into components
Forbid empty clauses with trails, i.e. adds the negation of their trails to the SAT-solver
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
Checks that the SAT context is still valid
type cut_res = private {cut_form : Libzipperposition.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).
print the current list of lemmas, and their status
val introduce_cut :
?reason:unit CCFormat.printer ->
?penalty:int ->
?depth:int ->
Libzipperposition.Cut_form.t ->
Logtk.Proof.Step.t ->
cut_resIntroduce a cut on the given clause(s). Pure.
Add a mean of proving lemmas
Add the given cut to the list of lemmas. Modifies the global list of lemmas. It will call the functions added by add_prove_lemma to try and prove this one.
add_imply l res means that the conjunction of lemmas in l implies that the lemma res is proven
Triggered every time a cut is introduced for an input lemma (i.e. every time a statement of the form `lemma F` is translated)
Triggered every time a cut is introduced, by any means. In particular it is triggered at least as often as on_input_lemma
Intercepts input lemmas and converts them into clauses. Triggers on_input_lemma with the resulting cut
Register inference rules to the environment