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
use z3_sys::*;
use Ast;
use Model;
use Optimize;
use Solver;
use Z3_MUTEX;
impl<'ctx> Model<'ctx> {
pub fn of_solver(slv: &Solver<'ctx>) -> Model<'ctx> {
Model {
ctx: slv.ctx,
z3_mdl: unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let m = Z3_solver_get_model(slv.ctx.z3_ctx, slv.z3_slv);
Z3_model_inc_ref(slv.ctx.z3_ctx, m);
m
},
}
}
pub fn of_optimize(opt: &Optimize<'ctx>) -> Model<'ctx> {
Model {
ctx: opt.ctx,
z3_mdl: unsafe {
let guard = Z3_MUTEX.lock().unwrap();
let m = Z3_optimize_get_model(opt.ctx.z3_ctx, opt.z3_opt);
Z3_model_inc_ref(opt.ctx.z3_ctx, m);
m
},
}
}
pub fn eval(&self, ast: &Ast<'ctx>) -> Option<Ast<'ctx>> {
let mut tmp: Z3_ast = ast.z3_ast;
let res = {
let guard = Z3_MUTEX.lock().unwrap();
unsafe { Z3_model_eval(self.ctx.z3_ctx, self.z3_mdl, ast.z3_ast, true, &mut tmp) }
};
if res {
Some(Ast::new(self.ctx, tmp))
} else {
None
}
}
}
impl<'ctx> Drop for Model<'ctx> {
fn drop(&mut self) {
let guard = Z3_MUTEX.lock().unwrap();
unsafe { Z3_model_dec_ref(self.ctx.z3_ctx, self.z3_mdl) };
}
}