oxidd_rules_bdd/
lib.rs

1//! Rules and other basic definitions for binary decision diagrams (BDDs)
2//!
3//! BDDs are represented using binary inner nodes with a level number, and two
4//! terminal nodes ⊤ and ⊥. The first outgoing edge (`node.get_child(0)`) is the
5//! "then" edge, the second edge is the "else" edge. Along with the
6//! ["simple"][simple] variant of BDDs, this crate also provides an
7//! implementation using [complemented edges][complement_edge] (here, we elide
8//! the ⊥ terminal).
9//!
10//! ## Feature flags
11#![doc = document_features::document_features!()]
12#![forbid(unsafe_code)]
13#![warn(missing_docs)]
14// `'id` lifetimes may make the code easier to understand
15#![allow(clippy::needless_lifetimes)]
16
17use oxidd_core::HasLevel;
18use oxidd_core::InnerNode;
19use oxidd_core::LevelNo;
20use oxidd_core::Manager;
21
22mod recursor;
23
24#[cfg(feature = "complement-edge")]
25pub mod complement_edge;
26#[cfg(feature = "simple")]
27pub mod simple;
28
29/// Remove all variables from `set` which are above level `until`
30///
31/// `set` is the conjunction of the variables. This means that popping a
32/// variable resorts to taking its “true” child.
33#[inline]
34fn set_pop<'a, M: Manager>(
35    manager: &'a M,
36    set: Borrowed<'a, M::Edge>,
37    until: LevelNo,
38) -> Borrowed<'a, M::Edge>
39where
40    M::InnerNode: HasLevel,
41{
42    match manager.get_node(&set) {
43        oxidd_core::Node::Inner(n) => {
44            if n.level() >= until {
45                set
46            } else {
47                // It seems like we cannot simply implement this as a loop due
48                // to lifetime restrictions. But the compiler should perform
49                // tail call optimization.
50                set_pop(manager, n.child(0), until)
51            }
52        }
53        oxidd_core::Node::Terminal(_) => set,
54    }
55}
56
57// --- Statistics --------------------------------------------------------------
58
59#[cfg(feature = "statistics")]
60struct StatCounters {
61    calls: std::sync::atomic::AtomicI64,
62    cache_queries: std::sync::atomic::AtomicI64,
63    cache_hits: std::sync::atomic::AtomicI64,
64    reduced: std::sync::atomic::AtomicI64,
65}
66
67#[cfg(feature = "statistics")]
68impl StatCounters {
69    #[allow(clippy::declare_interior_mutable_const)]
70    const INIT: StatCounters = StatCounters {
71        calls: std::sync::atomic::AtomicI64::new(0),
72        cache_queries: std::sync::atomic::AtomicI64::new(0),
73        cache_hits: std::sync::atomic::AtomicI64::new(0),
74        reduced: std::sync::atomic::AtomicI64::new(0),
75    };
76
77    fn print<O: oxidd_core::Countable + std::fmt::Debug>(counters: &[Self]) {
78        // spell-checker:ignore ctrs
79        for (i, ctrs) in counters.iter().enumerate() {
80            let calls = ctrs.calls.swap(0, std::sync::atomic::Ordering::Relaxed);
81            let cache_queries = ctrs
82                .cache_queries
83                .swap(0, std::sync::atomic::Ordering::Relaxed);
84            let cache_hits = ctrs
85                .cache_hits
86                .swap(0, std::sync::atomic::Ordering::Relaxed);
87            let reduced = ctrs.reduced.swap(0, std::sync::atomic::Ordering::Relaxed);
88
89            if calls == 0 {
90                continue;
91            }
92
93            let terminal_percent = (calls - cache_queries) as f32 / calls as f32 * 100.0;
94            let cache_hit_percent = cache_hits as f32 / cache_queries as f32 * 100.0;
95            let op = <O as oxidd_core::Countable>::from_usize(i);
96            eprintln!("  {op:?}: calls: {calls}, cache queries: {cache_queries} ({terminal_percent} % terminal cases), cache hits: {cache_hits} ({cache_hit_percent} %), reduced: {reduced}");
97        }
98    }
99}
100
101macro_rules! stat {
102    (call $op:expr) => {
103        let _ = $op as usize;
104        #[cfg(feature = "statistics")]
105        STAT_COUNTERS[$op as usize]
106            .calls
107            .fetch_add(1, ::std::sync::atomic::Ordering::Relaxed);
108    };
109    (cache_query $op:expr) => {
110        let _ = $op as usize;
111        #[cfg(feature = "statistics")]
112        STAT_COUNTERS[$op as usize]
113            .cache_queries
114            .fetch_add(1, ::std::sync::atomic::Ordering::Relaxed);
115    };
116    (cache_hit $op:expr) => {
117        let _ = $op as usize;
118        #[cfg(feature = "statistics")]
119        STAT_COUNTERS[$op as usize]
120            .cache_hits
121            .fetch_add(1, ::std::sync::atomic::Ordering::Relaxed);
122    };
123    (reduced $op:expr) => {
124        let _ = $op as usize;
125        #[cfg(feature = "statistics")]
126        STAT_COUNTERS[$op as usize]
127            .reduced
128            .fetch_add(1, ::std::sync::atomic::Ordering::Relaxed);
129    };
130}
131
132use oxidd_core::util::Borrowed;
133pub(crate) use stat;
oxidd_rules_bdd/lib.rs

oxidd_rules_bdd/
lib.rs
