Add vcpkg support and corresponding CI. (#251)

* Add basic support for vcpkg.

Use vcpkg-rs to manage z3 instead. A non-default feature vcpkg is added.

.github/workflows/rust.yml

@@ -94,6 +94,55 @@ jobs:
         run: cargo test -vv --features static-link-z3
       - name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled
         run: cargo test --manifest-path z3/Cargo.toml -vv --features 'static-link-z3 arbitrary-size-numeral'
+  build_with_vcpkg_installed_z3:
+    strategy:
+      matrix:
+        build: [windows] # [linux, macos, windows]
+        include:
+          # - build: linux
+          #   os: ubuntu-latest
+          #   vcpkg_triplet: x64-linux
+          # - build: macos
+          #   os: macos-latest
+          #   vcpkg_triplet: x64-osx
+          - build: windows
+            os: windows-latest
+            vcpkg_triplet: x64-windows-static-md
+    runs-on: ${{ matrix.os }}
+    env:
+      VCPKG_ROOT: ${{ github.workspace }}/vcpkg
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797
+        uses: KyleMayes/install-llvm-action@v1
+        if: matrix.os == 'windows-latest'
+        with:
+          version: "11.0"
+          directory: ${{ runner.temp }}/llvm
+      - name: Set LIBCLANG_PATH
+        run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV
+        if: matrix.os == 'windows-latest'
+      - run: echo  Instaling z3:${{ matrix.vcpkg_triplet }} on ${{ matrix.os }}.
+      - name: vcpkg build z3
+        uses: johnwason/vcpkg-action@v5
+        id: vcpkg
+        with:
+          pkgs: z3
+          triplet: ${{ matrix.vcpkg_triplet }}
+          cache-key: ${{ matrix.os }}
+          revision: master
+          token: ${{ github.token }}
+          extra-args: --clean-buildtrees-after-build
+      - name: Show default toolchain of rust.
+        run: rustup default
+      - name: Build `z3-sys` and `z3` with vcpkg installed Z3
+        run: cargo build -vv --features vcpkg
+      - name: Test `z3-sys` and `z3` with vcpkg installed Z3
+        run: cargo test -vv --features vcpkg
+      - name: Test `z3` with vcpkg installed Z3 and `arbitrary-size-numeral` enabled
+        run: cargo test --manifest-path z3/Cargo.toml -vv --features 'vcpkg arbitrary-size-numeral'
 
   run_clippy:
     runs-on: ubuntu-latest

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,13 +1,45 @@
 use std::env;
 
+#[cfg(not(feature = "vcpkg"))]
 const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER";
 
 fn main() {
+    // Feature `vcpkg` is prior to `static-link-z3` as vcpkg-installed z3 is also statically linked.
+
+    #[cfg(not(feature = "vcpkg"))]
     #[cfg(feature = "static-link-z3")]
-    build_z3();
+    build_bundled_z3();
 
     println!("cargo:rerun-if-changed=build.rs");
 
+    #[cfg(not(feature = "vcpkg"))]
+    let header = find_header_by_env();
+    #[cfg(feature = "vcpkg")]
+    let header = find_library_header_by_vcpkg();
+
+    generate_binding(&header);
+}
+
+#[cfg(feature = "vcpkg")]
+fn find_library_header_by_vcpkg() -> String {
+    let lib = vcpkg::Config::new()
+        .emit_includes(true)
+        .find_package("z3")
+        .unwrap();
+    for include in lib.include_paths.iter() {
+        let mut include = include.clone();
+        include.push("z3.h");
+        if include.exists() {
+            let header = include.to_str().unwrap().to_owned();
+            println!("cargo:rerun-if-changed={}", header);
+            return header;
+        }
+    }
+    panic!("z3.h is not found in include path of installed z3.");
+}
+
+#[cfg(not(feature = "vcpkg"))]
+fn find_header_by_env() -> String {
     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) {
@@ -17,6 +49,10 @@ fn main() {
     };
     println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR);
     println!("cargo:rerun-if-changed={}", header);
+    header
+}
+
+fn generate_binding(header: &str) {
     let out_path = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap());
 
     for x in &[
@@ -31,7 +67,7 @@ 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))
@@ -50,8 +86,10 @@ fn main() {
     }
 }
 
+/// Build z3 with bundled source codes.
+#[cfg(not(feature = "vcpkg"))]
 #[cfg(feature = "static-link-z3")]
-fn build_z3() {
+fn build_bundled_z3() {
     let mut cfg = cmake::Config::new("z3");
     cfg
         // Don't build `libz3.so`, build `libz3.a` instead.

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"