Use precompiled z3 libs by default

.github/workflows/rust.yml

@@ -8,31 +8,50 @@ on:
 
 env:
   CARGO_INCREMENTAL: 0
-  RUSTFLAGS: "-D warnings"
+  Z3_RELEASE: 'z3-4.8.12'
+  RUST_BACKTRACE: 'full'
 
 jobs:
   build:
-    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        os: [ubuntu-latest, windows-latest]
+        link: [default, static, system]
+    runs-on: ${{ matrix.os }}
     steps:
-    - uses: actions/checkout@v2
-    - name: Install Z3
-      run: sudo apt-get install libz3-dev
-    - name: Build
-      run: cargo build -vv --all
-      # XXX: Ubuntu's Z3 package seems to be missing some symbols, like
-      # `Z3_mk_pbeq`, leading to linker errors. Just ignore this, I guess, until
-      # we figure out how to work around it. At least we have the
-      # statically-linked Z3 tests below...
-      if: ${{ success() || failure() }}
-    - name: Run tests
-      run: cargo test -vv --all
-      # See above.
-      if: ${{ success() || failure() }}
-    - name: Run tests with `arbitrary-size-numeral` enabled
-      run: cargo test --manifest-path z3/Cargo.toml -vv --features arbitrary-size-numeral
-      # See above.
-      if: ${{ success() || failure() }}
+    - name: Checkout
+      uses: actions/checkout@v2
+      if: ${{ matrix.link != 'static' }}
+
+    - name: Checkout with submodules
+      uses: actions/checkout@v2
+      if: ${{ matrix.link == 'static' }}
+      with:
+        submodules: recursive
+
+    - name: Uninstall Z3 on Linux for non-system builds
+      if: ${{ matrix.os == 'ubuntu-latest' && matrix.link != 'system' }}
+      run: sudo apt-get remove libz3-dev
 
+    - name: Install Z3 on Windows for system builds
+      if: ${{ matrix.os == 'windows-latest' && matrix.link == 'system' }}
+      run: |
+        curl.exe -L "https://github.com/Z3Prover/z3/releases/download/${env:Z3_RELEASE}/${env:Z3_RELEASE}-x64-win.zip" -o "./${env:Z3_RELEASE}-x64-win.zip"
+        tar -xf "./${env:Z3_RELEASE}-x64-win.zip"
+        echo "${PWD}\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_PATH
+        echo "LIB=${PWD}\${env:Z3_RELEASE}-x64-win\bin" >> $env:GITHUB_ENV
+
+    - name: Test with Z3 releases
+      if: ${{ matrix.link  == 'default' }}
+      run: cargo test --lib -vv
+
+    - name: Test with Z3 system installation
+      if: ${{ matrix.link == 'system' }}
+      run: cargo test --lib -vv --features dynamic-link-z3
+
+    - name: Test with static Z3 builds
+      if: ${{ matrix.link  == 'static' }}
+      run: cargo test --lib -vv --features static-link-z3
   build_on_wasm:
     runs-on: ubuntu-latest
     steps:
@@ -64,36 +83,3 @@ jobs:
       run: |
         source ~/emsdk/emsdk_env.sh
         cargo build --target=wasm32-unknown-emscripten --manifest-path z3/Cargo.toml -vv --features static-link-z3
-  build_z3_statically:
-    strategy:
-      matrix:
-        build: [linux, macos, windows]
-        include:
-          - build: linux
-            os: ubuntu-latest
-          - build: macos
-            os: macos-latest
-          - build: windows
-            os: windows-latest
-    runs-on: ${{ matrix.os }}
-    steps:
-      - uses: actions/checkout@v2
-        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'
-      - name: Build z3-sys with statically linked Z3
-        run: cargo build --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3
-      - name: Build z3 with statically linked Z3
-        run: cargo build --manifest-path z3/Cargo.toml -vv --features static-link-z3
-      - name: Test `z3` with statically linked Z3
-        run: cargo test --manifest-path z3/Cargo.toml -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'

z3-sys/Cargo.toml

@@ -16,10 +16,10 @@ homepage = "https://github.com/prove-rs/z3.rs"
 repository = "https://github.com/prove-rs/z3.rs.git"
 
 [build-dependencies]
