mk_constructor method

Z3_constructor mk_constructor(
  1. Z3_context c,
  2. Z3_symbol name,
  3. Z3_symbol recognizer,
  4. int num_fields,
  5. Pointer<Z3_symbol> field_names,
  6. Pointer<Z3_sort> sorts,
  7. Pointer<UnsignedInt> sort_refs,
)

\brief Create a constructor.

\param c logical context. \param name constructor name. \param recognizer name of recognizer function. \param num_fields number of fields in constructor. \param field_names names of the constructor fields. \param sorts field sorts, 0 if the field sort refers to a recursive sort. \param 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.

\sa Z3_del_constructor \sa Z3_mk_constructor_list \sa Z3_query_constructor

def_API('Z3_mk_constructor', CONSTRUCTOR, (_in(CONTEXT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(3, SYMBOL), _in_array(3, SORT), _in_array(3, UINT)))

Implementation

Z3_constructor mk_constructor(
  Z3_context c,
  Z3_symbol name,
  Z3_symbol recognizer,
  int num_fields,
  ffi.Pointer<Z3_symbol> field_names,
  ffi.Pointer<Z3_sort> sorts,
  ffi.Pointer<ffi.UnsignedInt> sort_refs,
) {
  return _mk_constructor(
    c,
    name,
    recognizer,
    num_fields,
    field_names,
    sorts,
    sort_refs,
  );
}