Function z3_sys::Z3_mk_enumeration_sort [−][src]
pub unsafe extern "C" fn Z3_mk_enumeration_sort(
c: Z3_context,
name: Z3_symbol,
n: c_uint,
enum_names: *const Z3_symbol,
enum_consts: *mut Z3_func_decl,
enum_testers: *mut Z3_func_decl
) -> Z3_sort
Expand description
Create a enumeration sort.
An enumeration sort with n
elements.
This function will also declare the functions corresponding to the enumerations.
c
: logical contextname
: name of the enumeration sort.n
: number of elements in enumeration sort.enum_names
: names of the enumerated elements.enum_consts
: constants corresponding to the enumerated elements.enum_testers
: predicates testing if terms of the enumeration sort correspond to an enumeration.
For example, if this function is called with three symbols A, B, C and the name S, then
s
is a sort whose name is S, and the function returns three terms corresponding to A, B, C in
enum_consts
. The array enum_testers
has three predicates of type (s -> Bool)
.
The first predicate (corresponding to A) is true when applied to A, and false otherwise.
Similarly for the other predicates.