Expose Z3_get_version in the high-level interface

z3/src/lib.rs

@@ -30,9 +30,11 @@ mod sort;
 mod statistics;
 mod symbol;
 mod tactic;
+mod version;
 
 pub use crate::params::{get_global_param, reset_all_global_params, set_global_param};
 pub use crate::statistics::{StatisticsEntry, StatisticsValue};
+pub use crate::version::{full_version, version, Version};
 
 /// Configuration used to initialize [logical contexts](Context).
 ///

z3/src/version.rs

@@ -0,0 +1,29 @@
+use std::ffi::CStr;
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)]
+pub struct Version {
+    major: u32,
+    minor: u32,
+    build_number: u32,
+    revision_number: u32,
+}
+
+pub fn version() -> Version {
+    let mut ver = Version::default();
+    unsafe {
+        z3_sys::Z3_get_version(
+            &mut ver.major,
+            &mut ver.minor,
+            &mut ver.build_number,
+            &mut ver.revision_number,
+        );
+    }
+    ver
+}
+
+pub fn full_version() -> &'static str {
+    let ver_ptr = unsafe { z3_sys::Z3_get_full_version() };
+    let ver = unsafe { CStr::from_ptr(ver_ptr) };
+    ver.to_str()
+        .expect("Z3_get_full_version returned non-UTF-8 characters")
+}

z3/tests/lib.rs

@@ -1797,3 +1797,9 @@ fn iterate_all_solutions() {
             .collect()
     );
 }
+
+#[test]
+fn get_version() {
+    println!("Z3 version: {:?}", z3::version());
+    println!("Z3 full version string: {}", z3::full_version());
+}