Struct Pattern 

pub struct Pattern { /* private fields */ }

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

Implementations

impl Pattern

pub fn new(terms: &[&dyn Ast]) -> 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.

See also:

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

Trait Implementations

impl Debug for Pattern

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

Formats the value using the given formatter.

impl Display for Pattern

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

Formats the value using the given formatter.

impl Drop for Pattern

fn drop(&mut self)

Executes the destructor for this type.