espresso_logic/expression/
conversions.rs

1//! Conversions for BoolExpr
2//!
3//! This module provides conversion implementations between `BoolExpr` and `Dnf`.
4//!
5//! **Note (v3.1.1+):** `BoolExpr` and `Bdd` were unified—`Bdd` is now a type alias for `BoolExpr`.
6//! All boolean expressions use BDD as their internal representation. The conversions extract
7//! DNF from the internal BDD or create new BDD-backed expressions from DNF.
8
9use crate::cover::Dnf;
10use crate::expression::BoolExpr;
11
12// ============================================================================
13// Blanket Conversions TO Dnf
14// ============================================================================
15
16/// Convert BoolExpr to DNF
17///
18/// **Note (v3.1.1+):** BoolExpr IS a BDD internally. This extracts DNF from the internal
19/// BDD representation, ensuring canonical form and automatic optimisations.
20/// Uses caching to avoid expensive BDD traversal.
21impl From<BoolExpr> for Dnf {
22    fn from(expr: BoolExpr) -> Self {
23        expr.get_or_create_dnf()
24    }
25}
26
27/// Convert &BoolExpr to DNF
28///
29/// **Note (v3.1.1+):** BoolExpr IS a BDD internally. This extracts DNF from the internal
30/// BDD representation. Uses caching to avoid expensive BDD traversal.
31impl From<&BoolExpr> for Dnf {
32    fn from(expr: &BoolExpr) -> Self {
33        expr.get_or_create_dnf()
34    }
35}
36
37// Note (v3.1.1+): Bdd is a type alias for BoolExpr (unified architecture).
38// From<Bdd> implementations are covered by From<BoolExpr> above.
39
40// ============================================================================
41// Conversions FROM Dnf
42// ============================================================================
43
44/// Convert DNF to BoolExpr
45///
46/// **Note (v3.1.1+):** Creates a new BoolExpr with BDD as internal representation.
47/// Reconstructs a boolean expression in DNF form (OR of AND terms), which is then
48/// converted to BDD representation internally.
49///
50/// # Examples
51///
52/// ```
53/// use espresso_logic::{BoolExpr, Dnf};
54///
55/// let a = BoolExpr::variable("a");
56/// let b = BoolExpr::variable("b");
57/// let expr = a.and(&b);
58///
59/// let dnf = Dnf::from(&expr);
60/// let expr2 = BoolExpr::from(dnf);
61///
62/// assert!(expr.equivalent_to(&expr2));
63/// ```
64impl From<Dnf> for BoolExpr {
65    fn from(dnf: Dnf) -> Self {
66        if dnf.is_empty() {
67            return BoolExpr::constant(false);
68        }
69
70        // Convert each cube to a product term
71        let mut terms = Vec::new();
72        for cube in dnf.cubes() {
73            if cube.is_empty() {
74                // Empty cube means tautology (all variables are don't-care)
75                terms.push(BoolExpr::constant(true));
76            } else {
77                // Build AND of all literals in this cube
78                let factors: Vec<BoolExpr> = cube
79                    .iter()
80                    .map(|(var, &polarity)| {
81                        let v = BoolExpr::variable(var);
82                        if polarity {
83                            v
84                        } else {
85                            v.not()
86                        }
87                    })
88                    .collect();
89
90                let product = factors.into_iter().reduce(|acc, f| acc.and(&f)).unwrap();
91                terms.push(product);
92            }
93        }
94
95        // OR all terms together
96        let expr = terms.into_iter().reduce(|acc, t| acc.or(&t)).unwrap();
97
98        // Cache the source DNF (likely minimised from Espresso)
99        let _ = expr.dnf_cache.set(dnf);
100
101        expr
102    }
103}
104
105// Note: Bdd is now a type alias for BoolExpr, so From<Dnf> for Bdd
106// is covered by the From<Dnf> for BoolExpr implementation above.
espresso_logic/expression/conversions.rs

espresso_logic/expression/
conversions.rs
