added bindings for z3_param_descrs and related functions

z3-sys/src/lib.rs

@@ -1798,7 +1798,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:
     ///
@@ -1810,6 +1810,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,

z3/src/lib.rs

@@ -15,7 +15,7 @@ extern crate num;
 
 use std::ffi::CString;
 use z3_sys::*;
-pub use z3_sys::{AstKind, GoalPrec, SortKind};
+pub use z3_sys::{AstKind, GoalPrec, SortKind, SymbolKind};
 
 pub mod ast;
 mod config;
@@ -27,6 +27,7 @@ mod model;
 mod ops;
 mod optimize;
 mod params;
+mod param_descrs;
 mod pattern;
 mod probe;
 mod rec_func_decl;
@@ -245,6 +246,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 {

z3/src/param_descrs.rs

@@ -0,0 +1,115 @@
+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<N: Into<Symbol>>(&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<Symbol> {
+        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<N: Into<Symbol> + 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),
+            );
+            if d.is_null() {
+                None
+            } else {
+                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> {
+        <Self as fmt::Display>::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);
+        }
+    }
+}

z3/src/solver.rs

@@ -11,6 +11,8 @@ use Solver;
 use Statistics;
 use Symbol;
 
+use crate::ParamDescrs;
+
 impl<'ctx> Solver<'ctx> {
     pub(crate) unsafe fn wrap(ctx: &'ctx Context, z3_slv: Z3_solver) -> Solver<'ctx> {
         Z3_solver_inc_ref(ctx.z3_ctx, z3_slv);
@@ -279,6 +281,10 @@ impl<'ctx> Solver<'ctx> {
         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)
+    }
+
     /// Retrieve the statistics for the last [`Solver::check()`].
     pub fn get_statistics(&self) -> Statistics<'ctx> {
         unsafe {

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,29 @@ impl Symbol {
             }
         }
     }
+
+    pub fn new_from_z3_symbol(ctx: &Context, z3_symbol: Z3_symbol) -> Option<Symbol> {
+        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);
+                    if s.is_null() {
+                        return None;
+                    }
+                    CStr::from_ptr(s)
+                        .to_str()
+                        .ok()
+                        .map(|s| Symbol::String(s.to_owned()))
+                }
+            }
+        }
+    }
 }
 
 impl From<u32> for Symbol {
@@ -33,3 +59,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),
+        }
+    }
+}

z3/src/tactic.rs

@@ -15,6 +15,8 @@ use Probe;
 use Solver;
 use Tactic;
 
+use crate::ParamDescrs;
+
 impl<'ctx> ApplyResult<'ctx> {
     unsafe fn wrap(ctx: &'ctx Context, z3_apply_result: Z3_apply_result) -> ApplyResult<'ctx> {
         Z3_apply_result_inc_ref(ctx.z3_ctx, z3_apply_result);
@@ -242,6 +244,10 @@ impl<'ctx> Tactic<'ctx> {
             )
         }
     }
+
+    pub fn get_param_descrs(&'ctx self) -> ParamDescrs<'ctx> {
+        ParamDescrs::from_tactic(&self)
+    }
 }
 
 impl<'ctx> fmt::Display for Tactic<'ctx> {

z3/tests/lib.rs

@@ -321,6 +321,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();