z3-sys 0.13.0

Low-level bindings for the Z3 SMT solver from Microsoft Research
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123

use std::fs;
use std::path::Path;

/// A parsed Z3 version (major.minor.patch).
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Debug)]
pub(crate) struct Version {
    pub major: u32,
    pub minor: u32,
    pub patch: u32,
}

impl std::fmt::Display for Version {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{}.{}.{}", self.major, self.minor, self.patch)
    }
}

/// The minimum Z3 version z3-sys supports (Ubuntu 26.04's shipped Z3).
pub(crate) const MIN_SUPPORTED: Version = Version {
    major: 4,
    minor: 13,
    patch: 3,
};

/// Parses a dotted version string like `"4.13.3"` or `"4.13.3.0"`.
///
/// Extra trailing components (e.g. a build/tweak number) are ignored.
pub(crate) fn parse_dotted(s: &str) -> Option<Version> {
    let mut parts = s.trim().split('.');
    let major = parts.next()?.parse().ok()?;
    let minor = parts.next()?.parse().ok()?;
    let patch = parts.next().unwrap_or("0").parse().ok()?;
    Some(Version {
        major,
        minor,
        patch,
    })
}

/// Parses a Z3 version from a `z3_version.h` header, which defines
/// `Z3_MAJOR_VERSION`, `Z3_MINOR_VERSION`, and `Z3_BUILD_NUMBER` (the patch
/// component — Z3 does not call it `Z3_PATCH_VERSION`).
pub(crate) fn parse_header(path: &Path) -> Option<Version> {
    let contents = fs::read_to_string(path).ok()?;
    let major = find_macro_value(&contents, "Z3_MAJOR_VERSION")?;
    let minor = find_macro_value(&contents, "Z3_MINOR_VERSION")?;
    let patch = find_macro_value(&contents, "Z3_BUILD_NUMBER").unwrap_or(0);
    Some(Version {
        major,
        minor,
        patch,
    })
}

fn find_macro_value(contents: &str, name: &str) -> Option<u32> {
    for line in contents.lines() {
        let line = line.trim();
        let Some(rest) = line.strip_prefix("#define") else {
            continue;
        };
        let mut tokens = rest.split_whitespace();
        if tokens.next() == Some(name) {
            return tokens.next()?.parse().ok();
        }
    }
    None
}

/// Parses a version out of `z3 --version` output, e.g. `"Z3 version 4.13.3 -
/// 64 bit"`. Used as a fallback when no pkg-config metadata is available
/// (e.g. Z3 installed from a prebuilt release archive with no `.pc` file).
pub(crate) fn parse_cli_output(s: &str) -> Option<Version> {
    let after = s.split("version").nth(1)?;
    let token = after.split_whitespace().next()?;
    parse_dotted(token)
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn parses_dotted_versions() {
        assert_eq!(
            parse_dotted("4.13.3"),
            Some(Version {
                major: 4,
                minor: 13,
                patch: 3
            })
        );
        assert_eq!(
            parse_dotted("5.0"),
            Some(Version {
                major: 5,
                minor: 0,
                patch: 0
            })
        );
        assert_eq!(parse_dotted("not-a-version"), None);
    }

    #[test]
    fn parses_cli_output() {
        assert_eq!(
            parse_cli_output("Z3 version 4.13.3 - 64 bit"),
            Some(Version {
                major: 4,
                minor: 13,
                patch: 3
            })
        );
        assert_eq!(
            parse_cli_output("Z3 version 5.0.0"),
            Some(Version {
                major: 5,
                minor: 0,
                patch: 0
            })
        );
        assert_eq!(parse_cli_output("not z3 output"), None);
    }
}