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
use std::ffi::CString;
use z3_sys::*;
use Config;
use Context;
use ContextHandle;
impl Context {
pub fn new(cfg: &Config) -> Context {
Context {
z3_ctx: unsafe {
let p = Z3_mk_context_rc(cfg.z3_cfg);
debug!("new context {:p}", p);
Z3_set_error_handler(p, None);
p
},
}
}
/// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
pub fn interrupt(&self) {
self.handle().interrupt()
}
/// Obtain a handle that can be used to interrupt computation from another thread.
///
/// # See also:
///
/// - [`ContextHandle`]
/// - [`ContextHandle::interrupt()`]
pub fn handle(&self) -> ContextHandle {
ContextHandle { ctx: self }
}
/// Update a global parameter.
///
/// # See also
///
/// - [`Context::update_bool_param_value()`]
pub fn update_param_value(&mut self, k: &str, v: &str) {
let ks = CString::new(k).unwrap();
let vs = CString::new(v).unwrap();
unsafe { Z3_update_param_value(self.z3_ctx, ks.as_ptr(), vs.as_ptr()) };
}
/// Update a global parameter.
///
/// This is a helper function.
///
/// # See also
///
/// - [`Context::update_param_value()`]
pub fn update_bool_param_value(&mut self, k: &str, v: bool) {
self.update_param_value(k, if v { "true" } else { "false" })
}
}
impl<'ctx> ContextHandle<'ctx> {
/// Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.
pub fn interrupt(&self) {
unsafe {
Z3_interrupt(self.ctx.z3_ctx);
}
}
}
unsafe impl<'ctx> Sync for ContextHandle<'ctx> {}
unsafe impl<'ctx> Send for ContextHandle<'ctx> {}
impl Drop for Context {
fn drop(&mut self) {
unsafe { Z3_del_context(self.z3_ctx) };
}
}