Use system shipped z3

.github/workflows/rust.yml

@@ -20,11 +20,23 @@ jobs:
       run: cargo fmt -- --check
 
   build:
-    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        build: [linux, macos]
+        include:
+          - build: linux
+            os: ubuntu-latest
+          - build: macos
+            os: macos-latest
+    runs-on: ${{ matrix.os }}
     steps:
     - uses: actions/checkout@v3
     - name: Install Z3
+      if: matrix.os == 'ubuntu-latest'
       run: sudo apt-get install libz3-dev
+    - name: Install Z3
+      if: matrix.os == 'macos-latest'
+      run: brew install z3
     - name: Build
       run: cargo build -vv --all
       # XXX: Ubuntu's Z3 package seems to be missing some symbols, like

z3-sys/Cargo.toml

@@ -18,6 +18,7 @@ repository = "https://github.com/prove-rs/z3.rs.git"
 [build-dependencies]
 bindgen = { version = "0.66.0", default-features = false, features = ["runtime"] }
 cmake = { version = "0.1.49", optional = true }
+pkg-config = "0.3.27"
 
 [features]
 # Enable this feature to statically link our own build of Z3, rather than

z3-sys/build.rs

@@ -1,16 +1,38 @@
 use std::env;
+use std::path::PathBuf;
 
 const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER";
 
+#[cfg(feature = "static-link-z3")]
+fn build_static() -> Vec<PathBuf> {
+    if let Ok(lib) = pkg_config::Config::new().statik(true).probe("z3") {
+        lib.include_paths
+    } else {
+        // Oh, we don't have a shipped z3
+        vec![build_z3()]
+    }
+}
+
+#[cfg(not(feature = "static-link-z3"))]
+fn build_dynamic() -> Vec<PathBuf> {
+    if let Ok(lib) = pkg_config::Config::new().statik(false).probe("z3") {
+        lib.include_paths
+    } else {
+        // Nothing more to do, hope users have setup everything
+        vec![]
+    }
+}
+
 fn main() {
     #[cfg(feature = "static-link-z3")]
-    build_z3();
+    let includes = build_static();
+
+    #[cfg(not(feature = "static-link-z3"))]
+    let includes = build_dynamic();
 
     println!("cargo:rerun-if-changed=build.rs");
 
-    let header = if cfg!(feature = "static-link-z3") {
-        "z3/src/api/z3.h".to_string()
-    } else if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) {
+    let header = if let Ok(header_path) = std::env::var(Z3_HEADER_VAR) {
         header_path
     } else {
         "wrapper.h".to_string()
@@ -35,7 +57,8 @@ fn main() {
             .parse_callbacks(Box::new(bindgen::CargoCallbacks))
             .generate_comments(false)
             .rustified_enum(format!("Z3_{}", x))
-            .allowlist_type(format!("Z3_{}", x));
+            .allowlist_type(format!("Z3_{}", x))
+            .clang_args(includes.iter().map(|v| format!("-I{}", v.display())));
         if env::var("TARGET").unwrap() == "wasm32-unknown-emscripten" {
             enum_bindings = enum_bindings.clang_arg(format!(
                 "--sysroot={}/upstream/emscripten/cache/sysroot",
@@ -51,7 +74,7 @@ fn main() {
 }
 
 #[cfg(feature = "static-link-z3")]
-fn build_z3() {
+fn build_z3() -> PathBuf {
     let mut cfg = cmake::Config::new("z3");
     cfg
         // Don't build `libz3.so`, build `libz3.a` instead.
@@ -127,4 +150,6 @@ fn build_z3() {
     if let Some(cxx) = cxx {
         println!("cargo:rustc-link-lib={}", cxx);
     }
+
+    dst.join("include")
 }

z3/tests/lib.rs

@@ -1221,7 +1221,7 @@ fn test_tactic_fail() {
 
     let tactic = Tactic::new(&ctx, "fail");
     let apply_results = tactic.apply(&goal, Some(&params));
-    assert!(matches!(apply_results, Err(_)));
+    assert!(apply_results.is_err());
 }
 
 #[test]