z3/
config.rs

1use log::debug;
2use std::ffi::CString;
3
4use z3_sys::*;
5
6use crate::Config;
7
8impl Config {
9    /// Create a configuration object for the Z3 context object.
10    ///
11    /// Configurations are created in order to assign parameters
12    /// prior to creating contexts for Z3 interaction. For example,
13    /// if the users wishes to use proof generation, then call:
14    ///
15    /// ```
16    /// use z3::Config;
17    ///
18    /// let mut cfg = Config::new();
19    /// cfg.set_proof_generation(true);
20    /// ```
21    ///
22    /// # See also
23    ///
24    /// - [`with_z3_config`](crate::with_z3_config)
25    pub fn new() -> Config {
26        Config {
27            kvs: Vec::new(),
28            z3_cfg: unsafe {
29                let p = Z3_mk_config().unwrap();
30                debug!("new config {p:p}");
31                p
32            },
33        }
34    }
35
36    /// Set a configuration parameter.
37    ///
38    /// # See also
39    ///
40    /// - [`Config::set_bool_param_value()`]
41    pub fn set_param_value(&mut self, k: &str, v: &str) {
42        let ks = CString::new(k).unwrap();
43        let vs = CString::new(v).unwrap();
44        self.kvs.push((ks, vs));
45        unsafe {
46            Z3_set_param_value(
47                self.z3_cfg,
48                self.kvs.last().unwrap().0.as_ptr(),
49                self.kvs.last().unwrap().1.as_ptr(),
50            );
51        };
52    }
53
54    /// Set a configuration parameter.
55    ///
56    /// This is a helper function.
57    ///
58    /// # See also
59    ///
60    /// - [`Config::set_param_value()`]
61    pub fn set_bool_param_value(&mut self, k: &str, v: bool) {
62        self.set_param_value(k, if v { "true" } else { "false" });
63    }
64
65    /// Enable or disable proof generation.
66    ///
67    /// # See also
68    ///
69    /// - [`Solver::check()`](crate::Solver::check)
70    /// - [`Solver::get_proof()`](crate::Solver::get_proof)
71    pub fn set_proof_generation(&mut self, b: bool) {
72        self.set_bool_param_value("proof", b);
73    }
74
75    /// Enable or disable model generation.
76    ///
77    /// # See also
78    ///
79    /// - [`Solver::check()`](crate::Solver::check)
80    /// - [`Solver::get_model()`](crate::Solver::get_model)
81    pub fn set_model_generation(&mut self, b: bool) {
82        self.set_bool_param_value("model", b);
83    }
84
85    pub fn set_debug_ref_count(&mut self, b: bool) {
86        self.set_bool_param_value("debug_ref_count", b);
87    }
88
89    pub fn set_timeout_msec(&mut self, ms: u64) {
90        self.set_param_value("timeout", &format!("{ms}"));
91    }
92}
93
94impl Default for Config {
95    fn default() -> Self {
96        Self::new()
97    }
98}
99
100impl Drop for Config {
101    fn drop(&mut self) {
102        unsafe { Z3_del_config(self.z3_cfg) };
103    }
104}
z3/config.rs

z3/
config.rs
