Function z3_sys::Z3_query_constructor

pub unsafe extern "C" fn Z3_query_constructor(
    c: Z3_context,
    constr: Z3_constructor,
    num_fields: c_uint,
    constructor: *mut Z3_func_decl,
    tester: *mut Z3_func_decl,
    accessors: *mut Z3_func_decl
)

Query constructor for declared functions.

• c: logical context.
• constr: constructor container. The container must have been passed in to a Z3_mk_datatype call.
• num_fields: number of accessor fields in the constructor.
• constructor: constructor function declaration, allocated by user.
• tester: constructor test function declaration, allocated by user.
• accessors: array of accessor function declarations allocated by user. The array must contain num_fields elements.

See also:

• Z3_mk_constructor