z3_src/
lib.rs

1use std::{
2    env,
3    path::{Path, PathBuf},
4};
5
6const Z3_SRC_SOURCE_DIR: &str = "Z3_SRC_SOURCE_DIR";
7
8/// Build artifacts produced by compiling Z3 from source.
9pub struct Artifacts {
10    include_dir: PathBuf,
11    lib_dir: PathBuf,
12}
13
14impl Artifacts {
15    /// Path to the directory containing `z3.h`.
16    pub fn include_dir(&self) -> &Path {
17        &self.include_dir
18    }
19
20    /// Path to the directory containing the static Z3 library.
21    pub fn lib_dir(&self) -> &Path {
22        &self.lib_dir
23    }
24
25    /// Emit `cargo:rustc-link-*` directives. Call this from your `build.rs`.
26    pub fn print_cargo_metadata(&self) {
27        println!("cargo:rustc-link-search=native={}", self.lib_dir.display());
28        // MSVC produces `libz3-static.lib` (Z3 >= 5.3.2, so it doesn't collide
29        // with the shared build's import library) or `libz3.lib` (older Z3,
30        // e.g. via `Z3_SRC_SOURCE_DIR`). MinGW (including the `gnullvm` Rust
31        // target) follows the Unix archive naming convention and produces
32        // `libz3.a`, which must be requested as `z3` rather than `libz3`.
33        if env::var("CARGO_CFG_TARGET_ENV").as_deref() == Ok("msvc") {
34            if self.lib_dir.join("libz3-static.lib").exists() {
35                println!("cargo:rustc-link-lib=static=libz3-static");
36            } else {
37                println!("cargo:rustc-link-lib=static=libz3");
38            }
39        } else {
40            println!("cargo:rustc-link-lib=static=z3");
41        }
42    }
43}
44
45/// Build Z3 from source and return the resulting artifacts.
46///
47/// Call this from your crate's `build.rs`.
48///
49/// Source resolution priority:
50/// 1. `Z3_SRC_SOURCE_DIR` environment variable
51/// 2. Bundled source at `$CARGO_MANIFEST_DIR/z3/` (the submodule)
52/// 3. Panics with a clear message
53pub fn build() -> Artifacts {
54    println!("cargo:rerun-if-env-changed={Z3_SRC_SOURCE_DIR}");
55
56    let src_dir = resolve_source();
57
58    let dst = build_cmake(&src_dir);
59
60    let lib_dir = find_lib_dir(&dst);
61
62    let include_dir = dst.join("include");
63
64    Artifacts {
65        include_dir,
66        lib_dir,
67    }
68}
69
70fn resolve_source() -> PathBuf {
71    if let Ok(dir) = env::var(Z3_SRC_SOURCE_DIR) {
72        let path = PathBuf::from(dir);
73        assert!(
74            path.exists(),
75            "{Z3_SRC_SOURCE_DIR} points to non-existent path: {}",
76            path.display()
77        );
78        return path;
79    }
80
81    // env!() bakes in z3-src's own manifest directory at z3-src compile time,
82    // so this works correctly even when called from another crate's build.rs.
83    let submodule = Path::new(env!("CARGO_MANIFEST_DIR")).join("z3");
84    if submodule.exists() {
85        return submodule;
86    }
87
88    // Note that this panic should only be reachable in dev contexts: the crate has the
89    // source tree from the submodule prepublished already, so the above "submodule" check
90    // should always work.
91    //
92    // If, however, someone is developing on this library and has it checked out through git,
93    // and did not check out submodules, this may be hit, hence the message.
94    panic!("Z3 source not found — run `git submodule update --init` or set {Z3_SRC_SOURCE_DIR}");
95}
96
97fn build_cmake(src_dir: &Path) -> PathBuf {
98    let mut cfg = cmake::Config::new(src_dir);
99
100    cfg.define("Z3_BUILD_LIBZ3_SHARED", "false")
101        .define("Z3_BUILD_EXECUTABLE", "false")
102        .define("Z3_BUILD_TEST_EXECUTABLES", "false")
103        .define("Z3_ENABLE_EXAMPLE_TARGETS", "false");
104
105    // The cmake crate does not forward CMAKE_*_COMPILER_LAUNCHER env vars
106    // automatically; pass them explicitly so sccache/ccache can wrap the compiler.
107    for var in &["CMAKE_C_COMPILER_LAUNCHER", "CMAKE_CXX_COMPILER_LAUNCHER"] {
108        if let Ok(val) = env::var(var) {
109            cfg.define(var, val);
110        }
111    }
112
113    if env::var("CARGO_CFG_TARGET_OS").as_deref() == Ok("windows") {
114        cfg.cxxflag("-DWIN32");
115        cfg.cxxflag("-D_WINDOWS");
116
117        // These options are specific to Microsoft's compiler and runtime.
118        // Windows GNU targets are compiled by GCC-compatible clang when using
119        // cargo-zigbuild.
120        if env::var("CARGO_CFG_TARGET_ENV").as_deref() == Ok("msvc") {
121            // -MP enables parallel MSVC compilation, but conflicts with compiler launchers
122            // like sccache which handle parallelism per-invocation and cannot cache -MP mode.
123            if env::var("CMAKE_CXX_COMPILER_LAUNCHER").is_err() {
124                cfg.cxxflag("-MP");
125                cfg.build_arg("-m");
126            }
127
128            let target_features = env::var("CARGO_CFG_TARGET_FEATURE").unwrap_or_default();
129            let runtime = if target_features.split(',').any(|f| f.trim() == "crt-static") {
130                "MultiThreaded"
131            } else {
132                "MultiThreadedDLL"
133            };
134            cfg.define("CMAKE_MSVC_RUNTIME_LIBRARY", runtime);
135        }
136    } else if env::var("TARGET").unwrap().starts_with("wasm") {
137        // Z3 uses exceptions, which must be explicitly enabled for WASM.
138        cfg.no_default_flags(true).cxxflag("-fexceptions");
139    }
140
141    cfg.build()
142}
143
144fn find_lib_dir(dst: &Path) -> PathBuf {
145    for candidate in &["lib", "lib64"] {
146        let dir = dst.join(candidate);
147        if dir.exists() {
148            if *candidate == "lib64" {
149                assert_eq!(
150                    env::var("CARGO_CFG_TARGET_POINTER_WIDTH").unwrap(),
151                    "64",
152                    "lib64 only valid for 64-bit targets"
153                );
154            }
155            return dir;
156        }
157    }
158    panic!(
159        "Could not find lib directory in Z3 build output at {}",
160        dst.display()
161    );
162}
z3_src/lib.rs

z3_src/
lib.rs
