Function z3_sys::Z3_mk_constructor [−][src]
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
Expand description
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.