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
use z3_sys::*; use Context; use Optimize; use Model; use Ast; use Z3_MUTEX; impl<'ctx> Optimize<'ctx> { pub fn new(ctx: &'ctx Context) -> Optimize<'ctx> { Optimize { ctx: ctx, z3_opt: unsafe { let guard = Z3_MUTEX.lock().unwrap(); let opt = Z3_mk_optimize(ctx.z3_ctx); Z3_optimize_inc_ref(ctx.z3_ctx, opt); opt } } } pub fn assert(&self, ast: &Ast<'ctx>) { unsafe { let guard = Z3_MUTEX.lock().unwrap(); Z3_optimize_assert(self.ctx.z3_ctx, self.z3_opt, ast.z3_ast); } } pub fn maximize(&self, ast: &Ast<'ctx>) { unsafe { let guard = Z3_MUTEX.lock().unwrap(); Z3_optimize_maximize(self.ctx.z3_ctx, self.z3_opt, ast.z3_ast); } } pub fn minimize(&self, ast: &Ast<'ctx>) { unsafe { let guard = Z3_MUTEX.lock().unwrap(); Z3_optimize_minimize(self.ctx.z3_ctx, self.z3_opt, ast.z3_ast); } } pub fn check(&self) -> bool { unsafe { let guard = Z3_MUTEX.lock().unwrap(); Z3_optimize_check(self.ctx.z3_ctx, self.z3_opt) == Z3_L_TRUE } } pub fn get_model(&self) -> Model<'ctx> { Model::of_optimize(self) } } impl<'ctx> Drop for Optimize<'ctx> { fn drop(&mut self) { unsafe { let guard = Z3_MUTEX.lock().unwrap(); Z3_optimize_dec_ref(self.ctx.z3_ctx, self.z3_opt); } } }