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
use ast::Ast; use std::ffi::CStr; use std::fmt; use z3_sys::*; 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<T>(&self, ast: &T) -> Option<T> where T: Ast<'ctx>, { let mut tmp: Z3_ast = ast.get_z3_ast(); let res = { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_model_eval( self.ctx.z3_ctx, self.z3_mdl, ast.get_z3_ast(), true, &mut tmp, ) } }; if res { Some(T::new(self.ctx, tmp)) } else { None } } } impl<'ctx> fmt::Display for Model<'ctx> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { let p = unsafe { Z3_model_to_string(self.ctx.z3_ctx, self.z3_mdl) }; if p.is_null() { return Result::Err(fmt::Error); } match unsafe { CStr::from_ptr(p) }.to_str() { Ok(s) => write!(f, "{}", s), Err(_) => Result::Err(fmt::Error), } } } 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) }; } }