1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

use std::ffi::CString;
use z3_sys::*;
use Config;

impl Config {
    /// Create a configuration object for the Z3 context object.
    ///
    /// Configurations are created in order to assign parameters
    /// prior to creating contexts for Z3 interaction. For example,
    /// if the users wishes to use proof generation, then call:
    ///
    /// ```
    /// use z3::Config;
    ///
    /// let mut cfg = Config::new();
    /// cfg.set_proof_generation(true);
    /// ```
    ///
    /// # See also
    ///
    /// - [`Context::new()`](crate::Context::new)
    pub fn new() -> Config {
        Config {
            kvs: Vec::new(),
            z3_cfg: unsafe {
                let p = Z3_mk_config();
                debug!("new config {:p}", p);
                p
            },
        }
    }

    /// Set a configuration parameter.
    ///
    /// # See also
    ///
    /// - [`Config::set_bool_param_value()`]
    pub fn set_param_value(&mut self, k: &str, v: &str) {
        let ks = CString::new(k).unwrap();
        let vs = CString::new(v).unwrap();
        self.kvs.push((ks, vs));
        unsafe {
            Z3_set_param_value(
                self.z3_cfg,
                self.kvs.last().unwrap().0.as_ptr(),
                self.kvs.last().unwrap().1.as_ptr(),
            )
        };
    }

    /// Set a configuration parameter.
    ///
    /// This is a helper function.
    ///
    /// # See also
    ///
    /// - [`Config::set_param_value()`]
    pub fn set_bool_param_value(&mut self, k: &str, v: bool) {
        self.set_param_value(k, if v { "true" } else { "false" });
    }

    /// Enable or disable proof generation.
    ///
    /// # See also
    ///
    /// - [`Solver::check()`](crate::Solver::check)
    /// - [`Solver::get_proof()`](crate::Solver::get_proof)
    pub fn set_proof_generation(&mut self, b: bool) {
        self.set_bool_param_value("proof", b);
    }

    /// Enable or disable model generation.
    ///
    /// # See also
    ///
    /// - [`Solver::check()`](crate::Solver::check)
    /// - [`Solver::get_model()`](crate::Solver::get_model)
    pub fn set_model_generation(&mut self, b: bool) {
        self.set_bool_param_value("model", b);
    }

    pub fn set_debug_ref_count(&mut self, b: bool) {
        self.set_bool_param_value("debug_ref_count", b);
    }

    pub fn set_timeout_msec(&mut self, ms: u64) {
        self.set_param_value("timeout", &format!("{}", ms));
    }
}

impl Default for Config {
    fn default() -> Self {
        Self::new()
    }
}

impl Drop for Config {
    fn drop(&mut self) {
        unsafe { Z3_del_config(self.z3_cfg) };
    }
}