package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
doc/libzipperposition.induction/Libzipperposition_induction/Make/argument-1-E/FormRename/index.html
Module E.FormRename
module Ctx : Libzipperposition.Ctx.Smodule C = Cval on_pred_skolem_introduction : (C.t * Logtk.Term.t) Logtk.Signal.tthis signal is raised when a predicate Skolem is introduced
val is_renaming_clause : C.t -> boolThis 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