Module `Libzipperposition.Cover_set`

Cover Set

type cst = Ind_cst.t
type term = Logtk.Term.t
type case
type t

module Case : sig ... end

val pp : t CCFormat.printer
val ty : t -> Logtk.Type.t
val top : t -> cst: top constant of the coverset

val declarations : t -> (Logtk.ID.t * Logtk.Type.t) Iter.t: declarations set returns a list of type declarations that should be made if set is new (declare the top cst and its subcases)

val cases : ?⁠which:[ `Rec | `Base | `All ] -> t -> case Iter.t: Cases of the cover set

val sub_constants : t -> cst Iter.t: All sub-constants of a given inductive constant

val make : ?⁠cover_set_depth:int -> depth:int -> Logtk.Type.t -> t

Build a cover set for the given type.

a set of ground terms [t1,...,tn] with fresh constants inside (that are not declared as inductive!) such that bigor_{i in 1...n} t=ti is the skolemized version of the exhaustivity axiom on t's type.

parameter depth: the induction depth for the top constant in the coverset

parameter cover_set_depth: the depth of each case, that is, the number of constructor between the root of terms and leaf constants. default 1.