mk_pattern method

Z3_pattern mk_pattern(Z3_context c, int num_patterns, Pointer<Z3_ast> terms)

@name Quantifiers / /**@{/ /** \brief Create a pattern for quantifier instantiation.

Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.

Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is a called a multi-pattern.

In general, one can pass in a list of (multi-)patterns in the quantifier constructor.

\sa Z3_mk_forall \sa Z3_mk_exists

def_API('Z3_mk_pattern', PATTERN, (_in(CONTEXT), _in(UINT), _in_array(1, AST)))

Implementation

Z3_pattern mk_pattern(
  Z3_context c,
  int num_patterns,
  ffi.Pointer<Z3_ast> terms,
) {
  return _mk_pattern(
    c,
    num_patterns,
    terms,
  );
}