smtkit 0.1.1

Facade crate for SMT constraint IR + SMT-LIB backends
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

[package]
name = "smtkit"
version = "0.1.1"
edition = "2021"
license = "MIT OR Apache-2.0"
description = "Facade crate for SMT constraint IR + SMT-LIB backends"
repository = "https://github.com/arclabs561/smtkit"
homepage = "https://github.com/arclabs561/smtkit"
documentation = "https://docs.rs/smtkit"
readme = "README.md"
publish = true
keywords = ["smt", "smtlib", "z3", "solver", "formal-methods"]

[workspace]
resolver = "2"
members = [
  "crates/smtkit-core",
  "crates/smtkit-smtlib",
  "crates/smtkit-z3",
  "crates/smtkit-ci",
]

[workspace.dependencies]
anyhow = "1"
clap = "4"
serde_json = "1.0"

[dependencies]
anyhow = "1"
thiserror = "2"
smtkit-core = { version = "0.1.0", path = "crates/smtkit-core" }
smtkit-smtlib = { version = "0.1.0", path = "crates/smtkit-smtlib" }
smtkit-z3 = { version = "0.1.0", path = "crates/smtkit-z3", optional = true }

[features]
# No solver integration by default: pure SMT-LIB2 script generation.
default = []
# Enable running Z3 via an external `z3` binary.
z3-bin = ["smtkit-smtlib/z3-bin"]
## In-process Z3 backend (Rust bindings).
z3-inproc = ["dep:smtkit-z3"]
# Build Z3 from source as part of `cargo build` (no external solver needed).
z3-inproc-bundled = ["z3-inproc", "smtkit-z3/bundled"]
# Fetch a prebuilt Z3 from GitHub releases at build time (network).
z3-inproc-gh-release = ["z3-inproc", "smtkit-z3/gh-release"]
# Convenience: enable an in-process Z3 that does not depend on a system `z3` binary.
# (This uses `gh-release`, which requires network access during build.)
z3-auto = ["z3-inproc-gh-release"]