pub struct Pattern<'ctx> { /* private fields */ }
Expand description
A pattern for quantifier instantiation, used to guide quantifier instantiation.
Implementations§
source§impl<'ctx> Pattern<'ctx>
impl<'ctx> Pattern<'ctx>
sourcepub fn new(ctx: &'ctx Context, terms: &[&dyn Ast<'_>]) -> 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§
Auto Trait Implementations§
impl<'ctx> RefUnwindSafe for Pattern<'ctx>
impl<'ctx> !Send for Pattern<'ctx>
impl<'ctx> !Sync for Pattern<'ctx>
impl<'ctx> Unpin for Pattern<'ctx>
impl<'ctx> UnwindSafe for Pattern<'ctx>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more