Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

added bindings for global params #199

Merged
merged 1 commit into from
Jul 25, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions z3/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@ mod sort;
mod symbol;
mod tactic;

pub use params::{get_global_param, set_global_param, reset_all_global_params};

// Z3 appears to be only mostly-threadsafe, a few initializers
// and such race; so we mutex-guard all access to the library.
lazy_static! {
Expand Down
31 changes: 30 additions & 1 deletion z3/src/params.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use std::ffi::CStr;
use std::ffi::{CStr, CString};
use std::fmt;
use z3_sys::*;
use Context;
Expand Down Expand Up @@ -68,6 +68,35 @@ impl<'ctx> Params<'ctx> {
}
}

/// Set a global (or module) parameter. This setting is shared by all Z3 contexts.
pub fn set_global_param(param_id: &str, param_value: &str) {
let param_id = CString::new(param_id).unwrap();
let param_value = CString::new(param_value).unwrap();
let _guard = Z3_MUTEX.lock().unwrap();
unsafe {
Z3_global_param_set(param_id.as_ptr(), param_value.as_ptr());
}
}

/// Get a global (or module) parameter.
pub fn get_global_param(param_id: &str) -> Option<String> {
let param_id = CString::new(param_id).unwrap();
let _guard = Z3_MUTEX.lock().unwrap();
let mut ptr = std::ptr::null();
if unsafe { Z3_global_param_get(param_id.as_ptr(), &mut ptr as *mut *const i8) } {
let s = unsafe { CStr::from_ptr(ptr) };
s.to_str().ok().map(|s| s.to_owned())
} else {
None
}
}

/// Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).
pub fn reset_all_global_params() {
let _guard = Z3_MUTEX.lock().unwrap();
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) };
Expand Down
17 changes: 17 additions & 0 deletions z3/tests/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -303,6 +303,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(":pp.decimal");
assert_eq!(val, Some("false".to_owned()));
set_global_param(":pp.decimal", "true");
let val = get_global_param(":pp.decimal");
assert_eq!(val, Some("true".to_owned()));
reset_all_global_params();
let val = get_global_param(":pp.decimal");
assert_eq!(val, Some("false".to_owned()));
}

#[test]
fn test_substitution() {
let cfg = Config::new();
Expand Down