package libzipperposition

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

Module Libzipperposition.Ind_cstSource

Inductive Constants and Cases

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

Sourcetype 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.

Sourceexception InvalidDecl of string
Sourceexception NotAnInductiveConstant of Logtk.ID.t
Sourceval id_as_cst : Logtk.ID.t -> t option
Sourceval id_as_cst_exn : Logtk.ID.t -> t

Unsafe version of as_cst

Sourceval id_is_cst : Logtk.ID.t -> bool

Check whether the given constant is an inductive constant

Sourceval on_new_cst : t Logtk.Signal.t

Triggered with new inductive constants

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

Make a new constant of the given type

Sourceval is_sub : t -> bool

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

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

Do these two inductive constants have the same type?

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

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

Sourcemodule Cst_set : CCSet.S with type elt = t

Set of constants

Inductive Skolems

Sourcetype ind_skolem = Logtk.ID.t * Logtk.Type.t
Sourceval ind_skolem_compare : ind_skolem -> ind_skolem -> int
Sourceval ind_skolem_equal : ind_skolem -> ind_skolem -> bool
Sourceval 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.

Sourceval 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.

Sourceval ind_skolem_depth : Logtk.ID.t -> int

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