query_constructor method

void query_constructor(
  1. Z3_context c,
  2. Z3_constructor constr,
  3. int num_fields,
  4. Pointer<Z3_func_decl> constructor,
  5. Pointer<Z3_func_decl> tester,
  6. Pointer<Z3_func_decl> accessors,
)

\brief Query constructor for declared functions.

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

\sa Z3_mk_constructor

def_API('Z3_query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL)))

Implementation

void query_constructor(
  Z3_context c,
  Z3_constructor constr,
  int num_fields,
  ffi.Pointer<Z3_func_decl> constructor,
  ffi.Pointer<Z3_func_decl> tester,
  ffi.Pointer<Z3_func_decl> accessors,
) {
  return _query_constructor(
    c,
    constr,
    num_fields,
    constructor,
    tester,
    accessors,
  );
}