Struct z3::Pattern

pub struct Pattern<'ctx> { /* fields omitted */ }

A pattern for quantifier instantiation, used to guide quantifier instantiation.

Implementations

impl<'ctx> Pattern<'ctx>

pub fn new(ctx: &'ctx Context, terms: &[&dyn Ast<'_>]) -> Pattern<'ctx>

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.

See also:

• ast::forall_const()
• ast::exists_const()

Trait Implementations

impl<'ctx> Debug for Pattern<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for Pattern<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for Pattern<'ctx>

fn drop(&mut self)

Executes the destructor for this type.