mk_quantifier_const_ex method

Z3_ast mk_quantifier_const_ex(
  1. Z3_context c,
  2. bool is_forall,
  3. int weight,
  4. Z3_symbol quantifier_id,
  5. Z3_symbol skolem_id,
  6. int num_bound,
  7. Pointer<Z3_app> bound,
  8. int num_patterns,
  9. Pointer<Z3_pattern> patterns,
  10. int num_no_patterns,
  11. Pointer<Z3_ast> no_patterns,
  12. 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_ex', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(5, APP), _in(UINT), _in_array(7, PATTERN), _in(UINT), _in_array(9, AST), _in(AST)))

Implementation

Z3_ast mk_quantifier_const_ex(
  Z3_context c,
  bool is_forall,
  int weight,
  Z3_symbol quantifier_id,
  Z3_symbol skolem_id,
  int num_bound,
  ffi.Pointer<Z3_app> bound,
  int num_patterns,
  ffi.Pointer<Z3_pattern> patterns,
  int num_no_patterns,
  ffi.Pointer<Z3_ast> no_patterns,
  Z3_ast body,
) {
  return _mk_quantifier_const_ex(
    c,
    is_forall,
    weight,
    quantifier_id,
    skolem_id,
    num_bound,
    bound,
    num_patterns,
    patterns,
    num_no_patterns,
    no_patterns,
    body,
  );
}