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 std::ptr::null_mut; use z3_sys; use Ast; use Check; use Context; use Optimize; use Solver; pub struct Model<'c> { pub(crate) model: z3_sys::Z3_model, context: &'c Context, } impl<'c> Model<'c> { pub fn new(context: &'c Context, solver: &Solver) -> Option<Model<'c>> { if solver.check() != Check::Sat { None } else { let m = unsafe { z3_sys::Z3_solver_get_model(context.context, solver.solver) }; let model = Model { model: m, context: context, }; model.inc_ref(); Some(model) } } pub fn new_optimize(context: &'c Context, optimize: &Optimize) -> Option<Model<'c>> { if optimize.check() != Check::Sat { None } else { let m = unsafe { z3_sys::Z3_optimize_get_model(context.context, optimize.optimize) }; let model = Model { model: m, context: context, }; model.inc_ref(); Some(model) } } pub fn get_const_interp(&self, t: &Ast) -> Option<Ast> { let mut ast: z3_sys::Z3_ast = null_mut(); let r = unsafe { z3_sys::Z3_model_eval( self.context.context, self.model, t.ast, true, &mut ast as *mut z3_sys::Z3_ast, ) }; if r { Some(Ast { ast: ast }) } else { None } } fn inc_ref(&self) { unsafe { z3_sys::Z3_model_inc_ref(self.context.context, self.model); } } fn dec_ref(&self) { unsafe { z3_sys::Z3_model_dec_ref(self.context.context, self.model); } } } impl<'c> Drop for Model<'c> { fn drop(&mut self) { self.dec_ref(); } }