z3/
pattern.rs

1use ast::Ast;
2use std::convert::TryInto;
3use std::ffi::CStr;
4use std::fmt;
5use z3_sys::*;
6use Context;
7use Pattern;
8
9impl<'ctx> Pattern<'ctx> {
10    /// Create a pattern for quantifier instantiation.
11    ///
12    /// Z3 uses pattern matching to instantiate quantifiers. If a
13    /// pattern is not provided for a quantifier, then Z3 will
14    /// automatically compute a set of patterns for it. However, for
15    /// optimal performance, the user should provide the patterns.
16    ///
17    /// Patterns comprise a list of terms. The list should be
18    /// non-empty.  If the list comprises of more than one term, it is
19    /// a called a multi-pattern.
20    ///
21    /// In general, one can pass in a list of (multi-)patterns in the
22    /// quantifier constructor.
23    ///
24    /// # See also:
25    ///
26    /// - `ast::forall_const()`
27    /// - `ast::exists_const()`
28    pub fn new(ctx: &'ctx Context, terms: &[&dyn Ast]) -> Pattern<'ctx> {
29        assert!(!terms.is_empty());
30        assert!(terms.iter().all(|t| t.get_ctx().z3_ctx == ctx.z3_ctx));
31
32        let terms: Vec<_> = terms.iter().map(|t| t.get_z3_ast()).collect();
33
34        Pattern {
35            ctx,
36            z3_pattern: unsafe {
37                let p = Z3_mk_pattern(
38                    ctx.z3_ctx,
39                    terms.len().try_into().unwrap(),
40                    terms.as_ptr() as *const Z3_ast,
41                );
42                Z3_inc_ref(ctx.z3_ctx, p as Z3_ast);
43                p
44            },
45        }
46    }
47}
48
49impl<'ctx> fmt::Debug for Pattern<'ctx> {
50    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
51        let p = unsafe { Z3_pattern_to_string(self.ctx.z3_ctx, self.z3_pattern) };
52        if p.is_null() {
53            return Result::Err(fmt::Error);
54        }
55        match unsafe { CStr::from_ptr(p) }.to_str() {
56            Ok(s) => write!(f, "{}", s),
57            Err(_) => Result::Err(fmt::Error),
58        }
59    }
60}
61
62impl<'ctx> fmt::Display for Pattern<'ctx> {
63    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
64        <Self as fmt::Debug>::fmt(self, f)
65    }
66}
67
68impl<'ctx> Drop for Pattern<'ctx> {
69    fn drop(&mut self) {
70        unsafe {
71            Z3_dec_ref(self.ctx.z3_ctx, self.z3_pattern as Z3_ast);
72        }
73    }
74}
z3/pattern.rs

z3/
pattern.rs
