From d417ca737534a424669458be78d0789217d6181f Mon Sep 17 00:00:00 2001 From: AndesVL <32360382+AndesVL@users.noreply.github.com> Date: Sun, 5 Jun 2022 05:29:09 +0200 Subject: [PATCH 1/3] added bindings for z3_param_descrs and related functions --- z3/src/lib.rs | 9 +++- z3/src/param_descrs.rs | 111 +++++++++++++++++++++++++++++++++++++++++ z3/src/solver.rs | 6 +++ z3/src/symbol.rs | 34 ++++++++++++- z3/src/tactic.rs | 6 +++ z3/tests/lib.rs | 34 +++++++++++++ 6 files changed, 198 insertions(+), 2 deletions(-) create mode 100644 z3/src/param_descrs.rs diff --git a/z3/src/lib.rs b/z3/src/lib.rs index 0e7d80d5..19028b18 100644 --- a/z3/src/lib.rs +++ b/z3/src/lib.rs @@ -15,7 +15,7 @@ extern crate num; use std::ffi::CString; use std::sync::Mutex; use z3_sys::*; -pub use z3_sys::{AstKind, GoalPrec, SortKind}; +pub use z3_sys::{AstKind, GoalPrec, SortKind, SymbolKind}; pub mod ast; mod config; @@ -28,6 +28,7 @@ mod model; mod ops; mod optimize; mod params; +mod param_descrs; mod pattern; mod probe; mod solver; @@ -238,6 +239,12 @@ pub struct Params<'ctx> { z3_params: Z3_params, } +/// Provides a collection of parameter names, their types, default values and documentation strings. +pub struct ParamDescrs<'ctx> { + ctx: &'ctx Context, + z3_param_descrs: Z3_param_descrs, +} + /// Result of a satisfiability query. #[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum SatResult { diff --git a/z3/src/param_descrs.rs b/z3/src/param_descrs.rs new file mode 100644 index 00000000..2ef3df9a --- /dev/null +++ b/z3/src/param_descrs.rs @@ -0,0 +1,111 @@ +use std::ffi::CStr; +use std::fmt; +use std::str::Utf8Error; +use z3_sys::*; +use Context; +use ParamDescrs; +use Solver; +use Symbol; +use Tactic; +use Z3_MUTEX; + +impl<'ctx> ParamDescrs<'ctx> { + fn new_from_z3_type(ctx: &'ctx Context, z3_param_descrs: Z3_param_descrs) -> ParamDescrs<'ctx> { + ParamDescrs { + ctx, + z3_param_descrs, + } + } + + pub fn from_tactic(tactic: &'ctx Tactic<'ctx>) -> ParamDescrs<'ctx> { + let _guard = Z3_MUTEX.lock().unwrap(); + unsafe { + let ctx = tactic.ctx; + let z3_param_descrs = Z3_tactic_get_param_descrs(ctx.z3_ctx, tactic.z3_tactic); + let pd = ParamDescrs::new_from_z3_type(ctx, z3_param_descrs); + Z3_param_descrs_inc_ref(ctx.z3_ctx, z3_param_descrs); + pd + } + } + + pub fn from_solver(solver: &'ctx Solver<'ctx>) -> ParamDescrs<'ctx> { + let _guard = Z3_MUTEX.lock().unwrap(); + unsafe { + let ctx = solver.ctx; + let z3_param_descrs = Z3_solver_get_param_descrs(ctx.z3_ctx, solver.z3_slv); + let pd = ParamDescrs::new_from_z3_type(ctx, z3_param_descrs); + Z3_param_descrs_inc_ref(ctx.z3_ctx, z3_param_descrs); + pd + } + } + + pub fn get_size(&self) -> u32 { + unsafe { Z3_param_descrs_size(self.ctx.z3_ctx, self.z3_param_descrs) } + } + + pub fn get_param_kind>(&self, n: N) -> ParamKind { + let _guard = Z3_MUTEX.lock().unwrap(); + unsafe { + Z3_param_descrs_get_kind( + self.ctx.z3_ctx, + self.z3_param_descrs, + n.into().as_z3_symbol(self.ctx), + ) + } + } + + pub fn get_param_name(&self, index: u32) -> Option { + let n = { + let _guard = Z3_MUTEX.lock().unwrap(); + let p = self.get_size(); + if index > p { + return None; + } + unsafe { Z3_param_descrs_get_name(self.ctx.z3_ctx, self.z3_param_descrs, index) } + }; + Symbol::new_from_z3_symbol(self.ctx, n) + } + + pub fn get_param_documentation + Clone>(&'ctx self, n: N) -> Option<&'ctx str> { + if let ParamKind::Invalid = self.get_param_kind(n.clone()) { + return None; + } + let _guard = Z3_MUTEX.lock().unwrap(); + unsafe { + let d = Z3_param_descrs_get_documentation( + self.ctx.z3_ctx, + self.z3_param_descrs, + n.into().as_z3_symbol(self.ctx), + ); + CStr::from_ptr(d).to_str().ok() + } + } +} + +impl<'ctx> fmt::Display for ParamDescrs<'ctx> { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + let p = unsafe { Z3_param_descrs_to_string(self.ctx.z3_ctx, self.z3_param_descrs) }; + 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 ParamDescrs<'ctx> { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + ::fmt(self, f) + } +} + +impl<'ctx> Drop for ParamDescrs<'ctx> { + fn drop(&mut self) { + let _guard = Z3_MUTEX.lock().unwrap(); + unsafe { + Z3_param_descrs_dec_ref(self.ctx.z3_ctx, self.z3_param_descrs); + } + } +} diff --git a/z3/src/solver.rs b/z3/src/solver.rs index 22957392..df762b81 100644 --- a/z3/src/solver.rs +++ b/z3/src/solver.rs @@ -11,6 +11,8 @@ use Solver; use Symbol; use Z3_MUTEX; +use crate::ParamDescrs; + impl<'ctx> Solver<'ctx> { /// Create a new solver. This solver is a "combined solver" /// that internally uses a non-incremental (`solver1`) and an @@ -315,6 +317,10 @@ impl<'ctx> Solver<'ctx> { let _guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_set_params(self.ctx.z3_ctx, self.z3_slv, params.z3_params) }; } + + pub fn get_param_descrs(&'ctx self) -> ParamDescrs<'ctx> { + ParamDescrs::from_solver(&self) + } } impl<'ctx> fmt::Display for Solver<'ctx> { diff --git a/z3/src/symbol.rs b/z3/src/symbol.rs index 302fd742..0fa8bfa4 100644 --- a/z3/src/symbol.rs +++ b/z3/src/symbol.rs @@ -1,7 +1,10 @@ -use std::ffi::CString; +use std::convert::TryInto; +use std::ffi::{CStr, CString}; +use std::fmt; use z3_sys::*; use Context; use Symbol; +use Z3_MUTEX; impl Symbol { pub fn as_z3_symbol(&self, ctx: &Context) -> Z3_symbol { @@ -14,6 +17,26 @@ impl Symbol { } } } + + pub fn new_from_z3_symbol(ctx: &Context, z3_symbol: Z3_symbol) -> Option { + let _guard = Z3_MUTEX.lock().unwrap(); + unsafe { + let kind = Z3_get_symbol_kind(ctx.z3_ctx, z3_symbol); + match kind { + SymbolKind::Int => Z3_get_symbol_int(ctx.z3_ctx, z3_symbol) + .try_into() + .ok() + .map(|i| Symbol::Int(i)), + SymbolKind::String => { + let s = Z3_get_symbol_string(ctx.z3_ctx, z3_symbol); + CStr::from_ptr(s) + .to_str() + .ok() + .map(|s| Symbol::String(s.to_owned())) + } + } + } + } } impl From for Symbol { @@ -33,3 +56,12 @@ impl From<&str> for Symbol { Symbol::String(val.to_owned()) } } + +impl<'ctx> fmt::Display for Symbol { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + match self { + Symbol::Int(i) => write!(f, "{}", i), + Symbol::String(s) => write!(f, "{}", s), + } + } +} diff --git a/z3/src/tactic.rs b/z3/src/tactic.rs index e7ab5f6e..23c1b4dc 100644 --- a/z3/src/tactic.rs +++ b/z3/src/tactic.rs @@ -15,6 +15,8 @@ use Params; use Tactic; use Z3_MUTEX; +use crate::ParamDescrs; + impl<'ctx> ApplyResult<'ctx> { pub fn list_subgoals(self) -> impl Iterator> { let num_subgoals = unsafe { @@ -242,6 +244,10 @@ impl<'ctx> Tactic<'ctx> { z3_apply_result, }) } + + pub fn get_param_descrs(&'ctx self) -> ParamDescrs<'ctx> { + ParamDescrs::from_tactic(&self) + } } impl<'ctx> fmt::Display for Tactic<'ctx> { diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index c3142d8a..4ff7d234 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -303,6 +303,40 @@ fn test_params() { assert_eq!(solver.check(), SatResult::Sat); } +#[test] +fn test_param_descrs() { + let _ = env_logger::try_init(); + let cfg = Config::new(); + let ctx = Context::new(&cfg); + let solver = Solver::new(&ctx); + + let param_descrs = ParamDescrs::from_solver(&solver); + let size = param_descrs.get_size(); + assert!(size > 0); + let name = param_descrs.get_param_name(0); + assert!(name.is_some()); + let kind = param_descrs.get_param_kind("iDontExist"); + assert_eq!(kind, z3_sys::ParamKind::Invalid); + let kind = param_descrs.get_param_kind("model"); + assert_eq!(kind, z3_sys::ParamKind::Bool); + let doc = param_descrs.get_param_documentation("iDontExist"); + assert!(doc.is_none()); + let doc = param_descrs.get_param_documentation("model"); + assert_eq!(doc.unwrap(), "model generation for solvers, this parameter can be overwritten when creating a solver"); +} + +#[test] +fn test_param_descrs_from_tactic() { + let _ = env_logger::try_init(); + let cfg = Config::new(); + let ctx = Context::new(&cfg); + let t = Tactic::new(&ctx, "qfnra-nlsat"); + + let param_descrs = t.get_param_descrs(); + let kind = param_descrs.get_param_kind("lazy"); + assert_eq!(kind, z3_sys::ParamKind::UInt); +} + #[test] fn test_substitution() { let cfg = Config::new(); From 41e1b2089655f094f42ce655fc3882ccd3af95b9 Mon Sep 17 00:00:00 2001 From: AndesVL <32360382+AndesVL@users.noreply.github.com> Date: Sun, 5 Jun 2022 05:50:08 +0200 Subject: [PATCH 2/3] fixed documentation for Z3_param_descrs related functions --- z3-sys/src/lib.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/z3-sys/src/lib.rs b/z3-sys/src/lib.rs index d67b7e25..75f9e94f 100644 --- a/z3-sys/src/lib.rs +++ b/z3-sys/src/lib.rs @@ -1781,7 +1781,7 @@ extern "C" { /// Return the number of parameters in the given parameter description set. pub fn Z3_param_descrs_size(c: Z3_context, p: Z3_param_descrs) -> ::std::os::raw::c_uint; - /// Return the number of parameters in the given parameter description set. + /// Return the name of the parameter at given index `i`. /// /// # Preconditions: /// @@ -1793,6 +1793,10 @@ extern "C" { ) -> Z3_symbol; /// Retrieve documentation string corresponding to parameter name `s`. + /// + /// # Preconditions: + /// + /// - `s is a valid parameter name` pub fn Z3_param_descrs_get_documentation( c: Z3_context, p: Z3_param_descrs, From f3e4315f738d33fa7dbb0189762e273cfcf2a3e0 Mon Sep 17 00:00:00 2001 From: AndesVL <32360382+AndesVL@users.noreply.github.com> Date: Sun, 5 Jun 2022 12:57:47 +0200 Subject: [PATCH 3/3] added is_null checks to param_get_documentation and new_from_z3_symbol --- z3/src/param_descrs.rs | 6 +++++- z3/src/symbol.rs | 3 +++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/z3/src/param_descrs.rs b/z3/src/param_descrs.rs index 2ef3df9a..6730bd72 100644 --- a/z3/src/param_descrs.rs +++ b/z3/src/param_descrs.rs @@ -77,7 +77,11 @@ impl<'ctx> ParamDescrs<'ctx> { self.z3_param_descrs, n.into().as_z3_symbol(self.ctx), ); - CStr::from_ptr(d).to_str().ok() + if d.is_null() { + None + } else { + CStr::from_ptr(d).to_str().ok() + } } } } diff --git a/z3/src/symbol.rs b/z3/src/symbol.rs index 0fa8bfa4..7bc09088 100644 --- a/z3/src/symbol.rs +++ b/z3/src/symbol.rs @@ -29,6 +29,9 @@ impl Symbol { .map(|i| Symbol::Int(i)), SymbolKind::String => { let s = Z3_get_symbol_string(ctx.z3_ctx, z3_symbol); + if s.is_null() { + return None; + } CStr::from_ptr(s) .to_str() .ok()