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
use z3_sys::*; use Solver; use Optimize; use Model; use Ast; 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>> { unsafe { let mut tmp : Z3_ast = ast.z3_ast; let res; { let guard = Z3_MUTEX.lock().unwrap(); res = Z3_model_eval(self.ctx.z3_ctx, self.z3_mdl, ast.z3_ast, Z3_TRUE, &mut tmp) } if res == Z3_TRUE { Some(Ast::new(self.ctx, tmp)) } else { None } } } } impl<'ctx> Drop for Model<'ctx> { fn drop(&mut self) { unsafe { let guard = Z3_MUTEX.lock().unwrap(); Z3_model_dec_ref(self.ctx.z3_ctx, self.z3_mdl); } } }