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