[−][src]Function z3_sys::Z3_mk_pattern
pub unsafe extern "C" fn Z3_mk_pattern(
c: Z3_context,
num_patterns: c_uint,
terms: *const Z3_ast
) -> Z3_pattern
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.