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
use std::ffi::CString;
use z3_sys::*;
use Config;
use Z3_MUTEX;
impl Config {
pub fn new() -> Config {
Config {
kvs: Vec::new(),
z3_cfg: unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let p = Z3_mk_config();
debug!("new config {:p}", p);
p
},
}
}
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));
let guard = Z3_MUTEX.lock().unwrap();
unsafe {
Z3_set_param_value(
self.z3_cfg,
self.kvs.last().unwrap().0.as_ptr(),
self.kvs.last().unwrap().1.as_ptr(),
)
};
}
pub fn set_bool_param_value(&mut self, k: &str, v: bool) {
self.set_param_value(k, if v { "true" } else { "false" });
}
pub fn set_proof_generation(&mut self, b: bool) {
self.set_bool_param_value("proof", b);
}
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) {
let guard = Z3_MUTEX.lock().unwrap();
unsafe { Z3_del_config(self.z3_cfg) };
}
}