package libzipperposition

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

Inductive Constants and Cases

Skolem constants of an inductive type, coversets, etc. required for inductive reasoning.

type t

A ground term of an inductive type. It must correspond to a term built with the corresponding t only. For instance, a constant of type nat should be equal to s^n(0) in any model.

exception InvalidDecl of string
exception NotAnInductiveConstant of Logtk.ID.t
val id_as_cst : Logtk.ID.t -> t option
val id_as_cst_exn : Logtk.ID.t -> t

Unsafe version of as_cst

val id_is_cst : Logtk.ID.t -> bool

Check whether the given constant is an inductive constant

val on_new_cst : t Logtk.Signal.t

Triggered with new inductive constants

val make_skolem : Logtk.Type.t -> Logtk.ID.t
val make : ?depth:int -> is_sub:bool -> Logtk.Type.t -> t

Make a new constant of the given type

val is_sub : t -> bool

Is the constant a sub-constant (i.e. a subterm of a case in a coverset)?

val id_is_sub : Logtk.ID.t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val id : t -> Logtk.ID.t
val to_term : t -> Logtk.Term.t
val ty : t -> Logtk.Type.t
val same_type : t -> t -> bool

Do these two inductive constants have the same type?

val depth : t -> int
val dominates : t -> t -> bool

dominates c1 c2 if depth c1 < depth c2. This way, in coversets, the top constant dominates all sub-constants

module Cst_set : CCSet.S with type elt = t

Set of constants

Inductive Skolems

type ind_skolem = Logtk.ID.t * Logtk.Type.t
val ind_skolem_compare : ind_skolem -> ind_skolem -> int
val ind_skolem_equal : ind_skolem -> ind_skolem -> bool
val id_is_ind_skolem : Logtk.ID.t -> Logtk.Type.t -> bool

id_is_potential_cst id ty returns true if id:ty is a skolem constant of an inductive type, or if it is already an inductive constant.

val find_ind_skolems : Logtk.Term.t -> ind_skolem Iter.t

find_ind_skolem term searches subterms of term for constants that are of an inductive type and that are skolems or (already) inductive constants.

val ind_skolem_depth : Logtk.ID.t -> int

depth of the skolem (0 if not an inductive constant)

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