[−][src]Struct z3::Pattern
A pattern for quantifier instantiation, used to guide quantifier instantiation.
Methods
impl<'ctx> Pattern<'ctx>
[src]
pub fn new(ctx: &'ctx Context, terms: &[&Dynamic]) -> Pattern<'ctx>
[src]
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> Drop for Pattern<'ctx>
[src]
impl<'ctx> Display for Pattern<'ctx>
[src]
impl<'ctx> Debug for Pattern<'ctx>
[src]
Auto Trait Implementations
impl<'ctx> !Send for Pattern<'ctx>
impl<'ctx> Unpin for Pattern<'ctx>
impl<'ctx> !Sync for Pattern<'ctx>
impl<'ctx> UnwindSafe for Pattern<'ctx>
impl<'ctx> RefUnwindSafe for Pattern<'ctx>
Blanket Implementations
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,