-bindgen = { version = "0.64.0", default-features = false, features = ["runtime"] }
+bindgen = { version = "0.64.0", default-features = false, features = ["runtime"], optional = true }
 cmake = { version = "0.1.49", 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"]
+static-link-z3 = ["cmake"] # Locally build and statically link a fresh Z3 build.
+use-bindgen = ["bindgen"] # Generate fresh bindings with bindgen.
+dynamic-link-z3 = [] # Dynamically link the system's Z3 installation.

z3-sys/build.rs

@@ -1,57 +1,78 @@
-use std::env;
-
+#[cfg(feature = "use-bindgen")]
 const Z3_HEADER_VAR: &str = "Z3_SYS_Z3_HEADER";
 
-fn main() {
-    #[cfg(feature = "static-link-z3")]
-    build_z3();
+#[cfg(not(feature = "dynamic-link-z3"))]
+#[cfg(not(feature = "static-link-z3"))]
+const Z3_RELEASE: &str = "z3-4.8.12";
 
+#[cfg(target_os = "windows")]
+const Z3_ARCH: &str = "x64-win";
+#[cfg(target_os = "linux")]
+const Z3_ARCH: &str = "x64-glibc-2.31";
+
+fn main() {
     println!("cargo:rerun-if-changed=build.rs");
+    get_z3();
+    #[cfg(feature = "use-bindgen")]
+    bindgen();
+}
 
-    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) {
-        header_path
-    } else {
-        "wrapper.h".to_string()
-    };
-    println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR);
-    println!("cargo:rerun-if-changed={}", header);
-    let out_path = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap());
+#[cfg(not(feature = "dynamic-link-z3"))]
+#[cfg(not(feature = "static-link-z3"))]
+/// Use precompiled Z3 binaries.
+fn get_z3() {
+    let out_dir = std::path::PathBuf::from(std::env::var("OUT_DIR").unwrap());
+    let archive_filename = format!("{}-{}", Z3_RELEASE, Z3_ARCH);
+    let archive_url = format!("https://github.com/Z3Prover/z3/releases/download/{}/{}.zip", Z3_RELEASE, archive_filename);
+    let archive_path = out_dir.join(format!("{}.zip", archive_filename));
+    let release_folder = out_dir.join(archive_filename);
 
-    for x in &[
-        "ast_kind",
-        "ast_print_mode",
-        "decl_kind",
-        "error_code",
-        "goal_prec",
-        "param_kind",
-        "parameter_kind",
-        "sort_kind",
-        "symbol_kind",
-    ] {
-        let mut enum_bindings = bindgen::Builder::default()
-            .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?")
-            ));
-        }
-        enum_bindings
-            .generate()
-            .expect("Unable to generate bindings")
-            .write_to_file(out_path.join(format!("{}.rs", x)))
-            .expect("Couldn't write bindings!");
-    }
+    let curl = std::process::Command::new("curl")
+        .arg("-L")
+        .arg("-o")
+        .arg(&archive_path.to_str().unwrap())
+        .arg(&archive_url)
+        .spawn()
+        .unwrap()
+        .wait()
+        .unwrap();
+    assert!(curl.success());
+
+    #[cfg(target_os = "windows")]
+    let tar = std::process::Command::new("tar")
+        .current_dir(archive_path.parent().unwrap())
+        .arg("-x")
+        .arg("-f")
+        .arg(&archive_path.to_str().unwrap())
+        .spawn()
+        .unwrap()
+        .wait()
+        .unwrap();
+
+    #[cfg(not(target_os = "windows"))]
+    let tar = std::process::Command::new("unzip")
+        .current_dir(archive_path.parent().unwrap())
+        .arg(&archive_path.to_str().unwrap())
+        .spawn()
+        .unwrap()
+        .wait()
+        .unwrap();
+    assert!(tar.success());
+
+    // Add lib folder to the library search path.
+    println!("cargo:rustc-link-search=native={}/bin", &release_folder.to_str().unwrap());
 }
 
+#[cfg(feature = "dynamic-link-z3")]
+#[cfg(not(feature = "static-link-z3"))]
+/// Use the system's Z3 installation.
+fn get_z3() {}
+
+#[cfg(not(feature = "dynamic-link-z3"))]
 #[cfg(feature = "static-link-z3")]
