package libzipperposition

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

Module Avatar.MakeSource

Parameters

Signature

module E = E
module Solver = Sat

Split a clause into components

Sourceval check_empty : E.unary_inf_rule

Forbid empty clauses with trails, i.e. adds the negation of their trails to the SAT-solver

Sourceval before_check_sat : unit Logtk.Signal.t
Sourceval after_check_sat : unit Logtk.Signal.t
Sourceval 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

Sourceval check_satisfiability : E.generate_rule

Checks that the SAT context is still valid

Sourcetype 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).

Sourceval cut_pos : cut_res -> E.C.t list
Sourceval cut_lit : cut_res -> BLit.t
Sourceval cut_depth : cut_res -> int
Sourceval cut_proof : cut_res -> Logtk.Proof.Step.t
Sourceval cut_proof_parent : cut_res -> Logtk.Proof.Parent.t
Sourceval pp_cut_res : cut_res CCFormat.printer
Sourceval cut_res_clauses : cut_res -> E.C.t Iter.t
Sourceval print_lemmas : unit CCFormat.printer

print the current list of lemmas, and their status

Sourceval 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

Sourceval add_prove_lemma : (cut_res -> E.C.t list E.conversion_result) -> unit

Add a mean of proving lemmas

Sourceval 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.

Sourceval 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

Sourceval 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)

Sourceval 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

Sourceval convert_lemma : E.clause_conversion_rule

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

Sourceval register : split:bool -> 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