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        // Windows uses "libz3", Unix uses "z3"
29        if cfg!(target_os = "windows") {
30            println!("cargo:rustc-link-lib=static=libz3");
31        } else {
32            println!("cargo:rustc-link-lib=static=z3");
33        }
34    }
35}
36
37/// Build Z3 from source and return the resulting artifacts.
38///
39/// Call this from your crate's `build.rs`.
40///
41/// Source resolution priority:
42/// 1. `Z3_SRC_SOURCE_DIR` environment variable
43/// 2. Bundled source at `$CARGO_MANIFEST_DIR/z3/` (the submodule)
44/// 3. Panics with a clear message
45pub fn build() -> Artifacts {
46    println!("cargo:rerun-if-env-changed={Z3_SRC_SOURCE_DIR}");
47
48    let src_dir = resolve_source();
49
50    let dst = build_cmake(&src_dir);
51
52    let lib_dir = find_lib_dir(&dst);
53
54    let include_dir = dst.join("include");
55
56    Artifacts {
57        include_dir,
58        lib_dir,
59    }
60}
61
62fn resolve_source() -> PathBuf {
63    if let Ok(dir) = env::var(Z3_SRC_SOURCE_DIR) {
64        let path = PathBuf::from(dir);
65        assert!(
66            path.exists(),
67            "{Z3_SRC_SOURCE_DIR} points to non-existent path: {}",
68            path.display()
69        );
70        return path;
71    }
72
73    // env!() bakes in z3-src's own manifest directory at z3-src compile time,
74    // so this works correctly even when called from another crate's build.rs.
75    let submodule = Path::new(env!("CARGO_MANIFEST_DIR")).join("z3");
76    if submodule.exists() {
77        return submodule;
78    }
79
80    // Note that this panic should only be reachable in dev contexts: the crate has the
81    // source tree from the submodule prepublished already, so the above "submodule" check
82    // should always work.
83    //
84    // If, however, someone is developing on this library and has it checked out through git,
85    // and did not check out submodules, this may be hit, hence the message.
86    panic!("Z3 source not found — run `git submodule update --init` or set {Z3_SRC_SOURCE_DIR}");
87}
88
89fn build_cmake(src_dir: &Path) -> PathBuf {
90    let mut cfg = cmake::Config::new(src_dir);
91
92    cfg.define("Z3_BUILD_LIBZ3_SHARED", "false")
93        .define("Z3_BUILD_EXECUTABLE", "false")
94        .define("Z3_BUILD_TEST_EXECUTABLES", "false")
95        .define("Z3_ENABLE_EXAMPLE_TARGETS", "false");
96
97    if cfg!(target_os = "windows") {
98        // -MP and -m enable parallel compilation, measurably faster for Z3.
99        cfg.cxxflag("-MP");
100        cfg.build_arg("-m");
101        cfg.cxxflag("-DWIN32");
102        cfg.cxxflag("-D_WINDOWS");
103        cfg.define("CMAKE_MSVC_RUNTIME_LIBRARY", "MultiThreadedDLL");
104    } else if env::var("TARGET").unwrap().starts_with("wasm") {
105        // Z3 uses exceptions, which must be explicitly enabled for WASM.
106        cfg.no_default_flags(true).cxxflag("-fexceptions");
107    }
108
109    cfg.build()
110}
111
112fn find_lib_dir(dst: &Path) -> PathBuf {
113    for candidate in &["lib", "lib64"] {
114        let dir = dst.join(candidate);
115        if dir.exists() {
116            if *candidate == "lib64" {
117                assert_eq!(
118                    env::var("CARGO_CFG_TARGET_POINTER_WIDTH").unwrap(),
119                    "64",
120                    "lib64 only valid for 64-bit targets"
121                );
122            }
123            return dir;
124        }
125    }
126    panic!(
127        "Could not find lib directory in Z3 build output at {}",
128        dst.display()
129    );
130}
z3_src/lib.rs

z3_src/
lib.rs
