Function z3_sys::Z3_mk_enumeration_sort

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

Create a enumeration sort.

An enumeration sort with n elements. This function will also declare the functions corresponding to the enumerations.

• c: logical context
• name: 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.