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

z3_src/
lib.rs
