package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

Library for Zipperposition

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

Maintainers

S

simon.cruanes.2.17@m4x.org

Sources

2.1.tar.gz

md5=e72de75e9f0f87da9e6e8c0a4d4c89f9

sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287

doc/libzipperposition.calculi/Libzipperposition_calculi/Bce/Make/argument-1-E/Stm/Ctx/index.html

Module `Stm.Ctx`

val sk_ctx : unit -> Logtk.Skolem.ctx

val ord : unit -> Logtk.Ordering.t

current ordering on terms

val selection_fun : unit -> Libzipperposition.Selection.t

selection function for clauses

val set_selection_fun : Libzipperposition.Selection.t -> unit

val set_ord : Logtk.Ordering.t -> unit

val signature : unit -> Logtk.Signature.t

Current signature

val renaming : Logtk.Subst.Renaming.t

Utils

val compare : Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t

Compare two terms

val select : Libzipperposition.Selection.t

val bool_select : Libzipperposition.Bool_selection.t

val lost_completeness : unit -> unit

To be called when completeness is not preserved

val is_completeness_preserved : unit -> bool

Check whether completeness was preserved so far

val add_signature : Logtk.Signature.t -> unit

Merge the given signature with the context's one

val find_signature : Logtk.ID.t -> Logtk.Type.t option

Find the type of the given symbol

val find_signature_exn : Logtk.ID.t -> Logtk.Type.t

Unsafe version of find_signature.

raises Not_found
for unknown symbols

val declare : Logtk.ID.t -> Logtk.Type.t -> unit

Declare the type of a symbol (updates signature)

val declare_syms : (Logtk.ID.t * Logtk.Type.t) list -> unit

Declare multiple symbols (more efficient that calling declare function incrementally)

val on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t

val on_signature_update : Logtk.Signature.t Logtk.Signal.t

val set_injective_for_arg : Logtk.ID.t -> int -> unit

val is_injective_for_arg : Logtk.ID.t -> int -> bool

Literals

module Lit : sig ... end

On This Page

Utils
Literals