bitwright 0.14.0

Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and verified simplification.
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

[package]
name = "bitwright"
description = "Hash-consed fixed-width bit-vector expressions: exact evaluation, bit-level facts, and verified simplification."
version.workspace = true
edition.workspace = true
rust-version.workspace = true
license.workspace = true
repository.workspace = true
authors.workspace = true
readme = "../README.md"
# Integration tests need the unpublished reference evaluator (`bitwright-ref`).
exclude = ["tests/"]
keywords = ["bitvector", "smt", "simplification", "deobfuscation", "symbolic"]
categories = ["mathematics", "compilers", "algorithms"]

[package.metadata.docs.rs]
# Document the optional services (MBA, equality saturation, SMT-LIB) too.
all-features = true

[dependencies]
hashbrown = { version = "0.17", default-features = false }

[features]
default = ["check"]
## The rule soundness checker (`bitwright::check`); it proves rules with the native prover.
check = ["prove"]
## The native prover (`bitwright::prove`): bit-blasting, a CDCL SAT solver, DRUP certificates.
prove = []
## The MBA service (`bitwright::mba`, `Phase::Mba`) with the native signature solver.
mba = []
## The equality-saturation search service (`bitwright::eqsat`), default off.
eqsat = []
## SMT-LIB 2.6 export of expressions and rule obligations, and import of a QF_BV subset.
smtlib = []

[dev-dependencies]
bitwright-ref = { path = "../bitwright-ref" }

[lints]
workspace = true