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 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
use std::ffi::CStr; use std::fmt; use z3_sys::*; use Context; use Params; use Symbol; use Z3_MUTEX; impl<'ctx> Params<'ctx> { pub fn new(ctx: &'ctx Context) -> Params<'ctx> { Params { ctx, z3_params: unsafe { let guard = Z3_MUTEX.lock().unwrap(); let p = Z3_mk_params(ctx.z3_ctx); Z3_params_inc_ref(ctx.z3_ctx, p); p }, } } pub fn set_symbol<K: Into<Symbol>, V: Into<Symbol>>(&mut self, k: K, v: V) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_params_set_symbol( self.ctx.z3_ctx, self.z3_params, k.into().as_z3_symbol(self.ctx), v.into().as_z3_symbol(self.ctx), ) }; } pub fn set_bool<K: Into<Symbol>>(&mut self, k: K, v: bool) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_params_set_bool( self.ctx.z3_ctx, self.z3_params, k.into().as_z3_symbol(self.ctx), v, ) }; } pub fn set_f64<K: Into<Symbol>>(&mut self, k: K, v: f64) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_params_set_double( self.ctx.z3_ctx, self.z3_params, k.into().as_z3_symbol(self.ctx), v, ) }; } pub fn set_u32<K: Into<Symbol>>(&mut self, k: K, v: u32) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_params_set_uint( self.ctx.z3_ctx, self.z3_params, k.into().as_z3_symbol(self.ctx), v, ) }; } } impl<'ctx> fmt::Display for Params<'ctx> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { let p = unsafe { Z3_params_to_string(self.ctx.z3_ctx, self.z3_params) }; 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> fmt::Debug for Params<'ctx> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { <Self as fmt::Display>::fmt(self, f) } } impl<'ctx> Drop for Params<'ctx> { fn drop(&mut self) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_params_dec_ref(self.ctx.z3_ctx, self.z3_params) }; } }