Module Z3.Enumeration

module Enumeration: sig .. end

Functions to manipulate Enumeration expressions

val mk_sort : context -> Symbol.symbol -> Symbol.symbol list -> Sort.sort

Create a new enumeration sort.

val mk_sort_s : context -> string -> string list -> Sort.sort

Create a new enumeration sort.

val get_const_decls : Sort.sort -> FuncDecl.func_decl list

The function declarations of the constants in the enumeration.

val get_const_decl : Sort.sort -> int -> FuncDecl.func_decl

Retrieves the inx'th constant declaration in the enumeration.

val get_consts : Sort.sort -> Expr.expr list

The constants in the enumeration.

val get_const : Sort.sort -> int -> Expr.expr

Retrieves the inx'th constant in the enumeration.

val get_tester_decls : Sort.sort -> FuncDecl.func_decl list

The test predicates for the constants in the enumeration.

val get_tester_decl : Sort.sort -> int -> FuncDecl.func_decl

Retrieves the inx'th tester/recognizer declaration in the enumeration.