Add vcpkg support and corresponding CI.

z3-sys/Cargo.toml

@@ -18,8 +18,10 @@ 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 }
+vcpkg = { version = "0.2.15", optional = true }
 
 [features]
 # Enable this feature to statically link our own build of Z3, rather than
 # dynamically linking to the system's `libz3.so`.
 static-link-z3 = ["cmake"]
+vcpkg = ["dep:vcpkg"]

z3-sys/build.rs

@@ -1,7 +1,9 @@
 use std::env;
 
+#[cfg(not(feature = "vcpkg"))]
 const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER";
 
+#[cfg(not(feature = "vcpkg"))]
 fn main() {
     #[cfg(feature = "static-link-z3")]
     build_z3();
@@ -17,6 +19,33 @@ fn main() {
     };
     println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR);
     println!("cargo:rerun-if-changed={}", header);
+
+    generate_binding(&header);
+}
+
+#[cfg(feature = "vcpkg")]
+fn main() {
+    let lib = vcpkg::Config::new()
+        .emit_includes(true)
+        .find_package("z3")
+        .unwrap();
+    let found_header = lib.include_paths.iter().any(|include| {
+        let mut include = include.clone();
+        include.push("z3.h");
+        if include.exists() {
+            generate_binding(include.to_str().unwrap());
+            true
+        } else {
+            false
+        }
+    });
+    assert!(
+        found_header,
+        "z3.h is not found in include path of installed z3."
+    );
+}
+
+fn generate_binding(header: &str) {
     let out_path = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap());
 
     for x in &[
@@ -31,16 +60,26 @@ fn main() {
         "symbol_kind",
     ] {
         let mut enum_bindings = bindgen::Builder::default()
-            .header(&header)
+            .header(header)
             .parse_callbacks(Box::new(bindgen::CargoCallbacks))
             .generate_comments(false)
             .rustified_enum(format!("Z3_{}", x))
             .allowlist_type(format!("Z3_{}", x));
-        if env::var("TARGET").unwrap() == "wasm32-unknown-emscripten" {
-            enum_bindings = enum_bindings.clang_arg(format!(
-                "--sysroot={}/upstream/emscripten/cache/sysroot",
-                env::var("EMSDK").expect("$EMSDK env var missing. Is emscripten installed?")
-            ));
+        let target = env::var("TARGET").unwrap();
+        let wasm32 = target.starts_with("wasm32-unknown");
+        let wasm32_emscripten = target == "wasm32-unknown-emscripten";
+        if wasm32 {
+            let sysroot = env::var("EMSDK")
+                .map(|emsdk| format!("{}/upstream/emscripten/cache/sysroot", emsdk))
+                .or_else(|_err| {
+                    env::var("EMSCRIPTEN_ROOT")
+                        .map(|emscripten_root| format!("{}/cache/sysroot", emscripten_root))
+                });
+            if let Ok(sysroot) = sysroot {
+                enum_bindings = enum_bindings.clang_arg(format!("--sysroot={}", sysroot));
+            } else if wasm32_emscripten {
+                panic!("$EMSDK and $EMSCRIPTEN_ROOT env var missing. Is emscripten installed?");
+            }
         }
         enum_bindings
             .generate()

z3/Cargo.toml

@@ -21,6 +21,8 @@ arbitrary-size-numeral = ["num"]
 # dynamically linking to the system's `libz3.so`.
 static-link-z3 = ["z3-sys/static-link-z3"]
 
+vcpkg = ["z3-sys/vcpkg"]
+
 [dependencies]
 log = "0.4"
 

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]