Module Libzipperposition.Ind_cst

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

raises NotAnInductiveConstant

if it fails

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 pp : t CCFormat.printer
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 Cst_set.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 Sequence.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)