synth-verify 0.11.21

Z3 SMT translation validation for the Synth compiler
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

[package]
name = "synth-verify"
version.workspace = true
edition.workspace = true
authors.workspace = true
license.workspace = true
repository.workspace = true
homepage.workspace = true
keywords.workspace = true
categories.workspace = true
description = "Z3 SMT translation validation for the Synth compiler"

[features]
default = ["z3-solver", "arm"]
z3-solver = ["z3"]
arm = ["synth-synthesis"]

[dependencies]
# Core dependencies (always required)
synth-core = { path = "../synth-core", version = "0.11.21" }
synth-cfg = { path = "../synth-cfg", version = "0.11.21" }
synth-opt = { path = "../synth-opt", version = "0.11.21" }

# ARM synthesis (optional, behind 'arm' feature)
synth-synthesis = { path = "../synth-synthesis", version = "0.11.21", optional = true }

# SMT solver for formal verification
z3 = { version = "0.19", features = ["static-link-z3"], optional = true }

# Error handling
anyhow.workspace = true
thiserror.workspace = true

# Serialization for test cases
serde.workspace = true
serde_json.workspace = true

# Property-based testing
proptest.workspace = true

# For examples and reporting
chrono = "0.4"

[dev-dependencies]
criterion = "0.5"

[[example]]
name = "verification_report"
required-features = ["z3-solver", "arm"]