[−][src]Function z3_sys::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: