z3/
model.rs

1use std::ffi::CStr;
2use std::fmt;
3use z3_sys::*;
4
5use crate::{Context, FuncDecl, FuncInterp, Model, Optimize, Solver, Translate, ast::Ast};
6
7impl Model {
8    unsafe fn wrap(ctx: &Context, z3_mdl: Z3_model) -> Model {
9        unsafe {
10            Z3_model_inc_ref(ctx.z3_ctx.0, z3_mdl);
11        }
12        Model {
13            ctx: ctx.clone(),
14            z3_mdl,
15        }
16    }
17
18    pub fn of_solver(slv: &Solver) -> Option<Model> {
19        unsafe {
20            let m = Z3_solver_get_model(slv.ctx.z3_ctx.0, slv.z3_slv);
21            Some(Self::wrap(&slv.ctx, m?))
22        }
23    }
24
25    pub fn of_optimize(opt: &Optimize) -> Option<Model> {
26        unsafe {
27            let m = Z3_optimize_get_model(opt.ctx.z3_ctx.0, opt.z3_opt);
28            Some(Self::wrap(&opt.ctx, m?))
29        }
30    }
31
32    /// Returns the interpretation of the given `ast` in the `Model`
33    /// Returns `None` if there is no interpretation in the `Model`
34    pub fn get_const_interp<T: Ast>(&self, ast: &T) -> Option<T> {
35        let func = ast.safe_decl().ok()?;
36
37        let ret =
38            unsafe { Z3_model_get_const_interp(self.ctx.z3_ctx.0, self.z3_mdl, func.z3_func_decl) };
39        Some(unsafe { T::wrap(&self.ctx, ret?) })
40    }
41
42    /// Returns the interpretation of the given `f` in the `Model`
43    /// Returns `None` if there is no interpretation in the `Model`
44    pub fn get_func_interp(&self, f: &FuncDecl) -> Option<FuncInterp> {
45        if f.arity() == 0 {
46            let ret = unsafe {
47                Z3_model_get_const_interp(self.ctx.z3_ctx.0, self.z3_mdl, f.z3_func_decl)
48            }?;
49            let sort_kind = unsafe {
50                Z3_get_sort_kind(
51                    self.ctx.z3_ctx.0,
52                    Z3_get_range(self.ctx.z3_ctx.0, f.z3_func_decl).unwrap(),
53                )
54            };
55            match sort_kind {
56                SortKind::Array => {
57                    if unsafe { Z3_is_as_array(self.ctx.z3_ctx.0, ret) } {
58                        let fd = unsafe {
59                            FuncDecl::wrap(
60                                &self.ctx,
61                                Z3_get_as_array_func_decl(self.ctx.z3_ctx.0, ret).unwrap(),
62                            )
63                        };
64                        self.get_func_interp(&fd)
65                    } else {
66                        None
67                    }
68                }
69                _ => None,
70            }
71        } else {
72            let ret =
73                unsafe { Z3_model_get_func_interp(self.ctx.z3_ctx.0, self.z3_mdl, f.z3_func_decl) };
74            Some(unsafe { FuncInterp::wrap(&self.ctx, ret?) })
75        }
76    }
77
78    pub fn eval<T>(&self, ast: &T, model_completion: bool) -> Option<T>
79    where
80        T: Ast,
81    {
82        let mut tmp: Z3_ast = ast.get_z3_ast();
83        let res = {
84            unsafe {
85                Z3_model_eval(
86                    self.ctx.z3_ctx.0,
87                    self.z3_mdl,
88                    ast.get_z3_ast(),
89                    model_completion,
90                    &mut tmp,
91                )
92            }
93        };
94        if res {
95            Some(unsafe { T::wrap(&self.ctx, tmp) })
96        } else {
97            None
98        }
99    }
100
101    fn len(&self) -> u32 {
102        unsafe {
103            Z3_model_get_num_consts(self.ctx.z3_ctx.0, self.z3_mdl)
104                + Z3_model_get_num_funcs(self.ctx.z3_ctx.0, self.z3_mdl)
105        }
106    }
107
108    pub fn iter<'a>(&'a self) -> ModelIter<'a> {
109        self.into_iter()
110    }
111}
112
113impl fmt::Display for Model {
114    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
115        let p = unsafe { Z3_model_to_string(self.ctx.z3_ctx.0, self.z3_mdl) };
116        if p.is_null() {
117            return Result::Err(fmt::Error);
118        }
119        match unsafe { CStr::from_ptr(p) }.to_str() {
120            Ok(s) => write!(f, "{s}"),
121            Err(_) => Result::Err(fmt::Error),
122        }
123    }
124}
125
126impl fmt::Debug for Model {
127    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
128        <Self as fmt::Display>::fmt(self, f)
129    }
130}
131
132impl Drop for Model {
133    fn drop(&mut self) {
134        unsafe { Z3_model_dec_ref(self.ctx.z3_ctx.0, self.z3_mdl) };
135    }
136}
137
138#[derive(Debug)]
139/// <https://z3prover.github.io/api/html/classz3py_1_1_model_ref.html#a7890b7c9bc70cf2a26a343c22d2c8367>
140pub struct ModelIter<'a> {
141    model: &'a Model,
142    idx: u32,
143    len: u32,
144}
145
146impl<'a> IntoIterator for &'a Model {
147    type Item = FuncDecl;
148    type IntoIter = ModelIter<'a>;
149
150    fn into_iter(self) -> Self::IntoIter {
151        ModelIter {
152            model: self,
153            idx: 0,
154            len: self.len(),
155        }
156    }
157}
158
159impl Iterator for ModelIter<'_> {
160    type Item = FuncDecl;
161
162    fn next(&mut self) -> Option<Self::Item> {
163        if self.idx >= self.len {
164            None
165        } else {
166            let num_consts =
167                unsafe { Z3_model_get_num_consts(self.model.ctx.z3_ctx.0, self.model.z3_mdl) };
168            if self.idx < num_consts {
169                let const_decl = unsafe {
170                    Z3_model_get_const_decl(self.model.ctx.z3_ctx.0, self.model.z3_mdl, self.idx)
171                        .unwrap()
172                };
173                self.idx += 1;
174                Some(unsafe { FuncDecl::wrap(&self.model.ctx, const_decl) })
175            } else {
176                let func_decl = unsafe {
177                    Z3_model_get_func_decl(
178                        self.model.ctx.z3_ctx.0,
179                        self.model.z3_mdl,
180                        self.idx - num_consts,
181                    )
182                    .unwrap()
183                };
184                self.idx += 1;
185                Some(unsafe { FuncDecl::wrap(&self.model.ctx, func_decl) })
186            }
187        }
188    }
189
190    fn size_hint(&self) -> (usize, Option<usize>) {
191        let len = (self.len - self.idx) as usize;
192        (len, Some(len))
193    }
194}
195
196unsafe impl Translate for Model {
197    fn translate(&self, dest: &Context) -> Model {
198        unsafe {
199            Model::wrap(
200                dest,
201                Z3_model_translate(self.ctx.z3_ctx.0, self.z3_mdl, dest.z3_ctx.0).unwrap(),
202            )
203        }
204    }
205}
206
207#[cfg(test)]
208mod tests {
209    use crate::Solver;
210    use crate::ast::Bool;
211
212    #[test]
213    fn test_unsat() {
214        use crate::SatResult;
215        let solver = Solver::new();
216        solver.assert(Bool::from_bool(false));
217        assert_eq!(solver.check(), SatResult::Unsat);
218        assert!(solver.get_model().is_none());
219    }
220}
z3/model.rs

z3/
model.rs
