Struct Z3Pattern 

pub struct Z3Pattern {
    pub terms: Vec<TermId>,
}

Analogue of z3::Pattern.

A pattern (a.k.a. trigger) is a list of terms that guides e-matching instantiation of a quantifier. In OxiZ a pattern is materialised as the list of trigger terms it carries; construct one with Z3Context::mk_pattern and attach it to a quantifier with Z3Context::forall_with_patterns / Z3Context::exists_with_patterns.

Fields

terms: Vec<TermId>

The trigger terms making up this pattern.

Implementations

impl Z3Pattern

pub fn len(&self) -> usize

Number of trigger terms in this pattern.

pub fn is_empty(&self) -> bool

Returns true if the pattern carries no trigger terms.

Trait Implementations

impl Clone for Z3Pattern

fn clone(&self) -> Z3Pattern

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Z3Pattern

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

Formats the value using the given formatter.