z3/
func_interp.rs

1use std::fmt;
2use z3_sys::*;
3
4use crate::{
5    AstVector, Context, FuncEntry, FuncInterp,
6    ast::{Ast, Dynamic},
7};
8
9impl FuncInterp {
10    pub(crate) unsafe fn wrap(ctx: &Context, z3_func_interp: Z3_func_interp) -> Self {
11        unsafe {
12            Z3_func_interp_inc_ref(ctx.z3_ctx.0, z3_func_interp);
13        }
14
15        Self {
16            ctx: ctx.clone(),
17            z3_func_interp,
18        }
19    }
20
21    /// Returns the number of arguments in the function interpretation.
22    pub fn get_arity(&self) -> usize {
23        unsafe { Z3_func_interp_get_arity(self.ctx.z3_ctx.0, self.z3_func_interp) as usize }
24    }
25
26    /// Returns the number of entries in the function interpretation.
27    pub fn get_num_entries(&self) -> u32 {
28        unsafe { Z3_func_interp_get_num_entries(self.ctx.z3_ctx.0, self.z3_func_interp) }
29    }
30
31    /// Adds an entry to the function interpretation.
32    pub fn add_entry(&self, args: &[Dynamic], value: &Dynamic) {
33        let v: AstVector = args.into();
34        unsafe {
35            Z3_func_interp_add_entry(
36                self.ctx.z3_ctx.0,
37                self.z3_func_interp,
38                v.z3_ast_vector,
39                value.z3_ast,
40            );
41        }
42    }
43
44    /// Returns the entries of the function interpretation.
45    pub fn get_entries(&self) -> Vec<FuncEntry> {
46        (0..self.get_num_entries())
47            .map(|i| unsafe {
48                FuncEntry::wrap(
49                    &self.ctx,
50                    Z3_func_interp_get_entry(self.ctx.z3_ctx.0, self.z3_func_interp, i).unwrap(),
51                )
52            })
53            .collect()
54    }
55
56    /// Returns the else value of the function interpretation.
57    /// Returns None if the else value is not set by Z3.
58    pub fn get_else(&self) -> Dynamic {
59        unsafe {
60            Dynamic::wrap(
61                &self.ctx,
62                Z3_func_interp_get_else(self.ctx.z3_ctx.0, self.z3_func_interp).unwrap(),
63            )
64        }
65    }
66
67    /// Sets the else value of the function interpretation.
68    pub fn set_else(&self, ast: &Dynamic) {
69        unsafe { Z3_func_interp_set_else(self.ctx.z3_ctx.0, self.z3_func_interp, ast.z3_ast) }
70    }
71}
72
73impl fmt::Display for FuncInterp {
74    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
75        write!(f, "[")?;
76        self.get_entries().into_iter().try_for_each(|e| {
77            let n = e.get_num_args();
78            if n > 1 {
79                write!(f, "[")?;
80            };
81            write!(
82                f,
83                "{}",
84                e.get_args()
85                    .into_iter()
86                    .map(|a| a.to_string())
87                    .collect::<Vec<_>>()
88                    .join(", ")
89            )?;
90            if n > 1 {
91                write!(f, "]")?;
92            }
93            write!(f, " -> {}, ", e.get_value())
94        })?;
95        write!(f, "else -> {}", self.get_else())?;
96        write!(f, "]")
97    }
98}
99
100impl fmt::Debug for FuncInterp {
101    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
102        <Self as fmt::Display>::fmt(self, f)
103    }
104}
105
106impl Drop for FuncInterp {
107    fn drop(&mut self) {
108        unsafe {
109            Z3_func_interp_dec_ref(self.ctx.z3_ctx.0, self.z3_func_interp);
110        }
111    }
112}
z3/func_interp.rs

z3/
func_interp.rs