-fn build_z3() {
+#[cfg(not(target_os = "windows"))]
+/// Build and link Z3 statically on Linux/MacOS
+fn get_z3() {
     let mut cfg = cmake::Config::new("z3");
     cfg
         // Don't build `libz3.so`, build `libz3.a` instead.
@@ -61,16 +82,6 @@ fn build_z3() {
         // Don't build the tests.
         .define("Z3_BUILD_TEST_EXECUTABLES", "false");
 
-    if cfg!(target_os = "windows") {
-        // The compiler option -MP and the msbuild option -m
-        // can sometimes make builds slower but is measurably
-        // faster building Z3 with many cores.
-        cfg.cxxflag("-MP");
-        cfg.build_arg("-m");
-        cfg.cxxflag("-DWIN32");
-        cfg.cxxflag("-D_WINDOWS");
-    }
-
     let dst = cfg.build();
 
     // Z3 needs a C++ standard library. Customize which one we use with the
@@ -119,13 +130,80 @@ fn build_z3() {
         "Should have found the lib directory for our built Z3"
     );
 
-    if cfg!(target_os = "windows") {
-        println!("cargo:rustc-link-lib=static=libz3");
-    } else {
-        println!("cargo:rustc-link-lib=static=z3");
-    }
-
     if let Some(cxx) = cxx {
         println!("cargo:rustc-link-lib={}", cxx);
     }
 }
+
+#[cfg(not(feature = "dynamic-link-z3"))]
+#[cfg(feature = "static-link-z3")]
+#[cfg(target_os = "windows")]
+/// Build and link Z3 statically on Windows
+fn get_z3() {
+    let mut cfg = cmake::Config::new("z3");
+    cfg
+        // Don't build `libz3.so`, build `libz3.a` instead.
+        .define("Z3_BUILD_LIBZ3_SHARED", "false")
+        // Don't build the Z3 repl.
+        .define("Z3_BUILD_EXECUTABLE", "false")
+        // Don't build the tests.
+        .define("Z3_BUILD_TEST_EXECUTABLES", "false");
+        // The compiler option -MP and the msbuild option -m
+        // can sometimes make builds slower but is measurably
+        // faster building Z3 with many cores.
+        cfg.cxxflag("-MP");
+        cfg.build_arg("-m");
+        cfg.cxxflag("-DWIN32");
+        cfg.cxxflag("-D_WINDOWS");
+
+    let dst = cfg.build();
+
+    // Add lib folder to the library search path.
+    println!("cargo:rustc-link-search=native={}/lib", dst.to_str().unwrap());
+}
+
+#[cfg(feature = "use-bindgen")]
+fn bindgen() {
+    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) {
+        header_path
+    } else {
+        "wrapper.h".to_string()
+    };
+    println!("cargo:rerun-if-env-changed={}", Z3_HEADER_VAR);
+    println!("cargo:rerun-if-changed={}", header);
+    let out_path = std::path::PathBuf::from("generated".unwrap());
+
+    for x in &[
+        "ast_kind",
+        "ast_print_mode",
+        "decl_kind",
+        "error_code",
+        "goal_prec",
+        "param_kind",
+        "parameter_kind",
+        "sort_kind",
+        "symbol_kind",
+    ] {
+        let enum_bindings = bindgen::Builder::default()
+            .header(&header)
+            .parse_callbacks(Box::new(bindgen::CargoCallbacks))
+            .generate_comments(false)
+            .rustified_enum(format!("Z3_{}", x))
+            .allowlist_type(format!("Z3_{}", x))
+            .generate()
+            .expect("Unable to generate bindings");
+
+        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?")
+            ));
+        }
+
+        enum_bindings
+            .write_to_file(out_path.join(format!("{}.rs", x)))
+            .expect("Couldn't write bindings!");
+    }
+}

z3-sys/src/generated.rs

@@ -7,7 +7,7 @@ macro_rules! declare_generated_mods {
             // code.
             #[allow(dead_code)]
             mod $mod_name {
-                include!(concat!(env!("OUT_DIR"), "/", stringify!($mod_name), ".rs"));
+                include!(concat!("generated", "/", stringify!($mod_name), ".rs"));
             }
         )*
     };

z3-sys/src/generated/ast_kind.rs

@@ -0,0 +1,13 @@
+/* automatically generated by rust-bindgen 0.59.2 */
+
+#[repr(u32)]
+#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
+pub enum Z3_ast_kind {
+    Z3_NUMERAL_AST = 0,
+    Z3_APP_AST = 1,
+    Z3_VAR_AST = 2,
+    Z3_QUANTIFIER_AST = 3,
+    Z3_SORT_AST = 4,
+    Z3_FUNC_DECL_AST = 5,
+    Z3_UNKNOWN_AST = 1000,
+}

z3-sys/src/generated/ast_print_mode.rs

@@ -0,0 +1,9 @@
+/* automatically generated by rust-bindgen 0.59.2 */
+
+#[repr(u32)]
+#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq)]
+pub enum Z3_ast_print_mode {
+    Z3_PRINT_SMTLIB_FULL = 0,
+    Z3_PRINT_LOW_LEVEL = 1,
+    Z3_PRINT_SMTLIB2_COMPLIANT = 2,
+}