mk_exists_const method

Z3_ast mk_exists_const(
  1. Z3_context c,
  2. int weight,
  3. int num_bound,
  4. Pointer<Z3_app> bound,
  5. int num_patterns,
  6. Pointer<Z3_pattern> patterns,
  7. Z3_ast body,
)

\brief Similar to #Z3_mk_forall_const.

\brief Create an existential quantifier using a list of constants that will form the set of bound variables.

\param c logical context. \param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. \param num_bound number of constants to be abstracted into bound variables. \param bound array of constants to be abstracted into bound variables. \param num_patterns number of patterns. \param patterns array containing the patterns created using #Z3_mk_pattern. \param body the body of the quantifier.

\sa Z3_mk_pattern \sa Z3_mk_forall_const

def_API('Z3_mk_exists_const', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in_array(2, APP), _in(UINT), _in_array(4, PATTERN), _in(AST)))

Implementation

Z3_ast mk_exists_const(
  Z3_context c,
  int weight,
  int num_bound,
  ffi.Pointer<Z3_app> bound,
  int num_patterns,
  ffi.Pointer<Z3_pattern> patterns,
  Z3_ast body,
) {
  return _mk_exists_const(
    c,
    weight,
    num_bound,
    bound,
    num_patterns,
    patterns,
    body,
  );
}