Ananke is a collection of Decision Diagram (DD) libraries for Rust, focused on formal verification, static analysis, and symbolic logic research.
Core engines for different symbolic representations:
-
ananke-bdd : Binary Decision Diagrams (ROBDDs) with complement edges.
-
ananke-zdd : Zero-suppressed Decision Diagrams for sparse sets and combinatorial problems.
-
ananke-sdd : Sentential Decision Diagrams for succinct representation of complex knowledge bases.
Symbolic algorithms and analysis frameworks:
-
Abstract Interpretation : Static program analysis using BDDs to represent numeric and symbolic domains.
-
Symbolic Model Checking : CTL verification algorithms (EX, EF, AG, etc.) for large state spaces.
-
Symbolic Execution : Path-sensitive analysis for Boolean programs with counterexample generation.
Explorations in Boolean function theory and testing:
-
Theory-aware BDD-guided PBT : Integrating BDDs with property-based testing to handle domain-specific constraints.
-
Canonical Interaction Graphs (CIG) : Analyzing structural properties of Boolean functions via interaction graphs.
-
Boolean Function Space : Analysis and visualization of the Boolean function space.
-
Symbolic Expression Space : Symbolic representation and manipulation of Boolean expression tree spaces.
Add the desired engine to your Cargo.toml:
[dependencies] ananke-bdd = "0.1" # or ananke-zdd, ananke-sdd
For research examples, clone the repository and run via cargo:
git clone https://github.com/Lipen/ananke
cd ananke
cargo run -p model-checking --example mutexuse ananke_bdd::bdd::Bdd; let bdd = Bdd::default(); let x1 = bdd.mk_var(1); let x2 = bdd.mk_var(2); // f = x1 β§ Β¬x2 let f = bdd.apply_and(x1, -x2); assert!(!bdd.is_zero(f)); // Satisfiable println!("f = {}", bdd.to_bracket_string(f)); // f = ~@3:(x1, @2:(x2, β€, β₯), β€)
-
Guides: Tutorials for BDDs, Abstract Interpretation, and Model Checking.
-
API: Run
cargo doc --no-depsfor the full reference. -
Examples: Each crate and case study includes a
READMEand runnable examples.
The implementation uses hash-consing, operation caching, and 32-bit node handles to manage large state spaces efficiently.
--release mode!
This project is licensed under the MIT License.