mk_quantifier_const method

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

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

def_API('Z3_mk_quantifier_const', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(UINT), _in_array(3, APP), _in(UINT), _in_array(5, PATTERN), _in(AST)))

Implementation

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