z3/
pattern.rs

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

z3/
pattern.rs
