oxidd_rules_bdd/simple/
mod.rs

1//! Simple binary decision diagrams (i.e. no complemented edges)
2
3use std::borrow::Borrow;
4use std::fmt;
5use std::hash::Hash;
6
7use oxidd_core::util::{AllocResult, Borrowed};
8use oxidd_core::{DiagramRules, Edge, InnerNode, LevelNo, Manager, Node, ReducedOrNew};
9use oxidd_derive::Countable;
10
11use crate::stat;
12
13mod apply_rec;
14
15// --- Reduction Rules ---------------------------------------------------------
16
17/// [`DiagramRules`] for simple binary decision diagrams
18pub struct BDDRules;
19
20impl<E: Edge, N: InnerNode<E>> DiagramRules<E, N, BDDTerminal> for BDDRules {
21    type Cofactors<'a>
22        = N::ChildrenIter<'a>
23    where
24        N: 'a,
25        E: 'a;
26
27    #[inline(always)]
28    fn reduce<M: Manager<Edge = E, InnerNode = N>>(
29        manager: &M,
30        level: LevelNo,
31        children: impl IntoIterator<Item = E>,
32    ) -> ReducedOrNew<E, N> {
33        let mut it = children.into_iter();
34        let f_then = it.next().unwrap();
35        let f_else = it.next().unwrap();
36        debug_assert!(it.next().is_none());
37
38        if f_then == f_else {
39            manager.drop_edge(f_else);
40            ReducedOrNew::Reduced(f_then)
41        } else {
42            ReducedOrNew::New(N::new(level, [f_then, f_else]), Default::default())
43        }
44    }
45
46    #[inline(always)]
47    fn cofactors(_tag: E::Tag, node: &N) -> Self::Cofactors<'_> {
48        node.children()
49    }
50
51    #[inline(always)]
52    fn cofactor(_tag: E::Tag, node: &N, n: usize) -> Borrowed<'_, E> {
53        node.child(n)
54    }
55}
56
57/// Apply the reduction rules, creating a node in `manager` if necessary
58#[inline(always)]
59fn reduce<M>(manager: &M, level: LevelNo, t: M::Edge, e: M::Edge, op: BDDOp) -> AllocResult<M::Edge>
60where
61    M: Manager<Terminal = BDDTerminal>,
62{
63    // We do not use `DiagramRules::reduce()` here, as the iterator is
64    // apparently not fully optimized away.
65    if t == e {
66        stat!(reduced op);
67        manager.drop_edge(e);
68        return Ok(t);
69    }
70    oxidd_core::LevelView::get_or_insert(
71        &mut manager.level(level),
72        M::InnerNode::new(level, [t, e]),
73    )
74}
75
76/// Collect the two children of a binary node
77#[inline]
78#[must_use]
79fn collect_children<E: Edge, N: InnerNode<E>>(node: &N) -> (Borrowed<'_, E>, Borrowed<'_, E>) {
80    debug_assert_eq!(N::ARITY, 2);
81    let mut it = node.children();
82    let f_then = it.next().unwrap();
83    let f_else = it.next().unwrap();
84    debug_assert!(it.next().is_none());
85    (f_then, f_else)
86}
87
88// --- Terminal Type -----------------------------------------------------------
89
90/// Terminal nodes in simple binary decision diagrams
91#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Countable, Debug)]
92#[repr(u8)]
93pub enum BDDTerminal {
94    #[allow(missing_docs)]
95    False,
96    #[allow(missing_docs)]
97    True,
98}
99
100/// Error returned when parsing a [`BDDTerminal`] from string fails
101#[derive(Debug, PartialEq, Eq)]
102pub struct ParseTerminalErr;
103
104impl<Tag: Default> oxidd_dump::ParseTagged<Tag> for BDDTerminal {
105    fn parse(s: &str) -> Option<(Self, Tag)> {
106        let val = match s {
107            "t" | "T" | "true" | "True" | "TRUE" | "⊤" | "1" => BDDTerminal::True,
108            "f" | "F" | "false" | "False" | "FALSE" | "⊥" | "0" => BDDTerminal::False,
109            _ => return None,
110        };
111        Some((val, Tag::default()))
112    }
113}
114
115impl oxidd_dump::AsciiDisplay for BDDTerminal {
116    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
117        match self {
118            BDDTerminal::False => f.write_str("F"),
119            BDDTerminal::True => f.write_str("T"),
120        }
121    }
122}
123
124impl fmt::Display for BDDTerminal {
125    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
126        match self {
127            BDDTerminal::False => f.write_str("⊥"),
128            BDDTerminal::True => f.write_str("⊤"),
129        }
130    }
131}
132
133impl std::ops::Not for BDDTerminal {
134    type Output = BDDTerminal;
135
136    #[inline]
137    fn not(self) -> BDDTerminal {
138        match self {
139            BDDTerminal::False => BDDTerminal::True,
140            BDDTerminal::True => BDDTerminal::False,
141        }
142    }
143}
144
145/// Terminal case for binary operators
146#[inline]
147fn terminal_bin<'a, M: Manager<Terminal = BDDTerminal>, const OP: u8>(
148    m: &M,
149    f: &'a M::Edge,
150    g: &'a M::Edge,
151) -> Operation<'a, M::Edge> {
152    use BDDTerminal::*;
153    use Node::*;
154    use Operation::*;
155
156    if OP == BDDOp::And as u8 {
157        if f == g {
158            return Done(m.clone_edge(f));
159        }
160        match (m.get_node(f), m.get_node(g)) {
161            // Unique representation of {f, g} for commutative functions
162            (Inner(_), Inner(_)) if f > g => Binary(BDDOp::And, g.borrowed(), f.borrowed()),
163            (Inner(_), Inner(_)) => Binary(BDDOp::And, f.borrowed(), g.borrowed()),
164            (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == False => {
165                Done(m.get_terminal(False).unwrap())
166            }
167            (Terminal(_), _) => Done(m.clone_edge(g)),
168            (_, Terminal(_)) => Done(m.clone_edge(f)),
169        }
170    } else if OP == BDDOp::Or as u8 {
171        if f == g {
172            return Done(m.clone_edge(f));
173        }
174        match (m.get_node(f), m.get_node(g)) {
175            (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Or, g.borrowed(), f.borrowed()),
176            (Inner(_), Inner(_)) => Binary(BDDOp::Or, f.borrowed(), g.borrowed()),
177            (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == True => {
178                Done(m.get_terminal(True).unwrap())
179            }
180            (Terminal(_), _) => Done(m.clone_edge(g)),
181            (_, Terminal(_)) => Done(m.clone_edge(f)),
182        }
183    } else if OP == BDDOp::Nand as u8 {
184        if f == g {
185            return Not(f.borrowed());
186        }
187        match (m.get_node(f), m.get_node(g)) {
188            (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Nand, g.borrowed(), f.borrowed()),
189            (Inner(_), Inner(_)) => Binary(BDDOp::Nand, f.borrowed(), g.borrowed()),
190            (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == False => {
191                Done(m.get_terminal(True).unwrap())
192            }
193            (Terminal(_), _) => Not(g.borrowed()),
194            (_, Terminal(_)) => Not(f.borrowed()),
195        }
196    } else if OP == BDDOp::Nor as u8 {
197        if f == g {
198            return Not(f.borrowed());
199        }
200        match (m.get_node(f), m.get_node(g)) {
201            (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Nor, g.borrowed(), f.borrowed()),
202            (Inner(_), Inner(_)) => Binary(BDDOp::Nor, f.borrowed(), g.borrowed()),
203            (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == True => {
204                Done(m.get_terminal(False).unwrap())
205            }
206            (Terminal(_), _) => Not(g.borrowed()),
207            (_, Terminal(_)) => Not(f.borrowed()),
208        }
209    } else if OP == BDDOp::Xor as u8 {
210        if f == g {
211            return Done(m.get_terminal(False).unwrap());
212        }
213        match (m.get_node(f), m.get_node(g)) {
214            (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Xor, g.borrowed(), f.borrowed()),
215            (Inner(_), Inner(_)) => Binary(BDDOp::Xor, f.borrowed(), g.borrowed()),
216            (Terminal(t), _) if *t.borrow() == False => Done(m.clone_edge(g)),
217            (_, Terminal(t)) if *t.borrow() == False => Done(m.clone_edge(f)),
218            (Terminal(_), _) => Not(g.borrowed()),
219            (_, Terminal(_)) => Not(f.borrowed()),
220        }
221    } else if OP == BDDOp::Equiv as u8 {
222        if f == g {
223            return Done(m.get_terminal(True).unwrap());
224        }
225        match (m.get_node(f), m.get_node(g)) {
226            (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Equiv, g.borrowed(), f.borrowed()),
227            (Inner(_), Inner(_)) => Binary(BDDOp::Equiv, f.borrowed(), g.borrowed()),
228            (Terminal(t), _) if *t.borrow() == True => Done(m.clone_edge(g)),
229            (_, Terminal(t)) if *t.borrow() == True => Done(m.clone_edge(f)),
230            (Terminal(_), _) => Not(g.borrowed()),
231            (_, Terminal(_)) => Not(f.borrowed()),
232        }
233    } else if OP == BDDOp::Imp as u8 {
234        if f == g {
235            return Done(m.get_terminal(True).unwrap());
236        }
237        match (m.get_node(f), m.get_node(g)) {
238            (Inner(_), Inner(_)) => Binary(BDDOp::Imp, f.borrowed(), g.borrowed()),
239            (Terminal(t), _) if *t.borrow() == False => Done(m.get_terminal(True).unwrap()),
240            (_, Terminal(t)) if *t.borrow() == True => Done(m.get_terminal(True).unwrap()),
241            (Terminal(_), _) => Done(m.clone_edge(g)),
242            (_, Terminal(_)) => Not(f.borrowed()),
243        }
244    } else if OP == BDDOp::ImpStrict as u8 {
245        if f == g {
246            return Done(m.get_terminal(False).unwrap());
247        }
248        match (m.get_node(f), m.get_node(g)) {
249            (Inner(_), Inner(_)) => Binary(BDDOp::ImpStrict, f.borrowed(), g.borrowed()),
250            (Terminal(t), _) if *t.borrow() == True => Done(m.get_terminal(False).unwrap()),
251            (_, Terminal(t)) if *t.borrow() == False => Done(m.get_terminal(False).unwrap()),
252            (Terminal(_), _) => Done(m.clone_edge(g)),
253            (_, Terminal(_)) => Not(f.borrowed()),
254        }
255    } else {
256        unreachable!("invalid binary operator")
257    }
258}
259
260// --- Operations & Apply Implementation ---------------------------------------
261
262/// Native operators of this BDD implementation
263#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Hash, Ord, Countable, Debug)]
264#[repr(u8)]
265#[allow(missing_docs)]
266pub enum BDDOp {
267    Not,
268    And,
269    Or,
270    Nand,
271    Nor,
272    Xor,
273    Equiv,
274    Imp,
275    ImpStrict,
276
277    /// If-then-else
278    Ite,
279
280    Substitute,
281
282    Restrict,
283    /// Forall quantification
284    Forall,
285    /// Existential quantification
286    Exists,
287    /// Unique quantification
288    Unique,
289
290    ForallAnd,
291    ForallOr,
292    ForallNand,
293    ForallNor,
294    ForallXor,
295    ForallEquiv,
296    ForallImp,
297    ForallImpStrict,
298
299    ExistsAnd,
300    ExistsOr,
301    ExistsNand,
302    ExistsNor,
303    ExistsXor,
304    ExistsEquiv,
305    ExistsImp,
306    ExistsImpStrict,
307
308    UniqueAnd,
309    UniqueOr,
310    UniqueNand,
311    UniqueNor,
312    UniqueXor,
313    UniqueEquiv,
314    UniqueImp,
315    UniqueImpStrict,
316}
317
318impl BDDOp {
319    const fn from_apply_quant(q: u8, op: u8) -> Self {
320        if q == BDDOp::And as u8 {
321            match () {
322                _ if op == BDDOp::And as u8 => BDDOp::ForallAnd,
323                _ if op == BDDOp::Or as u8 => BDDOp::ForallOr,
324                _ if op == BDDOp::Nand as u8 => BDDOp::ForallNand,
325                _ if op == BDDOp::Nor as u8 => BDDOp::ForallNor,
326                _ if op == BDDOp::Xor as u8 => BDDOp::ForallXor,
327                _ if op == BDDOp::Equiv as u8 => BDDOp::ForallEquiv,
328                _ if op == BDDOp::Imp as u8 => BDDOp::ForallImp,
329                _ if op == BDDOp::ImpStrict as u8 => BDDOp::ForallImpStrict,
330                _ => panic!("invalid OP"),
331            }
332        } else if q == BDDOp::Or as u8 {
333            match () {
334                _ if op == BDDOp::And as u8 => BDDOp::ExistsAnd,
335                _ if op == BDDOp::Or as u8 => BDDOp::ExistsOr,
336                _ if op == BDDOp::Nand as u8 => BDDOp::ExistsNand,
337                _ if op == BDDOp::Nor as u8 => BDDOp::ExistsNor,
338                _ if op == BDDOp::Xor as u8 => BDDOp::ExistsXor,
339                _ if op == BDDOp::Equiv as u8 => BDDOp::ExistsEquiv,
340                _ if op == BDDOp::Imp as u8 => BDDOp::ExistsImp,
341                _ if op == BDDOp::ImpStrict as u8 => BDDOp::ExistsImpStrict,
342                _ => panic!("invalid OP"),
343            }
344        } else if q == BDDOp::Xor as u8 {
345            match () {
346                _ if op == BDDOp::And as u8 => BDDOp::UniqueAnd,
347                _ if op == BDDOp::Or as u8 => BDDOp::UniqueOr,
348                _ if op == BDDOp::Nand as u8 => BDDOp::UniqueNand,
349                _ if op == BDDOp::Nor as u8 => BDDOp::UniqueNor,
350                _ if op == BDDOp::Xor as u8 => BDDOp::UniqueXor,
351                _ if op == BDDOp::Equiv as u8 => BDDOp::UniqueEquiv,
352                _ if op == BDDOp::Imp as u8 => BDDOp::UniqueImp,
353                _ if op == BDDOp::ImpStrict as u8 => BDDOp::UniqueImpStrict,
354                _ => panic!("invalid OP"),
355            }
356        } else {
357            panic!("invalid quantifier");
358        }
359    }
360}
361
362enum Operation<'a, E: 'a + Edge> {
363    Binary(BDDOp, Borrowed<'a, E>, Borrowed<'a, E>),
364    Not(Borrowed<'a, E>),
365    Done(E),
366}
367
368#[cfg(feature = "statistics")]
369static STAT_COUNTERS: [crate::StatCounters; <BDDOp as oxidd_core::Countable>::MAX_VALUE + 1] =
370    [crate::StatCounters::INIT; <BDDOp as oxidd_core::Countable>::MAX_VALUE + 1];
371
372#[cfg(feature = "statistics")]
373/// Print statistics to stderr
374pub fn print_stats() {
375    eprintln!("[oxidd_rules_bdd::simple]");
376    crate::StatCounters::print::<BDDOp>(&STAT_COUNTERS);
377}
378
379// --- Function Interface ------------------------------------------------------
380
381#[cfg(feature = "multi-threading")]
382pub use apply_rec::mt::BDDFunctionMT;
383pub use apply_rec::BDDFunction;
oxidd_rules_bdd/simple/mod.rs

oxidd_rules_bdd/simple/
mod.rs
