package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Ctx : Ctx.S
module C = C
val on_pred_skolem_introduction : (C.t * Logtk.Term.t) Logtk.Signal.t

this signal is raised when a predicate Skolem is introduced

val is_renaming_clause : C.t -> bool

This clause has the shape of the renaming clause

val rename_form : ?should_rename:(Libzipperposition.FormulaRename.T.t -> bool) -> ?polarity_aware:bool -> c:C.t -> Libzipperposition.FormulaRename.T.t -> bool -> (Libzipperposition.FormulaRename.T.t * C.t list * C.t list) option

`rename_form ~should_rename ~c f polarity` tries to find a definition for formula f with the given polarity.

The result is of the form `Some (renamer term, new_defs, proof_parents)`

If the definition for a generalization of f is already found in the store, but with different polarity new_defs will contain definition for the missing polarity. If the definition of f is found for the right polarity, new_defs will be empty.

If f is not found an `should_rename f` holds, then definition of f is introduced for f with the given polarity.

In each case, proof_parents contains the clauses that introduce definition for f (either or both of polarities, that is).

For details and examples, consult our PAAR 2020 paper \urlhttp://matryoshka.gforge.inria.fr/pubs/ho_bools_paper.pdf

val get_skolem : parent:C.t -> mode:[< `Choice | `SkolemRecycle | `SkolemAlwaysFresh ] -> Libzipperposition.FormulaRename.T.t -> Libzipperposition.FormulaRename.T.t

`rename_form ~should_rename ~c f polarity` tries to find a definition for formula f with the given polarity.

The result is of the form `Some (renamer term, new_defs, proof_parents)`

If the definition for a generalization of f is already found in the store, but with different polarity new_defs will contain definition for the missing polarity. If the definition of f is found for the right polarity, new_defs will be empty.

If f is not found an `should_rename f` holds, then definition of f is introduced for f with the given polarity.

In each case, proof_parents contains the clauses that introduce definition for f (either or both of polarities, that is).

For details and examples, consult our PAAR 2020 paper \urlhttp://matryoshka.gforge.inria.fr/pubs/ho_bools_paper.pdf

`get_skolem ~parent ~mode f` computes a ``Skolem'' term for a formula f. This is either real Skolem term of Choice symbol applied to f, depending on the mode

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