Function Z3_mk_constructor 

pub unsafe extern "C" fn Z3_mk_constructor(
    c: Z3_context,
    name: Z3_symbol,
    recognizer: Z3_symbol,
    num_fields: c_uint,
    field_names: *const Z3_symbol,
    sorts: *const Z3_sort,
    sort_refs: *mut c_uint,
) -> Z3_constructor

Create a constructor.

• c: logical context.
• name: constructor name.
• recognizer: name of recognizer function.
• num_fields: number of fields in constructor.
• field_names: names of the constructor fields.
• sorts: field sorts, 0 if the field sort refers to a recursive sort.
• sort_refs: reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared.

See also:

• Z3_del_constructor
• Z3_mk_constructor_list
• Z3_query_constructor