From d836f05b363c85597242c5403e0650b719b815c7 Mon Sep 17 00:00:00 2001
From: Hennadii Chernyshchyk <genaloner@gmail.com>
Date: Thu, 13 Jul 2023 10:24:54 +0300
Subject: [PATCH] Add bindings for global params

---
 z3/src/context.rs | 23 +++++++++++++++++++++++
 z3/src/lib.rs     |  1 +
 z3/src/params.rs  | 41 ++++++++++++++++++++++++++++++++++++++++-
 z3/tests/lib.rs   | 17 +++++++++++++++++
 4 files changed, 81 insertions(+), 1 deletion(-)

diff --git a/z3/src/context.rs b/z3/src/context.rs
index ca65247b..8e736923 100644
--- a/z3/src/context.rs
+++ b/z3/src/context.rs
@@ -1,3 +1,4 @@
+use std::ffi::CString;
 use z3_sys::*;
 use Config;
 use Context;
@@ -29,6 +30,28 @@ impl Context {
     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> {
diff --git a/z3/src/lib.rs b/z3/src/lib.rs
index e50c94ec..11056155 100644
--- a/z3/src/lib.rs
+++ b/z3/src/lib.rs
@@ -38,6 +38,7 @@ mod statistics;
 mod symbol;
 mod tactic;
 
+pub use params::{get_global_param, reset_all_global_params, set_global_param};
 pub use statistics::{StatisticsEntry, StatisticsValue};
 
 /// Configuration used to initialize [logical contexts](Context).
diff --git a/z3/src/params.rs b/z3/src/params.rs
index e0d6f4c0..f100119a 100644
--- a/z3/src/params.rs
+++ b/z3/src/params.rs
@@ -1,4 +1,4 @@
-use std::ffi::CStr;
+use std::ffi::{CStr, CString};
 use std::fmt;
 use z3_sys::*;
 use Context;
@@ -60,6 +60,45 @@ impl<'ctx> Params<'ctx> {
     }
 }
 
+/// Get a global (or module) parameter.
+///
+/// # See also
+///
+/// - [`set_global_param()`]
+/// - [`reset_all_global_params()`]
+pub fn get_global_param(k: &str) -> Option<String> {
+    let ks = CString::new(k).unwrap();
+    let mut ptr = std::ptr::null();
+    if unsafe { Z3_global_param_get(ks.as_ptr(), &mut ptr as *mut *const i8) } {
+        let vs = unsafe { CStr::from_ptr(ptr) };
+        vs.to_str().ok().map(|vs| vs.to_owned())
+    } else {
+        None
+    }
+}
+
+/// Set a global (or module) parameter. This setting is shared by all Z3 contexts.
+///
+/// # See also
+///
+/// - [`get_global_param()`]
+/// - [`reset_all_global_params()`]
+pub fn set_global_param(k: &str, v: &str) {
+    let ks = CString::new(k).unwrap();
+    let vs = CString::new(v).unwrap();
+    unsafe { Z3_global_param_set(ks.as_ptr(), vs.as_ptr()) };
+}
+
+/// Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).
+///
+/// # See also
+///
+/// - [`get_global_param()`]
+/// - [`set_global_param()`]
+pub fn reset_all_global_params() {
+    unsafe { Z3_global_param_reset_all() };
+}
+
 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) };
diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs
index d2015473..127c73c6 100644
--- a/z3/tests/lib.rs
+++ b/z3/tests/lib.rs
@@ -367,6 +367,23 @@ fn test_params() {
     assert_eq!(solver.check(), SatResult::Sat);
 }
 
+#[test]
+fn test_global_params() {
+    let _ = env_logger::try_init();
+    // could interfere with other tests if they use global params
+    reset_all_global_params();
+    let val = get_global_param("iDontExist");
+    assert_eq!(val, None);
+    let val = get_global_param("verbose");
+    assert_eq!(val, Some("0".into()));
+    set_global_param("verbose", "1");
+    let val = get_global_param("verbose");
+    assert_eq!(val, Some("1".into()));
+    reset_all_global_params();
+    let val = get_global_param("verbose");
+    assert_eq!(val, Some("0".into()));
+}
+
 #[test]
 fn test_substitution() {
     let cfg = Config::new();