[package]
edition = "2024"
name = "oxiz-proof"
version = "0.2.0"
authors = ["COOLJAPAN OU (Team KitaSan)"]
build = false
autolib = false
autobins = false
autoexamples = false
autotests = false
autobenches = false
description = "Proof generation and checking for OxiZ SMT solver"
readme = "README.md"
keywords = [
"smt",
"proof",
"drat",
"alethe",
"verification",
]
categories = [
"algorithms",
"development-tools::testing",
]
license = "Apache-2.0"
repository = "https://github.com/cool-japan/oxiz"
resolver = "2"
[features]
default = []
sat-integration = ["oxiz-sat"]
serde = [
"dep:serde",
"smallvec/serde",
]
[lib]
name = "oxiz_proof"
path = "src/lib.rs"
[[bench]]
name = "proof_benchmarks"
path = "benches/proof_benchmarks.rs"
harness = false
[dependencies.num-bigint]
version = "0.4"
features = ["std"]
default-features = false
[dependencies.num-rational]
version = "0.4"
features = ["std"]
default-features = false
[dependencies.num-traits]
version = "0.2"
features = ["std"]
default-features = false
[dependencies.oxiz-core]
version = "0.2.0"
features = ["std"]
default-features = false
[dependencies.oxiz-sat]
version = "0.2.0"
features = ["std"]
optional = true
default-features = false
[dependencies.regex]
version = "1.12"
[dependencies.rustc-hash]
version = "2.1"
features = ["std"]
default-features = false
[dependencies.serde]
version = "1.0"
features = ["derive"]
optional = true
[dependencies.smallvec]
version = "1.15"
features = ["serde"]
[dependencies.thiserror]
version = "2.0"
features = ["std"]
default-features = false
[dependencies.tracing]
version = "0.1"
features = ["std"]
default-features = false
[dev-dependencies.criterion]
version = "0.7"
[dev-dependencies.proptest]
version = "1.11"