espresso_logic/expression/
operators.rs

1//! Operator overloading and boolean operations for boolean expressions
2
3use super::manager::{FALSE_NODE, TRUE_NODE};
4use super::BoolExpr;
5use std::ops::{Add, Mul, Not};
6use std::sync::{Arc, OnceLock};
7
8/// Logical AND operator for references: `&a * &b`
9///
10/// Implements the `*` operator for boolean expressions using references.
11/// This is the most efficient form as it avoids unnecessary cloning.
12///
13/// # Examples
14///
15/// ```
16/// use espresso_logic::BoolExpr;
17///
18/// let a = BoolExpr::variable("a");
19/// let b = BoolExpr::variable("b");
20/// let result = &a * &b;  // Equivalent to a.and(&b)
21/// ```
22impl Mul for &BoolExpr {
23    type Output = BoolExpr;
24
25    fn mul(self, rhs: &BoolExpr) -> BoolExpr {
26        self.and(rhs)
27    }
28}
29
30/// Logical AND operator: `a * b` (delegates to reference version)
31///
32/// Implements the `*` operator for owned boolean expressions.
33/// Note: Using references (`&a * &b`) is preferred for efficiency.
34///
35/// # Examples
36///
37/// ```
38/// use espresso_logic::BoolExpr;
39///
40/// let a = BoolExpr::variable("a");
41/// let b = BoolExpr::variable("b");
42/// // Both work, but references are preferred
43/// let result1 = a.clone() * b.clone();
44/// let result2 = &a * &b;
45/// ```
46impl Mul for BoolExpr {
47    type Output = BoolExpr;
48
49    fn mul(self, rhs: BoolExpr) -> BoolExpr {
50        self.and(&rhs)
51    }
52}
53
54/// Logical OR operator for references: `&a + &b`
55///
56/// Implements the `+` operator for boolean expressions using references.
57/// This is the most efficient form as it avoids unnecessary cloning.
58///
59/// # Examples
60///
61/// ```
62/// use espresso_logic::BoolExpr;
63///
64/// let a = BoolExpr::variable("a");
65/// let b = BoolExpr::variable("b");
66/// let result = &a + &b;  // Equivalent to a.or(&b)
67/// ```
68impl Add for &BoolExpr {
69    type Output = BoolExpr;
70
71    fn add(self, rhs: &BoolExpr) -> BoolExpr {
72        self.or(rhs)
73    }
74}
75
76/// Logical OR operator: `a + b` (delegates to reference version)
77///
78/// Implements the `+` operator for owned boolean expressions.
79/// Note: Using references (`&a + &b`) is preferred for efficiency.
80///
81/// # Examples
82///
83/// ```
84/// use espresso_logic::BoolExpr;
85///
86/// let a = BoolExpr::variable("a");
87/// let b = BoolExpr::variable("b");
88/// // Both work, but references are preferred
89/// let result1 = a.clone() + b.clone();
90/// let result2 = &a + &b;
91/// ```
92impl Add for BoolExpr {
93    type Output = BoolExpr;
94
95    fn add(self, rhs: BoolExpr) -> BoolExpr {
96        self.or(&rhs)
97    }
98}
99
100/// Logical NOT operator for references: `!&a`
101///
102/// Implements the `!` operator for boolean expressions using references.
103/// This is the most efficient form as it avoids unnecessary cloning.
104///
105/// # Examples
106///
107/// ```
108/// use espresso_logic::BoolExpr;
109///
110/// let a = BoolExpr::variable("a");
111/// let result = !&a;  // Equivalent to a.not()
112/// ```
113impl Not for &BoolExpr {
114    type Output = BoolExpr;
115
116    fn not(self) -> BoolExpr {
117        BoolExpr::not(self)
118    }
119}
120
121/// Logical NOT operator: `!a` (delegates to reference version)
122///
123/// Implements the `!` operator for owned boolean expressions.
124/// Note: Using references (`!&a`) is preferred for efficiency when the
125/// original expression is still needed.
126///
127/// # Examples
128///
129/// ```
130/// use espresso_logic::BoolExpr;
131///
132/// let a = BoolExpr::variable("a");
133/// // Both work, but references are preferred if you need 'a' later
134/// let result1 = !a.clone();
135/// let result2 = !&a;
136/// ```
137impl Not for BoolExpr {
138    type Output = BoolExpr;
139
140    fn not(self) -> BoolExpr {
141        BoolExpr::not(&self)
142    }
143}
144
145// Boolean operation methods
146impl BoolExpr {
147    /// Logical AND: create a new expression that is the conjunction of this and another
148    ///
149    /// Computes the conjunction using the BDD ITE operation:
150    /// `and(f, g) = ite(f, g, false)`
151    pub fn and(&self, other: &BoolExpr) -> BoolExpr {
152        // Use ITE: and(f, g) = ite(f, g, false)
153        let manager = Arc::clone(&self.manager);
154        let result = manager
155            .write()
156            .unwrap()
157            .ite(self.root, other.root, FALSE_NODE);
158        BoolExpr {
159            manager,
160            root: result,
161            dnf_cache: OnceLock::new(),
162            ast_cache: OnceLock::new(),
163        }
164    }
165
166    /// Logical OR: create a new expression that is the disjunction of this and another
167    ///
168    /// Computes the disjunction using the BDD ITE operation:
169    /// `or(f, g) = ite(f, true, g)`
170    pub fn or(&self, other: &BoolExpr) -> BoolExpr {
171        // Use ITE: or(f, g) = ite(f, true, g)
172        let manager = Arc::clone(&self.manager);
173        let result = manager
174            .write()
175            .unwrap()
176            .ite(self.root, TRUE_NODE, other.root);
177        BoolExpr {
178            manager,
179            root: result,
180            dnf_cache: OnceLock::new(),
181            ast_cache: OnceLock::new(),
182        }
183    }
184
185    /// Logical NOT: create a new expression that is the negation of this one
186    ///
187    /// Computes the negation using the BDD ITE operation:
188    /// `not(f) = ite(f, false, true)`
189    pub fn not(&self) -> BoolExpr {
190        // Use ITE: not(f) = ite(f, false, true)
191        let manager = Arc::clone(&self.manager);
192        let result = manager
193            .write()
194            .unwrap()
195            .ite(self.root, FALSE_NODE, TRUE_NODE);
196        BoolExpr {
197            manager,
198            root: result,
199            dnf_cache: OnceLock::new(),
200            ast_cache: OnceLock::new(),
201        }
202    }
203}
espresso_logic/expression/operators.rs

espresso_logic/expression/
operators.rs
