package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

Parameters

Signature

module E = E
module Solver = Sat
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 : (Libzipperposition.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 {
  1. cut_form : Libzipperposition.Cut_form.t;
    (*

    the lemma itself

    *)
  2. cut_pos : E.C.t list;
    (*

    clauses true if lemma is true

    *)
  3. cut_lit : BLit.t;
    (*

    lit that is true if lemma is true

    *)
  4. cut_depth : int;
    (*

    if the lemma is used to prove another lemma

    *)
  5. cut_proof : Logtk.Proof.Step.t;
    (*

    where does the lemma come from?

    *)
  6. cut_proof_parent : Logtk.Proof.Parent.t;
    (*

    how to justify sth from the lemma

    *)
  7. 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_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 Iter.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 -> Libzipperposition.Cut_form.t -> Logtk.Proof.Step.t -> cut_res

Introduce a cut on the given clause(s). Pure.

  • parameter 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 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 on_input_lemma

val convert_lemma : E.clause_conversion_rule

Intercepts input lemmas and converts them into clauses. Triggers on_input_lemma with the resulting cut

val register : split_kind:[< `Eager | `Lazy | `Off Off ] -> unit -> unit

Register inference rules to the environment

  • parameter split

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct