z3/
func_interp.rs

1use std::fmt;
2use z3_sys::*;
3
4use crate::{
5    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        unsafe {
34            let v = Z3_mk_ast_vector(self.ctx.z3_ctx.0).unwrap();
35            Z3_ast_vector_inc_ref(self.ctx.z3_ctx.0, v);
36            args.iter()
37                .for_each(|a| Z3_ast_vector_push(self.ctx.z3_ctx.0, v, a.z3_ast));
38
39            Z3_func_interp_add_entry(self.ctx.z3_ctx.0, self.z3_func_interp, v, value.z3_ast);
40        }
41    }
42
43    /// Returns the entries of the function interpretation.
44    pub fn get_entries(&self) -> Vec<FuncEntry> {
45        (0..self.get_num_entries())
46            .map(|i| unsafe {
47                FuncEntry::wrap(
48                    &self.ctx,
49                    Z3_func_interp_get_entry(self.ctx.z3_ctx.0, self.z3_func_interp, i).unwrap(),
50                )
51            })
52            .collect()
53    }
54
55    /// Returns the else value of the function interpretation.
56    /// Returns None if the else value is not set by Z3.
57    pub fn get_else(&self) -> Dynamic {
58        unsafe {
59            Dynamic::wrap(
60                &self.ctx,
61                Z3_func_interp_get_else(self.ctx.z3_ctx.0, self.z3_func_interp).unwrap(),
62            )
63        }
64    }
65
66    /// Sets the else value of the function interpretation.
67    pub fn set_else(&self, ast: &Dynamic) {
68        unsafe { Z3_func_interp_set_else(self.ctx.z3_ctx.0, self.z3_func_interp, ast.z3_ast) }
69    }
70}
71
72impl fmt::Display for FuncInterp {
73    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
74        write!(f, "[")?;
75        self.get_entries().into_iter().try_for_each(|e| {
76            let n = e.get_num_args();
77            if n > 1 {
78                write!(f, "[")?;
79            };
80            write!(
81                f,
82                "{}",
83                e.get_args()
84                    .into_iter()
85                    .map(|a| a.to_string())
86                    .collect::<Vec<_>>()
87                    .join(", ")
88            )?;
89            if n > 1 {
90                write!(f, "]")?;
91            }
92            write!(f, " -> {}, ", e.get_value())
93        })?;
94        write!(f, "else -> {}", self.get_else())?;
95        write!(f, "]")
96    }
97}
98
99impl fmt::Debug for FuncInterp {
100    fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
101        <Self as fmt::Display>::fmt(self, f)
102    }
103}
104
105impl Drop for FuncInterp {
106    fn drop(&mut self) {
107        unsafe {
108            Z3_func_interp_dec_ref(self.ctx.z3_ctx.0, self.z3_func_interp);
109        }
110    }
111}
z3/func_interp.rs

z3/
func_interp.rs
