oxilean_kernel/hash_cons/
mod.rs

1//! Structural sharing (hash-consing) for `Expr` values.
2//!
3//! A plain `Arena<Expr>` lets duplicate nodes coexist:
4//!
5//! ```text
6//! arena.alloc(Expr::BVar(0))  → Idx 0
7//! arena.alloc(Expr::BVar(0))  → Idx 1   // duplicate!
8//! ```
9//!
10//! `HashConsArena` wraps `Arena<Expr>` with a deduplication cache so that
11//! structurally equal expressions always share the same `Idx<Expr>`.
12//!
13//! # Usage
14//!
15//! ```
16//! use oxilean_kernel::hash_cons::HashConsArena;
17//! use oxilean_kernel::{Level, Name, BinderInfo};
18//!
19//! let mut hc = HashConsArena::new();
20//! let s1 = hc.mk_sort(Level::Zero);
21//! let s2 = hc.mk_sort(Level::Zero);
22//! assert_eq!(s1, s2, "identical sorts share one Idx");
23//! let stats = hc.stats();
24//! assert_eq!(stats.hits, 1);
25//! ```
26
27pub mod arena;
28pub mod key;
29pub mod stats;
30
31pub use arena::HashConsArena;
32pub use key::ExprKey;
33pub use stats::HashConsStats;
oxilean_kernel/hash_cons/mod.rs

oxilean_kernel/hash_cons/
mod.rs
