oxidd_core/
function.rs

1//! Function traits
2
3use std::fmt::Display;
4use std::hash::{BuildHasher, Hash};
5
6use nanorand::Rng;
7
8use crate::util::num::F64;
9use crate::util::{
10    AllocResult, Borrowed, EdgeDropGuard, NodeSet, OptBool, SatCountCache, SatCountNumber,
11    Substitution,
12};
13use crate::{DiagramRules, Edge, InnerNode, LevelNo, Manager, ManagerRef, Node, VarNo};
14
15/// Shorthand to get the [`Edge`] type associated with a [`Function`]
16pub type EdgeOfFunc<'id, F> = <<F as Function>::Manager<'id> as Manager>::Edge;
17/// Shorthand to get the edge tag type associated with a [`Function`]
18pub type ETagOfFunc<'id, F> = <<F as Function>::Manager<'id> as Manager>::EdgeTag;
19/// Shorthand to get the [`InnerNode`] type associated with a [`Function`]
20pub type INodeOfFunc<'id, F> = <<F as Function>::Manager<'id> as Manager>::InnerNode;
21/// Shorthand to get the `Terminal` type associated with a [`Function`]
22pub type TermOfFunc<'id, F> = <<F as Function>::Manager<'id> as Manager>::Terminal;
23
24/// Function in a decision diagram
25///
26/// A function is some kind of external reference to a node as opposed to
27/// [`Edge`]s, which are diagram internal. A function also includes a reference
28/// to the diagram's manager. So one may view a function as an [`Edge`] plus a
29/// [`ManagerRef`].
30///
31/// Functions are what the library's user mostly works with. There may be
32/// subtraits such as `BooleanFunction` in the `oxidd-rules-bdd` crate which
33/// provide more functionality, in this case applying connectives of boolean
34/// logic to other functions.
35///
36/// For some methods of this trait, there are notes on locking behavior. In a
37/// concurrent setting, a manager has some kind of read/write lock, and
38/// [`Self::with_manager_shared()`] / [`Self::with_manager_exclusive()`] acquire
39/// this lock accordingly. In a sequential implementation, a
40/// [`RefCell`][std::cell::RefCell] or the like may be used instead of lock.
41///
42/// # Safety
43///
44/// An implementation must ensure that the "[`Edge`] part" of the function
45/// points to a node that is stored in the manager referenced  by the
46/// "[`ManagerRef`] part" of the function. All functions of this trait must
47/// maintain this link accordingly. In particular, [`Self::as_edge()`] and
48/// [`Self::into_edge()`] must panic as specified there.
49pub unsafe trait Function: Clone + Ord + Hash {
50    /// Representation identifier such as "BDD" or "MTBDD"
51    const REPR_ID: &str; // `str` and not an `enum` for extensibility
52
53    /// Type of the associated manager
54    ///
55    /// This type is generic over a lifetime `'id` to permit the "lifetime
56    /// trick" used, e.g., in [`GhostCell`][GhostCell]: The idea is to make the
57    /// [`Manager`], [`Edge`] and [`InnerNode`] types [invariant][variance] over
58    /// `'id`. Any call to one of the
59    /// [`with_manager_shared()`][Function::with_manager_shared] /
60    /// [`with_manager_exclusive()`][Function::with_manager_exclusive] functions
61    /// of the [`Function`] or [`ManagerRef`] trait, which "generate" a fresh
62    /// lifetime `'id`. Now the type system ensures that every edge or node with
63    /// `'id` comes belongs to the manager from the `with_manager_*()` call.
64    /// This means that we can reduce the amount of runtime checks needed to
65    /// uphold the invariant that the children of a node stored in [`Manager`] M
66    /// are stored in M as well.
67    ///
68    /// Note that [`Function`] and [`ManagerRef`] are (typically) outside the
69    /// scope of this lifetime trick to make the library more flexible.
70    ///
71    /// [GhostCell]: https://plv.mpi-sws.org/rustbelt/ghostcell/
72    /// [variance]: https://doc.rust-lang.org/reference/subtyping.html
73    type Manager<'id>: Manager;
74
75    /// [Manager references][ManagerRef] for [`Self::Manager`]
76    type ManagerRef: for<'id> ManagerRef<Manager<'id> = Self::Manager<'id>>;
77
78    /// Create a new function from a manager reference and an edge
79    fn from_edge<'id>(manager: &Self::Manager<'id>, edge: EdgeOfFunc<'id, Self>) -> Self;
80
81    /// Create a new function from a manager reference and an edge reference
82    #[inline(always)]
83    fn from_edge_ref<'id>(manager: &Self::Manager<'id>, edge: &EdgeOfFunc<'id, Self>) -> Self {
84        Self::from_edge(manager, manager.clone_edge(edge))
85    }
86
87    /// Converts this function into the underlying edge (as reference), checking
88    /// that it belongs to the given `manager`
89    ///
90    /// Panics if the function does not belong to `manager`.
91    fn as_edge<'id>(&self, manager: &Self::Manager<'id>) -> &EdgeOfFunc<'id, Self>;
92
93    /// Converts this function into the underlying edge, checking that it
94    /// belongs to the given `manager`
95    ///
96    /// Panics if the function does not belong to `manager`.
97    fn into_edge<'id>(self, manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
98
99    /// Clone the [`ManagerRef`] part
100    fn manager_ref(&self) -> Self::ManagerRef;
101
102    /// Obtain a shared manager reference as well as the underlying edge
103    ///
104    /// Locking behavior: acquires the manager's lock for shared access.
105    ///
106    /// # Example
107    ///
108    /// ```
109    /// # use oxidd_core::function::Function;
110    /// fn my_eq<F: Function>(f: &F, g: &F) -> bool {
111    ///     f.with_manager_shared(|manager, f_edge| {
112    ///         // Do something meaningful with `manager` and `edge` (the following
113    ///         // is better done using `f == g` without `with_manager_shared()`)
114    ///         let g_edge = g.as_edge(manager);
115    ///         f_edge == g_edge
116    ///     })
117    /// }
118    /// ```
119    fn with_manager_shared<F, T>(&self, f: F) -> T
120    where
121        F: for<'id> FnOnce(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>) -> T;
122
123    /// Obtain an exclusive manager reference as well as the underlying edge
124    ///
125    /// Locking behavior: acquires the manager's lock for exclusive access.
126    ///
127    /// # Example
128    ///
129    /// ```
130    /// # use oxidd_core::{*, function::Function, util::AllocResult};
131    /// /// Adds a binary node on a new level with children `f` and `g`
132    /// fn foo<F: Function>(f: &F, g: &F) -> AllocResult<F> {
133    ///     f.with_manager_exclusive(|manager, f_edge| {
134    ///         let level = manager.add_vars(1).start;
135    ///         let fe = manager.clone_edge(f_edge);
136    ///         let ge = manager.clone_edge(g.as_edge(manager));
137    ///         let he = manager.level(level).get_or_insert(InnerNode::new(level, [fe, ge]))?;
138    ///         Ok(F::from_edge(manager, he))
139    ///     })
140    /// }
141    /// ```
142    fn with_manager_exclusive<F, T>(&self, f: F) -> T
143    where
144        F: for<'id> FnOnce(&mut Self::Manager<'id>, &EdgeOfFunc<'id, Self>) -> T;
145
146    /// Count the number of nodes in this function, including terminal nodes
147    ///
148    /// Locking behavior: acquires the manager's lock for shared access.
149    fn node_count(&self) -> usize {
150        fn inner<M: Manager>(manager: &M, e: &M::Edge, set: &mut M::NodeSet) {
151            if set.insert(e) {
152                if let Node::Inner(node) = manager.get_node(e) {
153                    for e in node.children() {
154                        inner(manager, &*e, set)
155                    }
156                }
157            }
158        }
159
160        self.with_manager_shared(|manager, edge| {
161            let mut set = Default::default();
162            inner(manager, edge, &mut set);
163            set.len()
164        })
165    }
166}
167
168/// Substitution extension for [`Function`]
169pub trait FunctionSubst: Function {
170    /// Substitute variables in `self` according to `substitution`
171    ///
172    /// The substitution is performed in a parallel fashion, e.g.:
173    /// `(¬x ∧ ¬y)[x ↦ ¬x ∧ ¬y, y ↦ ⊥] = ¬(¬x ∧ ¬y) ∧ ¬⊥ = x ∨ y`
174    ///
175    /// Locking behavior: acquires the manager's lock for shared access.
176    ///
177    /// Panics if `self` and the function in `substitution` don't belong to the
178    /// same manager.
179    fn substitute<'a>(
180        &'a self,
181        substitution: impl Substitution<Replacement = &'a Self>,
182    ) -> AllocResult<Self> {
183        if substitution.pairs().len() == 0 {
184            return Ok(self.clone());
185        }
186        self.with_manager_shared(|manager, edge| {
187            Ok(Self::from_edge(
188                manager,
189                Self::substitute_edge(
190                    manager,
191                    edge,
192                    substitution.map(|(v, r)| (v, r.as_edge(manager).borrowed())),
193                )?,
194            ))
195        })
196    }
197
198    /// `Edge` version of [`Self::substitute()`]
199    #[must_use]
200    fn substitute_edge<'id, 'a>(
201        manager: &'a Self::Manager<'id>,
202        edge: &'a EdgeOfFunc<'id, Self>,
203        substitution: impl Substitution<Replacement = Borrowed<'a, EdgeOfFunc<'id, Self>>>,
204    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
205}
206
207/// Boolean functions 𝔹ⁿ → 𝔹
208///
209/// As a user of this trait, you are probably most interested in methods like
210/// [`Self::not()`], [`Self::and()`], and [`Self::or()`]. As an implementor, it
211/// suffices to implement the functions operating on edges.
212pub trait BooleanFunction: Function {
213    /// Get the always false function `⊥`
214    fn f<'id>(manager: &Self::Manager<'id>) -> Self {
215        Self::from_edge(manager, Self::f_edge(manager))
216    }
217    /// Get the always true function `⊤`
218    fn t<'id>(manager: &Self::Manager<'id>) -> Self {
219        Self::from_edge(manager, Self::t_edge(manager))
220    }
221
222    /// Get the Boolean function that is true if and only if `var` is true
223    ///
224    /// Panics if `var` is greater or equal to the number of variables in
225    /// `manager`.
226    fn var<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<Self> {
227        Ok(Self::from_edge(manager, Self::var_edge(manager, var)?))
228    }
229
230    /// Get the Boolean function that is true if and only if `var` is false
231    ///
232    /// Panics if `var` is greater or equal to the number of variables in
233    /// `manager`.
234    fn not_var<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<Self> {
235        Ok(Self::from_edge(manager, Self::not_var_edge(manager, var)?))
236    }
237
238    /// Get the cofactors `(f_true, f_false)` of `self`
239    ///
240    /// Let f(x₀, …, xₙ) be represented by `self`, where x₀ is (currently) the
241    /// top-most variable. Then f<sub>true</sub>(x₁, …, xₙ) = f(⊤, x₁, …, xₙ)
242    /// and f<sub>false</sub>(x₁, …, xₙ) = f(⊥, x₁, …, xₙ).
243    ///
244    /// Note that the domain of f is 𝔹ⁿ⁺¹ while the domain of f<sub>true</sub>
245    /// and f<sub>false</sub> is 𝔹ⁿ. This is irrelevant in case of BDDs and
246    /// BCDDs, but not for ZBDDs: For instance, g(x₀) = x₀ and g'(x₀, x₁) = x₀
247    /// have the same representation as BDDs or BCDDs, but different
248    /// representations as ZBDDs.
249    ///
250    /// Structurally, the cofactors are simply the children in case of BDDs and
251    /// ZBDDs. (For BCDDs, the edge tags are adjusted accordingly.) On these
252    /// representations, runtime is thus in O(1).
253    ///
254    /// Returns `None` iff `self` references a terminal node. If you only need
255    /// `f_true` or `f_false`, [`Self::cofactor_true`] or
256    /// [`Self::cofactor_false`] are slightly more efficient.
257    ///
258    /// Locking behavior: acquires the manager's lock for shared access.
259    fn cofactors(&self) -> Option<(Self, Self)> {
260        self.with_manager_shared(|manager, f| {
261            let (ft, ff) = Self::cofactors_edge(manager, f)?;
262            Some((
263                Self::from_edge_ref(manager, &ft),
264                Self::from_edge_ref(manager, &ff),
265            ))
266        })
267    }
268
269    /// Get the cofactor `f_true` of `self`
270    ///
271    /// This method is slightly more efficient than [`Self::cofactors`] in case
272    /// `f_false` is not needed.
273    ///
274    /// For a more detailed description, see [`Self::cofactors`].
275    ///
276    /// Returns `None` iff `self` references a terminal node.
277    ///
278    /// Locking behavior: acquires the manager's lock for shared access.
279    fn cofactor_true(&self) -> Option<Self> {
280        self.with_manager_shared(|manager, f| {
281            let (ft, _) = Self::cofactors_edge(manager, f)?;
282            Some(Self::from_edge_ref(manager, &ft))
283        })
284    }
285
286    /// Get the cofactor `f_false` of `self`
287    ///
288    /// This method is slightly more efficient than [`Self::cofactors`] in case
289    /// `f_true` is not needed.
290    ///
291    /// For a more detailed description, see [`Self::cofactors`].
292    ///
293    /// Returns `None` iff `self` references a terminal node.
294    ///
295    /// Locking behavior: acquires the manager's lock for shared access.
296    fn cofactor_false(&self) -> Option<Self> {
297        self.with_manager_shared(|manager, f| {
298            let (_, ff) = Self::cofactors_edge(manager, f)?;
299            Some(Self::from_edge_ref(manager, &ff))
300        })
301    }
302
303    /// Compute the negation `¬self`
304    ///
305    /// Locking behavior: acquires the manager's lock for shared access.
306    fn not(&self) -> AllocResult<Self> {
307        self.with_manager_shared(|manager, edge| {
308            Ok(Self::from_edge(manager, Self::not_edge(manager, edge)?))
309        })
310    }
311    /// Compute the negation `¬self`, owned version
312    ///
313    /// Compared to [`Self::not()`], this method does not need to clone the
314    /// function, so when the implementation is using (e.g.) complemented edges,
315    /// this might be a little bit faster than [`Self::not()`].
316    ///
317    /// Locking behavior: acquires the manager's lock for shared access.
318    fn not_owned(self) -> AllocResult<Self> {
319        self.not()
320    }
321    /// Compute the conjunction `self ∧ rhs`
322    ///
323    /// Locking behavior: acquires the manager's lock for shared access.
324    ///
325    /// Panics if `self` and `rhs` don't belong to the same manager.
326    fn and(&self, rhs: &Self) -> AllocResult<Self> {
327        self.with_manager_shared(|manager, lhs| {
328            let e = Self::and_edge(manager, lhs, rhs.as_edge(manager))?;
329            Ok(Self::from_edge(manager, e))
330        })
331    }
332    /// Compute the disjunction `self ∨ rhs`
333    ///
334    /// Locking behavior: acquires the manager's lock for shared access.
335    ///
336    /// Panics if `self` and `rhs` don't belong to the same manager.
337    fn or(&self, rhs: &Self) -> AllocResult<Self> {
338        self.with_manager_shared(|manager, lhs| {
339            let e = Self::or_edge(manager, lhs, rhs.as_edge(manager))?;
340            Ok(Self::from_edge(manager, e))
341        })
342    }
343    /// Compute the negated conjunction `self ⊼ rhs`
344    ///
345    /// Locking behavior: acquires the manager's lock for shared access.
346    ///
347    /// Panics if `self` and `rhs` don't belong to the same manager.
348    fn nand(&self, rhs: &Self) -> AllocResult<Self> {
349        self.with_manager_shared(|manager, lhs| {
350            let e = Self::nand_edge(manager, lhs, rhs.as_edge(manager))?;
351            Ok(Self::from_edge(manager, e))
352        })
353    }
354    /// Compute the negated disjunction `self ⊽ rhs`
355    ///
356    /// Locking behavior: acquires the manager's lock for shared access.
357    ///
358    /// Panics if `self` and `rhs` don't belong to the same manager.
359    fn nor(&self, rhs: &Self) -> AllocResult<Self> {
360        self.with_manager_shared(|manager, lhs| {
361            let e = Self::nor_edge(manager, lhs, rhs.as_edge(manager))?;
362            Ok(Self::from_edge(manager, e))
363        })
364    }
365    /// Compute the exclusive disjunction `self ⊕ rhs`
366    ///
367    /// Locking behavior: acquires the manager's lock for shared access.
368    ///
369    /// Panics if `self` and `rhs` don't belong to the same manager.
370    fn xor(&self, rhs: &Self) -> AllocResult<Self> {
371        self.with_manager_shared(|manager, lhs| {
372            let e = Self::xor_edge(manager, lhs, rhs.as_edge(manager))?;
373            Ok(Self::from_edge(manager, e))
374        })
375    }
376    /// Compute the equivalence `self ↔ rhs`
377    ///
378    /// Locking behavior: acquires the manager's lock for shared access.
379    ///
380    /// Panics if `self` and `rhs` don't belong to the same manager.
381    fn equiv(&self, rhs: &Self) -> AllocResult<Self> {
382        self.with_manager_shared(|manager, lhs| {
383            let e = Self::equiv_edge(manager, lhs, rhs.as_edge(manager))?;
384            Ok(Self::from_edge(manager, e))
385        })
386    }
387    /// Compute the implication `self → rhs` (or `self ≤ rhs`)
388    ///
389    /// Locking behavior: acquires the manager's lock for shared access.
390    ///
391    /// Panics if `self` and `rhs` don't belong to the same manager.
392    fn imp(&self, rhs: &Self) -> AllocResult<Self> {
393        self.with_manager_shared(|manager, lhs| {
394            let e = Self::imp_edge(manager, lhs, rhs.as_edge(manager))?;
395            Ok(Self::from_edge(manager, e))
396        })
397    }
398    /// Compute the strict implication `self < rhs`
399    ///
400    /// Locking behavior: acquires the manager's lock for shared access.
401    ///
402    /// Panics if `self` and `rhs` don't belong to the same manager.
403    fn imp_strict(&self, rhs: &Self) -> AllocResult<Self> {
404        self.with_manager_shared(|manager, lhs| {
405            let e = Self::imp_strict_edge(manager, lhs, rhs.as_edge(manager))?;
406            Ok(Self::from_edge(manager, e))
407        })
408    }
409
410    /// Get the always false function `⊥` as edge
411    fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
412    /// Get the always true function `⊤` as edge
413    fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
414
415    /// Get the Boolean function (as edge) that is true if and only if `var` is
416    /// true
417    ///
418    /// Panics if `var` is greater or equal to the number of variables in
419    /// `manager`.
420    fn var_edge<'id>(
421        manager: &Self::Manager<'id>,
422        var: VarNo,
423    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
424
425    /// Get the Boolean function (as edge) that is true if and only if `var` is
426    /// false
427    ///
428    /// Panics if `var` is greater or equal to the number of variables in
429    /// `manager`.
430    fn not_var_edge<'id>(
431        manager: &Self::Manager<'id>,
432        var: VarNo,
433    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
434        Self::not_edge_owned(manager, Self::var_edge(manager, var)?)
435    }
436
437    /// Get the cofactors `(f_true, f_false)` of `f`, edge version
438    ///
439    /// Returns `None` iff `f` references a terminal node. For more details on
440    /// the semantics of `f_true` and `f_false`, see [`Self::cofactors`].
441    #[inline]
442    #[allow(clippy::type_complexity)]
443    fn cofactors_edge<'a, 'id>(
444        manager: &'a Self::Manager<'id>,
445        f: &'a EdgeOfFunc<'id, Self>,
446    ) -> Option<(
447        Borrowed<'a, EdgeOfFunc<'id, Self>>,
448        Borrowed<'a, EdgeOfFunc<'id, Self>>,
449    )> {
450        if let Node::Inner(node) = manager.get_node(f) {
451            Some(Self::cofactors_node(f.tag(), node))
452        } else {
453            None
454        }
455    }
456
457    /// Get the cofactors `(f_true, f_false)` of `node`, assuming an incoming
458    /// edge with `EdgeTag`
459    ///
460    /// Returns `None` iff `f` references a terminal node. For more details on
461    /// the semantics of `f_true` and `f_false`, see [`Self::cofactors`].
462    ///
463    /// Implementation note: The default implementation assumes that
464    /// [cofactor 0][DiagramRules::cofactor] corresponds to `f_true` and
465    /// [cofactor 1][DiagramRules::cofactor] corresponds to `f_false`.
466    #[inline]
467    fn cofactors_node<'a, 'id>(
468        tag: ETagOfFunc<'id, Self>,
469        node: &'a INodeOfFunc<'id, Self>,
470    ) -> (
471        Borrowed<'a, EdgeOfFunc<'id, Self>>,
472        Borrowed<'a, EdgeOfFunc<'id, Self>>,
473    ) {
474        let cofactor = <<Self::Manager<'id> as Manager>::Rules as DiagramRules<_, _, _>>::cofactor;
475        (cofactor(tag, node, 0), cofactor(tag, node, 1))
476    }
477
478    /// Compute the negation `¬edge`, edge version
479    #[must_use]
480    fn not_edge<'id>(
481        manager: &Self::Manager<'id>,
482        edge: &EdgeOfFunc<'id, Self>,
483    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
484
485    /// Compute the negation `¬edge`, owned edge version
486    ///
487    /// Compared to [`Self::not_edge()`], this method does not need to clone the
488    /// edge, so when the implementation is using (e.g.) complemented edges,
489    /// this might be a little bit faster than [`Self::not_edge()`].
490    #[must_use]
491    fn not_edge_owned<'id>(
492        manager: &Self::Manager<'id>,
493        edge: EdgeOfFunc<'id, Self>,
494    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
495        let edge = EdgeDropGuard::new(manager, edge);
496        Self::not_edge(manager, &edge)
497    }
498
499    /// Compute the conjunction `lhs ∧ rhs`, edge version
500    #[must_use]
501    fn and_edge<'id>(
502        manager: &Self::Manager<'id>,
503        lhs: &EdgeOfFunc<'id, Self>,
504        rhs: &EdgeOfFunc<'id, Self>,
505    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
506    /// Compute the disjunction `lhs ∨ rhs`, edge version
507    #[must_use]
508    fn or_edge<'id>(
509        manager: &Self::Manager<'id>,
510        lhs: &EdgeOfFunc<'id, Self>,
511        rhs: &EdgeOfFunc<'id, Self>,
512    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
513    /// Compute the negated conjunction `lhs ⊼ rhs`, edge version
514    #[must_use]
515    fn nand_edge<'id>(
516        manager: &Self::Manager<'id>,
517        lhs: &EdgeOfFunc<'id, Self>,
518        rhs: &EdgeOfFunc<'id, Self>,
519    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
520    /// Compute the negated disjunction `lhs ⊽ rhs`, edge version
521    #[must_use]
522    fn nor_edge<'id>(
523        manager: &Self::Manager<'id>,
524        lhs: &EdgeOfFunc<'id, Self>,
525        rhs: &EdgeOfFunc<'id, Self>,
526    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
527    /// Compute the exclusive disjunction `lhs ⊕ rhs`, edge version
528    #[must_use]
529    fn xor_edge<'id>(
530        manager: &Self::Manager<'id>,
531        lhs: &EdgeOfFunc<'id, Self>,
532        rhs: &EdgeOfFunc<'id, Self>,
533    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
534    /// Compute the equivalence `lhs ↔ rhs`, edge version
535    #[must_use]
536    fn equiv_edge<'id>(
537        manager: &Self::Manager<'id>,
538        lhs: &EdgeOfFunc<'id, Self>,
539        rhs: &EdgeOfFunc<'id, Self>,
540    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
541    /// Compute the implication `lhs → rhs`, edge version
542    #[must_use]
543    fn imp_edge<'id>(
544        manager: &Self::Manager<'id>,
545        lhs: &EdgeOfFunc<'id, Self>,
546        rhs: &EdgeOfFunc<'id, Self>,
547    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
548    /// Compute the strict implication `lhs < rhs`, edge version
549    #[must_use]
550    fn imp_strict_edge<'id>(
551        manager: &Self::Manager<'id>,
552        lhs: &EdgeOfFunc<'id, Self>,
553        rhs: &EdgeOfFunc<'id, Self>,
554    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
555
556    /// Returns `true` iff `self` is satisfiable, i.e. is not `⊥`
557    ///
558    /// Locking behavior: acquires the manager's lock for shared access.
559    fn satisfiable(&self) -> bool {
560        self.with_manager_shared(|manager, edge| {
561            let f = EdgeDropGuard::new(manager, Self::f_edge(manager));
562            edge != &*f
563        })
564    }
565
566    /// Returns `true` iff `self` is valid, i.e. is `⊤`
567    ///
568    /// Locking behavior: acquires the manager's lock for shared access.
569    fn valid(&self) -> bool {
570        self.with_manager_shared(|manager, edge| {
571            let t = EdgeDropGuard::new(manager, Self::t_edge(manager));
572            edge == &*t
573        })
574    }
575
576    /// Compute `if self { then_case } else { else_case }`
577    ///
578    /// This is equivalent to `(self ∧ then_case) ∨ (¬self ∧ else_case)` but
579    /// possibly more efficient than computing all the
580    /// conjunctions/disjunctions.
581    ///
582    /// Locking behavior: acquires the manager's lock for shared access.
583    ///
584    /// Panics if `self`, `then_case`, and `else_case` don't belong to the same
585    /// manager.
586    fn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self> {
587        self.with_manager_shared(|manager, if_edge| {
588            let then_edge = then_case.as_edge(manager);
589            let else_edge = else_case.as_edge(manager);
590            let res = Self::ite_edge(manager, if_edge, then_edge, else_edge)?;
591            Ok(Self::from_edge(manager, res))
592        })
593    }
594
595    /// Compute `if if_edge { then_edge } else { else_edge }` (edge version)
596    ///
597    /// This is equivalent to `(self ∧ then_case) ∨ (¬self ∧ else_case)` but
598    /// possibly more efficient than computing all the
599    /// conjunctions/disjunctions.
600    #[must_use]
601    fn ite_edge<'id>(
602        manager: &Self::Manager<'id>,
603        if_edge: &EdgeOfFunc<'id, Self>,
604        then_edge: &EdgeOfFunc<'id, Self>,
605        else_edge: &EdgeOfFunc<'id, Self>,
606    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
607        let f = EdgeDropGuard::new(manager, Self::and_edge(manager, if_edge, then_edge)?);
608        let g = EdgeDropGuard::new(manager, Self::imp_strict_edge(manager, if_edge, else_edge)?);
609        Self::or_edge(manager, &*f, &*g)
610    }
611
612    /// Count the number of satisfying assignments, assuming `vars` input
613    /// variables
614    ///
615    /// The `cache` can be used to speed up multiple model counting operations
616    /// for functions in the same decision diagram. If the model counts of just
617    /// one function are of interest, one may simply pass an empty
618    /// [`SatCountCache`] (using `&mut SatCountCache::default()`). The cache
619    /// will automatically be invalidated in case there have been reordering
620    /// operations or `vars` changed since the last query (see
621    /// [`SatCountCache::clear_if_invalid()`]). Still, it is the caller's
622    /// responsibility to not use the cache for different managers.
623    ///
624    /// Locking behavior: acquires the manager's lock for shared access.
625    fn sat_count<N: SatCountNumber, S: std::hash::BuildHasher>(
626        &self,
627        vars: LevelNo,
628        cache: &mut SatCountCache<N, S>,
629    ) -> N {
630        self.with_manager_shared(|manager, edge| Self::sat_count_edge(manager, edge, vars, cache))
631    }
632
633    /// `Edge` version of [`Self::sat_count()`]
634    fn sat_count_edge<'id, N: SatCountNumber, S: std::hash::BuildHasher>(
635        manager: &Self::Manager<'id>,
636        edge: &EdgeOfFunc<'id, Self>,
637        vars: LevelNo,
638        cache: &mut SatCountCache<N, S>,
639    ) -> N;
640
641    /// Pick a cube of this function
642    ///
643    /// A cube `c` of a function `f` is a satisfying assignment, i.e., `c → f`
644    /// holds, and can be represented as a conjunction of literals. It does
645    /// not necessarily define all variables in the function's domain (it is
646    /// not necessarily a canonical minterm). For most (if not all) kinds of
647    /// decision diagrams, cubes have at most one node per level.
648    ///
649    /// Returns `None` if the function is false. Otherwise, this method returns
650    /// a vector where the i-th entry indicates whether the i-th variable is
651    /// true, false, or "don't care."
652    ///
653    /// Whenever a value for a variable needs to be chosen (i.e., it cannot be
654    /// left as a don't care), `choice` is called to determine the valuation for
655    /// this variable. The argument of type [`LevelNo`] is the level
656    /// corresponding to that variable. It is guaranteed that `choice` will
657    /// only be called at most once for each level. The [`Edge`] argument is
658    /// guaranteed to point to an inner node at the respective level. (We
659    /// pass an [`Edge`] and not an [`InnerNode`] reference since [`Edge`]s
660    /// provide more information, e.g., the [`NodeID`][Edge::node_id()].)
661    ///
662    /// Locking behavior: acquires the manager's lock for shared access.
663    fn pick_cube(
664        &self,
665        choice: impl for<'id> FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool,
666    ) -> Option<Vec<OptBool>> {
667        self.with_manager_shared(|manager, edge| Self::pick_cube_edge(manager, edge, choice))
668    }
669
670    /// Pick a symbolic cube of this function, i.e., as decision diagram
671    ///
672    /// A cube `c` of a function `f` is a satisfying assignment, i.e., `c → f`
673    /// holds, and can be represented as a conjunction of literals. It does
674    /// not necessarily define all variables in the function's domain (it is
675    /// not necessarily a canonical minterm). For most (if not all) kinds of
676    /// decision diagrams, cubes have at most one node per level.
677    ///
678    /// Whenever a value for a variable needs to be chosen (i.e., it cannot be
679    /// left as a don't care), `choice` is called to determine the valuation for
680    /// this variable. The argument of type [`LevelNo`] is the level
681    /// corresponding to that variable. It is guaranteed that `choice` will
682    /// only be called at most once for each level. The [`Edge`] argument is
683    /// guaranteed to point to an inner node at the respective level. (We
684    /// pass an [`Edge`] and not an [`InnerNode`] reference since [`Edge`]s
685    /// provide more information, e.g., the [`NodeID`][Edge::node_id()].)
686    ///
687    /// If `self` is `⊥`, then the return value will be `⊥`.
688    ///
689    /// Locking behavior: acquires the manager's lock for shared access.
690    fn pick_cube_dd(
691        &self,
692        choice: impl for<'id> FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool,
693    ) -> AllocResult<Self> {
694        self.with_manager_shared(|manager, edge| {
695            let res = Self::pick_cube_dd_edge(manager, edge, choice)?;
696            Ok(Self::from_edge(manager, res))
697        })
698    }
699
700    /// Pick a symbolic cube of this function, i.e., as decision diagram, using
701    /// the literals in `literal_set` if there is a choice
702    ///
703    /// A cube `c` of a function `f` is a satisfying assignment, i.e., `c → f`
704    /// holds, and can be represented as a conjunction of literals. It does
705    /// not necessarily define all variables in the function's domain (it is
706    /// not necessarily a canonical minterm). For most (if not all) kinds of
707    /// decision diagrams, cubes have at most one node per level.
708    ///
709    /// `literal_set` is represented as a conjunction of literals. Whenever
710    /// there is a choice for a variable, it will be set to true if the variable
711    /// has a positive occurrence in `literal_set`, and set to false if it
712    /// occurs negated in `literal_set`. If the variable does not occur in
713    /// `literal_set`, then it will be left as don't care if possible, otherwise
714    /// an arbitrary (not necessarily random) choice will be performed.
715    ///
716    /// If `self` is `⊥`, then the return value will be `⊥`.
717    ///
718    /// Locking behavior: acquires the manager's lock for shared access.
719    fn pick_cube_dd_set(&self, literal_set: &Self) -> AllocResult<Self> {
720        self.with_manager_shared(|manager, edge| {
721            let res = Self::pick_cube_dd_set_edge(manager, edge, literal_set.as_edge(manager))?;
722            Ok(Self::from_edge(manager, res))
723        })
724    }
725
726    /// `Edge` version of [`Self::pick_cube()`]
727    fn pick_cube_edge<'id>(
728        manager: &Self::Manager<'id>,
729        edge: &EdgeOfFunc<'id, Self>,
730        choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool,
731    ) -> Option<Vec<OptBool>>;
732
733    /// `Edge` version of [`Self::pick_cube_dd()`]
734    fn pick_cube_dd_edge<'id>(
735        manager: &Self::Manager<'id>,
736        edge: &EdgeOfFunc<'id, Self>,
737        choice: impl FnMut(&Self::Manager<'id>, &EdgeOfFunc<'id, Self>, LevelNo) -> bool,
738    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
739
740    /// `Edge` version of [`Self::pick_cube_dd_set()`]
741    fn pick_cube_dd_set_edge<'id>(
742        manager: &Self::Manager<'id>,
743        edge: &EdgeOfFunc<'id, Self>,
744        literal_set: &EdgeOfFunc<'id, Self>,
745    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
746
747    /// Pick a random cube of this function, where each cube has the same
748    /// probability of being chosen
749    ///
750    /// Returns `None` if the function is false. Otherwise, this method returns
751    /// a vector where the i-th entry indicates whether the i-th variable is
752    /// true, false, or "don't care." To obtain a total valuation from this
753    /// partial valuation, it suffices to pick true or false with probability ½.
754    /// (Note that this function returns a partial valuation with n "don't
755    /// cares" with a probability that is 2<sup>n</sup> as high as the
756    /// probability of any total valuation.)
757    ///
758    /// Locking behavior: acquires the manager's lock for shared access.
759    fn pick_cube_uniform<S: BuildHasher>(
760        &self,
761        cache: &mut SatCountCache<F64, S>,
762        rng: &mut crate::util::Rng,
763    ) -> Option<Vec<OptBool>> {
764        self.with_manager_shared(|manager, edge| {
765            Self::pick_cube_uniform_edge(manager, edge, cache, rng)
766        })
767    }
768
769    /// `Edge` version of [`Self::pick_cube_uniform()`]
770    fn pick_cube_uniform_edge<'id, S: BuildHasher>(
771        manager: &Self::Manager<'id>,
772        edge: &EdgeOfFunc<'id, Self>,
773        cache: &mut SatCountCache<F64, S>,
774        rng: &mut crate::util::Rng,
775    ) -> Option<Vec<OptBool>> {
776        let vars = manager.num_levels();
777        Self::pick_cube_edge(manager, edge, |manager, edge, _| {
778            let tag = edge.tag();
779            // `edge` is guaranteed to point to an inner node
780            let node = manager.get_node(edge).unwrap_inner();
781            let (t, e) = Self::cofactors_node(tag, node);
782            let t_count = Self::sat_count_edge(manager, &*t, vars, cache).0;
783            let e_count = Self::sat_count_edge(manager, &*e, vars, cache).0;
784            rng.generate::<f64>() < t_count / (t_count + e_count)
785        })
786    }
787
788    /// Evaluate this Boolean function
789    ///
790    /// `args` consists of pairs `(variable, value)` and determines the
791    /// valuation for all variables in the function's domain. The order is
792    /// irrelevant (except that if the valuation for a variable is given
793    /// multiple times, the last value counts).
794    ///
795    /// Note that the domain of the Boolean function represented by `self` is
796    /// implicit and may comprise a strict subset of the variables in the
797    /// manager only. This method assumes that the function's domain
798    /// corresponds the set of variables in `args`. Remember that there are
799    /// kinds of decision diagrams (e.g., ZBDDs) where the domain plays a
800    /// crucial role for the interpretation of decision diagram nodes as a
801    /// Boolean function. On the other hand, extending the domain of, e.g.,
802    /// ordinary BDDs does not affect the evaluation result.
803    ///
804    /// Should there be a decision node for a variable not part of the domain,
805    /// then `false` is used as the decision value.
806    ///
807    /// Locking behavior: acquires the manager's lock for shared access.
808    ///
809    /// Panics if any variable number in `args` is larger that the number of
810    /// variables in the containing manager.
811    fn eval(&self, args: impl IntoIterator<Item = (VarNo, bool)>) -> bool {
812        self.with_manager_shared(|manager, edge| Self::eval_edge(manager, edge, args))
813    }
814
815    /// `Edge` version of [`Self::eval()`]
816    fn eval_edge<'id>(
817        manager: &Self::Manager<'id>,
818        edge: &EdgeOfFunc<'id, Self>,
819        args: impl IntoIterator<Item = (VarNo, bool)>,
820    ) -> bool;
821}
822
823// The `cfg_attr` below is used such that cbindgen does not output the
824// Rust-specific documentation.
825
826/// Binary operators on Boolean functions
827#[cfg_attr(
828    all(),
829    doc = "
830
831The operators are used by the combined apply and quantification operations of
832the [`BooleanFunctionQuant`] trait. The operators themselves correspond to the
833ones defined in [`BooleanFunction`]."
834)]
835#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
836#[repr(u8)]
837pub enum BooleanOperator {
838    /// Conjunction `lhs ∧ rhs`
839    And,
840    /// Disjunction `lhs ∨ rhs`
841    Or,
842    /// Exclusive disjunction `lhs ⊕ rhs`
843    Xor,
844    /// Equivalence `lhs ↔ rhs`
845    Equiv,
846    /// Negated conjunction `lhs ⊼ rhs`
847    Nand,
848    /// Negated disjunction `lhs ⊽ rhs`
849    Nor,
850    /// Implication `lhs → rhs`
851    Imp,
852    /// Strict implication `lhs < rhs`
853    ImpStrict,
854}
855
856/// cbindgen:ignore
857unsafe impl crate::Countable for BooleanOperator {
858    const MAX_VALUE: usize = BooleanOperator::ImpStrict as usize;
859
860    fn as_usize(self) -> usize {
861        self as usize
862    }
863
864    fn from_usize(value: usize) -> Self {
865        use BooleanOperator::*;
866        match () {
867            _ if value == And as usize => And,
868            _ if value == Or as usize => Or,
869            _ if value == Xor as usize => Xor,
870            _ if value == Equiv as usize => Equiv,
871            _ if value == Nand as usize => Nand,
872            _ if value == Nor as usize => Nor,
873            _ if value == Imp as usize => Imp,
874            _ if value == ImpStrict as usize => ImpStrict,
875            _ => panic!("{value} does not correspond to a Boolean operator"),
876        }
877    }
878}
879
880/// cbindgen:ignore
881impl Display for BooleanOperator {
882    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
883        use BooleanOperator::*;
884        match self {
885            And => write!(f, "∧"),
886            Or => write!(f, "∨"),
887            Xor => write!(f, "⊕"),
888            Equiv => write!(f, "↔"),
889            Nand => write!(f, "⊼"),
890            Nor => write!(f, "⊽"),
891            Imp => write!(f, "→"),
892            ImpStrict => write!(f, "<"),
893        }
894    }
895}
896
897/// Quantification extension for [`BooleanFunction`]
898pub trait BooleanFunctionQuant: BooleanFunction {
899    /// Restrict a set of `vars` to constant values
900    ///
901    /// `vars` conceptually is a partial assignment, represented as the
902    /// conjunction of positive or negative literals, depending on whether the
903    /// variable should be mapped to true or false.
904    ///
905    /// Locking behavior: acquires the manager's lock for shared access.
906    ///
907    /// Panics if `self` and `vars` don't belong to the same manager.
908    fn restrict(&self, vars: &Self) -> AllocResult<Self> {
909        self.with_manager_shared(|manager, root| {
910            let e = Self::restrict_edge(manager, root, vars.as_edge(manager))?;
911            Ok(Self::from_edge(manager, e))
912        })
913    }
914
915    /// Compute the universal quantification over `vars`
916    ///
917    /// `vars` is a set of variables, which in turn is just the conjunction of
918    /// the variables. This operation removes all occurrences of the variables
919    /// by universal quantification. Universal quantification `∀x. f(…, x, …)`
920    /// of a Boolean function `f(…, x, …)` over a single variable `x` is
921    /// `f(…, 0, …) ∧ f(…, 1, …)`.
922    ///
923    /// Locking behavior: acquires the manager's lock for shared access.
924    ///
925    /// Panics if `self` and `vars` don't belong to the same manager.
926    fn forall(&self, vars: &Self) -> AllocResult<Self> {
927        self.with_manager_shared(|manager, root| {
928            let e = Self::forall_edge(manager, root, vars.as_edge(manager))?;
929            Ok(Self::from_edge(manager, e))
930        })
931    }
932
933    /// Compute the existential quantification over `vars`
934    ///
935    /// `vars` is a set of variables, which in turn is just the conjunction of
936    /// the variables. This operation removes all occurrences of the variables
937    /// by existential quantification. Existential quantification
938    /// `∃x. f(…, x, …)` of a Boolean function `f(…, x, …)` over a single
939    /// variable `x` is `f(…, 0, …) ∨ f(…, 1, …)`.
940    ///
941    /// Locking behavior: acquires the manager's lock for shared access.
942    ///
943    /// Panics if `self` and `vars` don't belong to the same manager.
944    fn exists(&self, vars: &Self) -> AllocResult<Self> {
945        self.with_manager_shared(|manager, root| {
946            let e = Self::exists_edge(manager, root, vars.as_edge(manager))?;
947            Ok(Self::from_edge(manager, e))
948        })
949    }
950    /// Deprecated alias for [`Self::exists()`]
951    #[deprecated]
952    fn exist(&self, vars: &Self) -> AllocResult<Self> {
953        self.exists(vars)
954    }
955
956    /// Compute the unique quantification over `vars`
957    ///
958    /// `vars` is a set of variables, which in turn is just the conjunction of
959    /// the variables. This operation removes all occurrences of the variables
960    /// by unique quantification. Unique quantification `∃!x. f(…, x, …)` of a
961    /// Boolean function `f(…, x, …)` over a single variable `x` is
962    /// `f(…, 0, …) ⊕ f(…, 1, …)`.
963    ///
964    /// Unique quantification is also known as the
965    /// [Boolean difference](https://en.wikipedia.org/wiki/Boole%27s_expansion_theorem#Operations_with_cofactors)
966    /// or
967    /// [Boolean derivative](https://en.wikipedia.org/wiki/Boolean_differential_calculus).
968    ///
969    /// Locking behavior: acquires the manager's lock for shared access.
970    ///
971    /// Panics if `self` and `vars` don't belong to the same manager.
972    fn unique(&self, vars: &Self) -> AllocResult<Self> {
973        self.with_manager_shared(|manager, root| {
974            let e = Self::unique_edge(manager, root, vars.as_edge(manager))?;
975            Ok(Self::from_edge(manager, e))
976        })
977    }
978
979    /// Combined application of `op` and quantification `∀x. self <op> rhs`,
980    /// where `<op>` is any of the operations from [`BooleanOperator`]
981    ///
982    /// See also [`Self::forall()`] and the trait [`BooleanFunction`] for more
983    /// details.
984    ///
985    /// Locking behavior: acquires the manager's lock for shared access.
986    ///
987    /// Panics if `self` and `rhs` and `vars` don't belong to the same manager.
988    fn apply_forall(&self, op: BooleanOperator, rhs: &Self, vars: &Self) -> AllocResult<Self> {
989        self.with_manager_shared(|manager, root| {
990            let e = Self::apply_forall_edge(
991                manager,
992                op,
993                root,
994                rhs.as_edge(manager),
995                vars.as_edge(manager),
996            )?;
997            Ok(Self::from_edge(manager, e))
998        })
999    }
1000
1001    /// Combined application of `op` and quantification `∃x. self <op> rhs`,
1002    /// where `<op>` is any of the operations from [`BooleanOperator`]
1003    ///
1004    /// See also [`Self::exist()`] and the trait [`BooleanFunction`] for more
1005    /// details.
1006    ///
1007    /// Panics if `self` and `rhs` and `vars` don't belong to the same manager.
1008    fn apply_exists(&self, op: BooleanOperator, rhs: &Self, vars: &Self) -> AllocResult<Self> {
1009        self.with_manager_shared(|manager, root| {
1010            let e = Self::apply_exists_edge(
1011                manager,
1012                op,
1013                root,
1014                rhs.as_edge(manager),
1015                vars.as_edge(manager),
1016            )?;
1017            Ok(Self::from_edge(manager, e))
1018        })
1019    }
1020    /// Deprecated alias for [`Self::apply_exists()`]
1021    #[deprecated]
1022    #[must_use]
1023    fn apply_exist(&self, op: BooleanOperator, rhs: &Self, vars: &Self) -> AllocResult<Self> {
1024        self.apply_exists(op, rhs, vars)
1025    }
1026
1027    /// Combined application of `op` and quantification `∃!x. self <op> rhs`,
1028    /// where `<op>` is any of the operations from [`BooleanOperator`]
1029    ///
1030    /// See also [`Self::unique()`] and the trait [`BooleanFunction`] for more
1031    /// details.
1032    ///
1033    /// Panics if `self` and `rhs` and `vars` don't belong to the same manager.
1034    fn apply_unique(&self, op: BooleanOperator, rhs: &Self, vars: &Self) -> AllocResult<Self> {
1035        self.with_manager_shared(|manager, root| {
1036            let e = Self::apply_unique_edge(
1037                manager,
1038                op,
1039                root,
1040                rhs.as_edge(manager),
1041                vars.as_edge(manager),
1042            )?;
1043            Ok(Self::from_edge(manager, e))
1044        })
1045    }
1046
1047    /// Restrict a set of `vars` to constant values, edge version
1048    ///
1049    /// See [`Self::restrict()`] for more details.
1050    #[must_use]
1051    fn restrict_edge<'id>(
1052        manager: &Self::Manager<'id>,
1053        root: &EdgeOfFunc<'id, Self>,
1054        vars: &EdgeOfFunc<'id, Self>,
1055    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1056
1057    /// Compute the universal quantification of `root` over `vars`, edge
1058    /// version
1059    ///
1060    /// See [`Self::forall()`] for more details.
1061    #[must_use]
1062    fn forall_edge<'id>(
1063        manager: &Self::Manager<'id>,
1064        root: &EdgeOfFunc<'id, Self>,
1065        vars: &EdgeOfFunc<'id, Self>,
1066    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1067
1068    /// Compute the existential quantification of `root` over `vars`, edge
1069    /// version
1070    ///
1071    /// See [`Self::exists()`] for more details.
1072    #[must_use]
1073    fn exists_edge<'id>(
1074        manager: &Self::Manager<'id>,
1075        root: &EdgeOfFunc<'id, Self>,
1076        vars: &EdgeOfFunc<'id, Self>,
1077    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1078    /// Deprecated alias for [`Self::exists_edge()`]
1079    #[must_use]
1080    #[deprecated]
1081    fn exist_edge<'id>(
1082        manager: &Self::Manager<'id>,
1083        root: &EdgeOfFunc<'id, Self>,
1084        vars: &EdgeOfFunc<'id, Self>,
1085    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1086        Self::exists_edge(manager, root, vars)
1087    }
1088
1089    /// Compute the unique quantification of `root` over `vars`, edge version
1090    ///
1091    /// See [`Self::unique()`] for more details.
1092    #[must_use]
1093    fn unique_edge<'id>(
1094        manager: &Self::Manager<'id>,
1095        root: &EdgeOfFunc<'id, Self>,
1096        vars: &EdgeOfFunc<'id, Self>,
1097    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1098
1099    /// Combined application of `op` and forall quantification, edge version
1100    ///
1101    /// See [`Self::apply_forall()`] for more details.
1102    #[must_use]
1103    fn apply_forall_edge<'id>(
1104        manager: &Self::Manager<'id>,
1105        op: BooleanOperator,
1106        lhs: &EdgeOfFunc<'id, Self>,
1107        rhs: &EdgeOfFunc<'id, Self>,
1108        vars: &EdgeOfFunc<'id, Self>,
1109    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1110        // Naive default implementation
1111        use BooleanOperator::*;
1112        let inner = EdgeDropGuard::new(
1113            manager,
1114            match op {
1115                And => Self::and_edge(manager, lhs, rhs),
1116                Or => Self::or_edge(manager, lhs, rhs),
1117                Xor => Self::xor_edge(manager, lhs, rhs),
1118                Equiv => Self::equiv_edge(manager, lhs, rhs),
1119                Nand => Self::nand_edge(manager, lhs, rhs),
1120                Nor => Self::nor_edge(manager, lhs, rhs),
1121                Imp => Self::imp_edge(manager, lhs, rhs),
1122                ImpStrict => Self::imp_strict_edge(manager, lhs, rhs),
1123            }?,
1124        );
1125
1126        Self::forall_edge(manager, &inner, vars)
1127    }
1128
1129    /// Combined application of `op` and existential quantification, edge
1130    /// version
1131    ///
1132    /// See [`Self::apply_exist()`] for more details.
1133    #[must_use]
1134    fn apply_exists_edge<'id>(
1135        manager: &Self::Manager<'id>,
1136        op: BooleanOperator,
1137        lhs: &EdgeOfFunc<'id, Self>,
1138        rhs: &EdgeOfFunc<'id, Self>,
1139        vars: &EdgeOfFunc<'id, Self>,
1140    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1141        // Naive default implementation
1142        use BooleanOperator::*;
1143        let inner = EdgeDropGuard::new(
1144            manager,
1145            match op {
1146                And => Self::and_edge(manager, lhs, rhs),
1147                Or => Self::or_edge(manager, lhs, rhs),
1148                Xor => Self::xor_edge(manager, lhs, rhs),
1149                Equiv => Self::equiv_edge(manager, lhs, rhs),
1150                Nand => Self::nand_edge(manager, lhs, rhs),
1151                Nor => Self::nor_edge(manager, lhs, rhs),
1152                Imp => Self::imp_edge(manager, lhs, rhs),
1153                ImpStrict => Self::imp_strict_edge(manager, lhs, rhs),
1154            }?,
1155        );
1156
1157        Self::exists_edge(manager, &inner, vars)
1158    }
1159    /// Deprecated alias for [`Self::apply_exists_edge()`]
1160    #[deprecated]
1161    #[must_use]
1162    fn apply_exist_edge<'id>(
1163        manager: &Self::Manager<'id>,
1164        op: BooleanOperator,
1165        lhs: &EdgeOfFunc<'id, Self>,
1166        rhs: &EdgeOfFunc<'id, Self>,
1167        vars: &EdgeOfFunc<'id, Self>,
1168    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1169        Self::apply_exists_edge(manager, op, lhs, rhs, vars)
1170    }
1171
1172    /// Combined application of `op` and unique quantification, edge version
1173    ///
1174    /// See [`Self::apply_unique()`] for more details.
1175    #[must_use]
1176    fn apply_unique_edge<'id>(
1177        manager: &Self::Manager<'id>,
1178        op: BooleanOperator,
1179        lhs: &EdgeOfFunc<'id, Self>,
1180        rhs: &EdgeOfFunc<'id, Self>,
1181        vars: &EdgeOfFunc<'id, Self>,
1182    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1183        // Naive default implementation
1184        use BooleanOperator::*;
1185        let inner = EdgeDropGuard::new(
1186            manager,
1187            match op {
1188                And => Self::and_edge(manager, lhs, rhs),
1189                Or => Self::or_edge(manager, lhs, rhs),
1190                Xor => Self::xor_edge(manager, lhs, rhs),
1191                Equiv => Self::equiv_edge(manager, lhs, rhs),
1192                Nand => Self::nand_edge(manager, lhs, rhs),
1193                Nor => Self::nor_edge(manager, lhs, rhs),
1194                Imp => Self::imp_edge(manager, lhs, rhs),
1195                ImpStrict => Self::imp_strict_edge(manager, lhs, rhs),
1196            }?,
1197        );
1198
1199        Self::unique_edge(manager, &inner, vars)
1200    }
1201}
1202
1203/// Set of Boolean vectors
1204///
1205/// A Boolean function f: 𝔹ⁿ → 𝔹 may also be regarded as a set S ∈ 𝒫(𝔹ⁿ), where
1206/// S = {v ∈ 𝔹ⁿ | f(v) = 1}. f is also called the characteristic function of S.
1207/// We can even view a Boolean vector as a subset of some "universe" U, so we
1208/// also have S ∈ 𝒫(𝒫(U)). For example, let U = {a, b, c}. The function a is
1209/// the set of all sets containing a, {a, ab, abc, ac} (for the sake of
1210/// readability, we write ab for the set {a, b}). Conversely, the set {a} is the
1211/// function a ∧ ¬b ∧ ¬c.
1212///
1213/// Counting the number of elements in a `BooleanVecSet` is equivalent to
1214/// counting the number of satisfying assignments of its characteristic
1215/// function. Hence, you may use [`BooleanFunction::sat_count()`] for this task.
1216///
1217/// The functions of this trait can be implemented efficiently for ZBDDs.
1218///
1219/// As a user of this trait, you are probably most interested in methods like
1220/// [`Self::union()`], [`Self::intsec()`], and [`Self::diff()`]. As an
1221/// implementor, it suffices to implement the functions operating on edges.
1222pub trait BooleanVecSet: Function {
1223    /// Get the singleton set {var}
1224    ///
1225    /// Panics if `var` is greater or equal to the number of variables in
1226    /// `manager`.
1227    fn singleton<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<Self> {
1228        Ok(Self::from_edge(
1229            manager,
1230            Self::singleton_edge(manager, var)?,
1231        ))
1232    }
1233
1234    /// Get the empty set ∅
1235    ///
1236    /// This corresponds to the Boolean function ⊥.
1237    fn empty<'id>(manager: &Self::Manager<'id>) -> Self {
1238        Self::from_edge(manager, Self::empty_edge(manager))
1239    }
1240
1241    /// Get the set {∅}
1242    ///
1243    /// This corresponds to the Boolean function ¬x₁ ∧ … ∧ ¬xₙ
1244    fn base<'id>(manager: &Self::Manager<'id>) -> Self {
1245        Self::from_edge(manager, Self::base_edge(manager))
1246    }
1247
1248    /// Get the subset of `self` not containing `var`, formally
1249    /// `{s ∈ self | var ∉ s}`
1250    ///
1251    /// Locking behavior: acquires a shared manager lock
1252    ///
1253    /// Panics if `self` and `var` do not belong to the same manager.
1254    fn subset0(&self, var: VarNo) -> AllocResult<Self> {
1255        self.with_manager_shared(|manager, set| {
1256            let e = Self::subset0_edge(manager, set, var)?;
1257            Ok(Self::from_edge(manager, e))
1258        })
1259    }
1260
1261    /// Get the subset of `self` containing `var` with `var` removed afterwards,
1262    /// formally `{s ∖ {var} | s ∈ self ∧ var ∈ s}`
1263    ///
1264    /// Locking behavior: acquires a shared manager lock
1265    ///
1266    /// Panics if `self` and `var` do not belong to the same manager.
1267    fn subset1(&self, var: VarNo) -> AllocResult<Self> {
1268        self.with_manager_shared(|manager, set| {
1269            let e = Self::subset1_edge(manager, set, var)?;
1270            Ok(Self::from_edge(manager, e))
1271        })
1272    }
1273
1274    /// Swap [`subset0`][Self::subset0] and [`subset1`][Self::subset1] with
1275    /// respect to `var`, formally
1276    /// `{s ∪ {var} | s ∈ self ∧ var ∉ s} ∪ {s ∖ {var} | s ∈ self ∧ var ∈ s}`
1277    ///
1278    /// Locking behavior: acquires a shared manager lock
1279    ///
1280    /// Panics if `self` and `var` do not belong to the same manager.
1281    fn change(&self, var: VarNo) -> AllocResult<Self> {
1282        self.with_manager_shared(|manager, set| {
1283            let e = Self::change_edge(manager, set, var)?;
1284            Ok(Self::from_edge(manager, e))
1285        })
1286    }
1287
1288    /// Compute the union `self ∪ rhs`
1289    ///
1290    /// Locking behavior: acquires a shared manager lock
1291    ///
1292    /// Panics if `self` and `rhs` do not belong to the same manager.
1293    fn union(&self, rhs: &Self) -> AllocResult<Self> {
1294        self.with_manager_shared(|manager, lhs| {
1295            let e = Self::union_edge(manager, lhs, rhs.as_edge(manager))?;
1296            Ok(Self::from_edge(manager, e))
1297        })
1298    }
1299
1300    /// Compute the intersection `self ∩ rhs`
1301    ///
1302    /// Locking behavior: acquires a shared manager lock
1303    ///
1304    /// Panics if `self` and `rhs` do not belong to the same manager.
1305    fn intsec(&self, rhs: &Self) -> AllocResult<Self> {
1306        self.with_manager_shared(|manager, lhs| {
1307            let e = Self::intsec_edge(manager, lhs, rhs.as_edge(manager))?;
1308            Ok(Self::from_edge(manager, e))
1309        })
1310    }
1311
1312    /// Compute the set difference `self ∖ rhs`
1313    ///
1314    /// Locking behavior: acquires a shared manager lock
1315    ///
1316    /// Panics if `self` and `rhs` do not belong to the same manager.
1317    fn diff(&self, rhs: &Self) -> AllocResult<Self> {
1318        self.with_manager_shared(|manager, lhs| {
1319            let e = Self::diff_edge(manager, lhs, rhs.as_edge(manager))?;
1320            Ok(Self::from_edge(manager, e))
1321        })
1322    }
1323
1324    /// Edge version of [`Self::singleton()`]
1325    fn singleton_edge<'id>(
1326        manager: &Self::Manager<'id>,
1327        var: VarNo,
1328    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1329
1330    /// Edge version of [`Self::empty()`]
1331    fn empty_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
1332
1333    /// Edge version of [`Self::base()`]
1334    fn base_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
1335
1336    /// Edge version of [`Self::subset0()`]
1337    fn subset0_edge<'id>(
1338        manager: &Self::Manager<'id>,
1339        set: &EdgeOfFunc<'id, Self>,
1340        var: VarNo,
1341    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1342
1343    /// Edge version of [`Self::subset1()`]
1344    fn subset1_edge<'id>(
1345        manager: &Self::Manager<'id>,
1346        set: &EdgeOfFunc<'id, Self>,
1347        var: VarNo,
1348    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1349
1350    /// Edge version of [`Self::change()`]
1351    fn change_edge<'id>(
1352        manager: &Self::Manager<'id>,
1353        set: &EdgeOfFunc<'id, Self>,
1354        var: VarNo,
1355    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1356
1357    /// Compute the union `lhs ∪ rhs`, edge version
1358    fn union_edge<'id>(
1359        manager: &Self::Manager<'id>,
1360        lhs: &EdgeOfFunc<'id, Self>,
1361        rhs: &EdgeOfFunc<'id, Self>,
1362    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1363
1364    /// Compute the intersection `lhs ∩ rhs`, edge version
1365    fn intsec_edge<'id>(
1366        manager: &Self::Manager<'id>,
1367        lhs: &EdgeOfFunc<'id, Self>,
1368        rhs: &EdgeOfFunc<'id, Self>,
1369    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1370
1371    /// Compute the set difference `lhs ∖ rhs`, edge version
1372    fn diff_edge<'id>(
1373        manager: &Self::Manager<'id>,
1374        lhs: &EdgeOfFunc<'id, Self>,
1375        rhs: &EdgeOfFunc<'id, Self>,
1376    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1377}
1378
1379/// Basic trait for numbers
1380///
1381/// [`zero()`][Self::zero], [`one()`][Self::one], and [`nan()`][Self::nan] are
1382/// implemented as functions because depending on the number underlying type,
1383/// it can be hard/impossible to obtain a `const` for these values.
1384/// This trait also includes basic arithmetic methods. This is to avoid cloning
1385/// of big integers. We could also require `&Self: Add<&Self, Output = Self>`
1386/// etc., but this would lead to ugly trait bounds.
1387///
1388/// Used by [`PseudoBooleanFunction::Number`]
1389pub trait NumberBase: Clone + Eq + Hash + PartialOrd {
1390    /// Get the value 0
1391    fn zero() -> Self;
1392    /// Get the value 1
1393    fn one() -> Self;
1394
1395    /// Get the value "not a number," e.g. the result of a division 0/0.
1396    ///
1397    /// `Self::nan() == Self::nan()` should evaluate to `true`.
1398    fn nan() -> Self;
1399
1400    /// Returns `true` iff `self == Self::zero()`
1401    fn is_zero(&self) -> bool {
1402        self == &Self::zero()
1403    }
1404    /// Returns `true` iff `self == Self::one()`
1405    fn is_one(&self) -> bool {
1406        self == &Self::one()
1407    }
1408    /// Returns `true` iff `self == Self::nan()`
1409    fn is_nan(&self) -> bool {
1410        self == &Self::nan()
1411    }
1412
1413    /// Compute `self + rhs`
1414    fn add(&self, rhs: &Self) -> Self;
1415    /// Compute `self - rhs`
1416    fn sub(&self, rhs: &Self) -> Self;
1417    /// Compute `self * rhs`
1418    fn mul(&self, rhs: &Self) -> Self;
1419    /// Compute `self / rhs`
1420    fn div(&self, rhs: &Self) -> Self;
1421}
1422
1423/// Pseudo-Boolean function 𝔹ⁿ → ℝ
1424pub trait PseudoBooleanFunction: Function {
1425    /// The number type used for the functions' target set.
1426    type Number: NumberBase;
1427
1428    /// Get the constant `value`
1429    fn constant<'id>(manager: &Self::Manager<'id>, value: Self::Number) -> AllocResult<Self> {
1430        Ok(Self::from_edge(
1431            manager,
1432            Self::constant_edge(manager, value)?,
1433        ))
1434    }
1435
1436    /// Get the function that is 1 if the variable is true and 0 otherwise.
1437    ///
1438    /// Panics if `var` is greater or equal to the number of variables in
1439    /// `manager`.
1440    fn var<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<Self> {
1441        Ok(Self::from_edge(manager, Self::var_edge(manager, var)?))
1442    }
1443
1444    /// Point-wise addition `self + rhs`
1445    ///
1446    /// Locking behavior: acquires a shared manager lock
1447    ///
1448    /// Panics if `self` and `rhs` do not belong to the same manager.
1449    fn add(&self, rhs: &Self) -> AllocResult<Self> {
1450        self.with_manager_shared(|manager, lhs| {
1451            let e = Self::add_edge(manager, lhs, rhs.as_edge(manager))?;
1452            Ok(Self::from_edge(manager, e))
1453        })
1454    }
1455
1456    /// Point-wise subtraction `self - rhs`
1457    ///
1458    /// Locking behavior: acquires a shared manager lock
1459    ///
1460    /// Panics if `self` and `rhs` do not belong to the same manager.
1461    fn sub(&self, rhs: &Self) -> AllocResult<Self> {
1462        self.with_manager_shared(|manager, lhs| {
1463            let e = Self::sub_edge(manager, lhs, rhs.as_edge(manager))?;
1464            Ok(Self::from_edge(manager, e))
1465        })
1466    }
1467
1468    /// Point-wise multiplication `self * rhs`
1469    ///
1470    /// Locking behavior: acquires a shared manager lock
1471    ///
1472    /// Panics if `self` and `rhs` do not belong to the same manager.
1473    fn mul(&self, rhs: &Self) -> AllocResult<Self> {
1474        self.with_manager_shared(|manager, lhs| {
1475            let e = Self::mul_edge(manager, lhs, rhs.as_edge(manager))?;
1476            Ok(Self::from_edge(manager, e))
1477        })
1478    }
1479
1480    /// Point-wise division `self / rhs`
1481    ///
1482    /// Locking behavior: acquires a shared manager lock
1483    ///
1484    /// Panics if `self` and `rhs` do not belong to the same manager.
1485    fn div(&self, rhs: &Self) -> AllocResult<Self> {
1486        self.with_manager_shared(|manager, lhs| {
1487            let e = Self::div_edge(manager, lhs, rhs.as_edge(manager))?;
1488            Ok(Self::from_edge(manager, e))
1489        })
1490    }
1491
1492    /// Point-wise minimum `min(self, rhs)`
1493    ///
1494    /// Locking behavior: acquires a shared manager lock
1495    ///
1496    /// Panics if `self` and `rhs` do not belong to the same manager.
1497    fn min(&self, rhs: &Self) -> AllocResult<Self> {
1498        self.with_manager_shared(|manager, lhs| {
1499            let e = Self::min_edge(manager, lhs, rhs.as_edge(manager))?;
1500            Ok(Self::from_edge(manager, e))
1501        })
1502    }
1503
1504    /// Point-wise maximum `max(self, rhs)`
1505    ///
1506    /// Locking behavior: acquires a shared manager lock
1507    ///
1508    /// Panics if `self` and `rhs` do not belong to the same manager.
1509    fn max(&self, rhs: &Self) -> AllocResult<Self> {
1510        self.with_manager_shared(|manager, lhs| {
1511            let e = Self::max_edge(manager, lhs, rhs.as_edge(manager))?;
1512            Ok(Self::from_edge(manager, e))
1513        })
1514    }
1515
1516    /// Edge version of [`Self::constant()`]
1517    fn constant_edge<'id>(
1518        manager: &Self::Manager<'id>,
1519        value: Self::Number,
1520    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1521
1522    /// Edge version of [`Self::var()`]
1523    fn var_edge<'id>(
1524        manager: &Self::Manager<'id>,
1525        var: VarNo,
1526    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1527
1528    /// Edge version of [`Self::add()`]
1529    fn add_edge<'id>(
1530        manager: &Self::Manager<'id>,
1531        lhs: &EdgeOfFunc<'id, Self>,
1532        rhs: &EdgeOfFunc<'id, Self>,
1533    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1534
1535    /// Edge version of [`Self::sub()`]
1536    fn sub_edge<'id>(
1537        manager: &Self::Manager<'id>,
1538        lhs: &EdgeOfFunc<'id, Self>,
1539        rhs: &EdgeOfFunc<'id, Self>,
1540    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1541
1542    /// Edge version of [`Self::mul()`]
1543    fn mul_edge<'id>(
1544        manager: &Self::Manager<'id>,
1545        lhs: &EdgeOfFunc<'id, Self>,
1546        rhs: &EdgeOfFunc<'id, Self>,
1547    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1548
1549    /// Edge version of [`Self::div()`]
1550    fn div_edge<'id>(
1551        manager: &Self::Manager<'id>,
1552        lhs: &EdgeOfFunc<'id, Self>,
1553        rhs: &EdgeOfFunc<'id, Self>,
1554    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1555
1556    /// Edge version of [`Self::min()`]
1557    fn min_edge<'id>(
1558        manager: &Self::Manager<'id>,
1559        lhs: &EdgeOfFunc<'id, Self>,
1560        rhs: &EdgeOfFunc<'id, Self>,
1561    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1562
1563    /// Edge version of [`Self::max()`]
1564    fn max_edge<'id>(
1565        manager: &Self::Manager<'id>,
1566        lhs: &EdgeOfFunc<'id, Self>,
1567        rhs: &EdgeOfFunc<'id, Self>,
1568    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1569
1570    /// Evaluate this function
1571    ///
1572    /// `args` consists of pairs `(variable, value)` and determines the
1573    /// valuation for all variables in the function's domain. The order is
1574    /// irrelevant (except that if the valuation for a variable is given
1575    /// multiple times, the last value counts).
1576    ///
1577    /// Should there be a decision node for a variable not part of the domain,
1578    /// then `unknown` is used as the decision value.
1579    ///
1580    /// Locking behavior: acquires the manager's lock for shared access.
1581    ///
1582    /// Panics if any variable number in `args` is larger that the number of
1583    /// variables in the containing manager.
1584    fn eval(&self, args: impl IntoIterator<Item = (VarNo, bool)>) -> Self::Number {
1585        self.with_manager_shared(|manager, edge| Self::eval_edge(manager, edge, args))
1586    }
1587
1588    /// `Edge` version of [`Self::eval()`]
1589    fn eval_edge<'id>(
1590        manager: &Self::Manager<'id>,
1591        edge: &EdgeOfFunc<'id, Self>,
1592        args: impl IntoIterator<Item = (VarNo, bool)>,
1593    ) -> Self::Number;
1594}
1595
1596/// Function of three valued logic
1597pub trait TVLFunction: Function {
1598    /// Get the always false function `⊥`
1599    fn f<'id>(manager: &Self::Manager<'id>) -> Self {
1600        Self::from_edge(manager, Self::f_edge(manager))
1601    }
1602    /// Get the always true function `⊤`
1603    fn t<'id>(manager: &Self::Manager<'id>) -> Self {
1604        Self::from_edge(manager, Self::t_edge(manager))
1605    }
1606    /// Get the "unknown" function `U`
1607    fn u<'id>(manager: &Self::Manager<'id>) -> Self {
1608        Self::from_edge(manager, Self::t_edge(manager))
1609    }
1610
1611    /// Get the cofactors `(f_true, f_unknown, f_false)` of `self`
1612    ///
1613    /// Let f(x₀, …, xₙ) be represented by `self`, where x₀ is (currently) the
1614    /// top-most variable. Then f<sub>true</sub>(x₁, …, xₙ) = f(⊤, x₁, …, xₙ)
1615    /// and f<sub>false</sub>(x₁, …, xₙ) = f(⊥, x₁, …, xₙ).
1616    ///
1617    /// Note that the domain of f is 𝔹ⁿ⁺¹ while the domain of f<sub>true</sub>
1618    /// and f<sub>false</sub> is 𝔹ⁿ.
1619    ///
1620    /// Returns `None` iff `self` references a terminal node. If you only need
1621    /// `f_true`, `f_unknown`, or `f_false`, [`Self::cofactor_true`],
1622    /// [`Self::cofactor_unknown`], or [`Self::cofactor_false`] are slightly
1623    /// more efficient.
1624    ///
1625    /// Locking behavior: acquires the manager's lock for shared access.
1626    fn cofactors(&self) -> Option<(Self, Self, Self)> {
1627        self.with_manager_shared(|manager, f| {
1628            let (ft, fu, ff) = Self::cofactors_edge(manager, f)?;
1629            Some((
1630                Self::from_edge_ref(manager, &ft),
1631                Self::from_edge_ref(manager, &fu),
1632                Self::from_edge_ref(manager, &ff),
1633            ))
1634        })
1635    }
1636
1637    /// Get the cofactor `f_true` of `self`
1638    ///
1639    /// This method is slightly more efficient than [`Self::cofactors`] in case
1640    /// `f_unknown` and `f_false` are not needed.
1641    ///
1642    /// For a more detailed description, see [`Self::cofactors`].
1643    ///
1644    /// Returns `None` iff `self` references a terminal node.
1645    ///
1646    /// Locking behavior: acquires the manager's lock for shared access.
1647    fn cofactor_true(&self) -> Option<Self> {
1648        self.with_manager_shared(|manager, f| {
1649            let (ft, _, _) = Self::cofactors_edge(manager, f)?;
1650            Some(Self::from_edge_ref(manager, &ft))
1651        })
1652    }
1653    /// Get the cofactor `f_unknown` of `self`
1654    ///
1655    /// This method is slightly more efficient than [`Self::cofactors`] in case
1656    /// `f_true` and `f_false` are not needed.
1657    ///
1658    /// For a more detailed description, see [`Self::cofactors`].
1659    ///
1660    /// Returns `None` iff `self` references a terminal node.
1661    ///
1662    /// Locking behavior: acquires the manager's lock for shared access.
1663    fn cofactor_unknown(&self) -> Option<Self> {
1664        self.with_manager_shared(|manager, f| {
1665            let (_, fu, _) = Self::cofactors_edge(manager, f)?;
1666            Some(Self::from_edge_ref(manager, &fu))
1667        })
1668    }
1669    /// Get the cofactor `f_false` of `self`
1670    ///
1671    /// This method is slightly more efficient than [`Self::cofactors`] in case
1672    /// `f_true` and `f_unknown` are not needed.
1673    ///
1674    /// For a more detailed description, see [`Self::cofactors`].
1675    ///
1676    /// Returns `None` iff `self` references a terminal node.
1677    ///
1678    /// Locking behavior: acquires the manager's lock for shared access.
1679    fn cofactor_false(&self) -> Option<Self> {
1680        self.with_manager_shared(|manager, f| {
1681            let (_, _, ff) = Self::cofactors_edge(manager, f)?;
1682            Some(Self::from_edge_ref(manager, &ff))
1683        })
1684    }
1685
1686    /// Get the function that is true if the variable is true, false if the
1687    /// variable is false, and undefined otherwise
1688    ///
1689    /// Panics if `var` is greater or equal to the number of variables in
1690    /// `manager`.
1691    fn var<'id>(manager: &Self::Manager<'id>, var: VarNo) -> AllocResult<Self> {
1692        Ok(Self::from_edge(manager, Self::var_edge(manager, var)?))
1693    }
1694
1695    /// Compute the negation `¬self`
1696    ///
1697    /// Locking behavior: acquires the manager's lock for shared access.
1698    fn not(&self) -> AllocResult<Self> {
1699        self.with_manager_shared(|manager, edge| {
1700            Ok(Self::from_edge(manager, Self::not_edge(manager, edge)?))
1701        })
1702    }
1703    /// Compute the negation `¬self`, owned version
1704    ///
1705    /// Compared to [`Self::not()`], this method does not need to clone the
1706    /// function, so when the implementation is using (e.g.) complemented edges,
1707    /// this might be a little bit faster than [`Self::not()`].
1708    ///
1709    /// Locking behavior: acquires the manager's lock for shared access.
1710    fn not_owned(self) -> AllocResult<Self> {
1711        self.not()
1712    }
1713    /// Compute the conjunction `self ∧ rhs`
1714    ///
1715    /// Locking behavior: acquires the manager's lock for shared access.
1716    ///
1717    /// Panics if `self` and `rhs` don't belong to the same manager.
1718    fn and(&self, rhs: &Self) -> AllocResult<Self> {
1719        self.with_manager_shared(|manager, lhs| {
1720            let e = Self::and_edge(manager, lhs, rhs.as_edge(manager))?;
1721            Ok(Self::from_edge(manager, e))
1722        })
1723    }
1724    /// Compute the disjunction `self ∨ rhs`
1725    ///
1726    /// Locking behavior: acquires the manager's lock for shared access.
1727    ///
1728    /// Panics if `self` and `rhs` don't belong to the same manager.
1729    fn or(&self, rhs: &Self) -> AllocResult<Self> {
1730        self.with_manager_shared(|manager, lhs| {
1731            let e = Self::or_edge(manager, lhs, rhs.as_edge(manager))?;
1732            Ok(Self::from_edge(manager, e))
1733        })
1734    }
1735    /// Compute the negated conjunction `self ⊼ rhs`
1736    ///
1737    /// Locking behavior: acquires the manager's lock for shared access.
1738    ///
1739    /// Panics if `self` and `rhs` don't belong to the same manager.
1740    fn nand(&self, rhs: &Self) -> AllocResult<Self> {
1741        self.with_manager_shared(|manager, lhs| {
1742            let e = Self::nand_edge(manager, lhs, rhs.as_edge(manager))?;
1743            Ok(Self::from_edge(manager, e))
1744        })
1745    }
1746    /// Compute the negated disjunction `self ⊽ rhs`
1747    ///
1748    /// Locking behavior: acquires the manager's lock for shared access.
1749    ///
1750    /// Panics if `self` and `rhs` don't belong to the same manager.
1751    fn nor(&self, rhs: &Self) -> AllocResult<Self> {
1752        self.with_manager_shared(|manager, lhs| {
1753            let e = Self::nor_edge(manager, lhs, rhs.as_edge(manager))?;
1754            Ok(Self::from_edge(manager, e))
1755        })
1756    }
1757    /// Compute the exclusive disjunction `self ⊕ rhs`
1758    ///
1759    /// Locking behavior: acquires the manager's lock for shared access.
1760    ///
1761    /// Panics if `self` and `rhs` don't belong to the same manager.
1762    fn xor(&self, rhs: &Self) -> AllocResult<Self> {
1763        self.with_manager_shared(|manager, lhs| {
1764            let e = Self::xor_edge(manager, lhs, rhs.as_edge(manager))?;
1765            Ok(Self::from_edge(manager, e))
1766        })
1767    }
1768    /// Compute the equivalence `self ↔ rhs`
1769    ///
1770    /// Locking behavior: acquires the manager's lock for shared access.
1771    ///
1772    /// Panics if `self` and `rhs` don't belong to the same manager.
1773    fn equiv(&self, rhs: &Self) -> AllocResult<Self> {
1774        self.with_manager_shared(|manager, lhs| {
1775            let e = Self::equiv_edge(manager, lhs, rhs.as_edge(manager))?;
1776            Ok(Self::from_edge(manager, e))
1777        })
1778    }
1779    /// Compute the implication `self → rhs` (or `self ≤ rhs`)
1780    ///
1781    /// Locking behavior: acquires the manager's lock for shared access.
1782    ///
1783    /// Panics if `self` and `rhs` don't belong to the same manager.
1784    fn imp(&self, rhs: &Self) -> AllocResult<Self> {
1785        self.with_manager_shared(|manager, lhs| {
1786            let e = Self::imp_edge(manager, lhs, rhs.as_edge(manager))?;
1787            Ok(Self::from_edge(manager, e))
1788        })
1789    }
1790    /// Compute the strict implication `self < rhs`
1791    ///
1792    /// Locking behavior: acquires the manager's lock for shared access.
1793    ///
1794    /// Panics if `self` and `rhs` don't belong to the same manager.
1795    fn imp_strict(&self, rhs: &Self) -> AllocResult<Self> {
1796        self.with_manager_shared(|manager, lhs| {
1797            let e = Self::imp_strict_edge(manager, lhs, rhs.as_edge(manager))?;
1798            Ok(Self::from_edge(manager, e))
1799        })
1800    }
1801
1802    /// Get the always false function `⊥` as edge
1803    fn f_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
1804    /// Get the always true function `⊤` as edge
1805    fn t_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
1806    /// Get the "unknown" function `U` as edge
1807    fn u_edge<'id>(manager: &Self::Manager<'id>) -> EdgeOfFunc<'id, Self>;
1808
1809    /// Get the cofactors `(f_true, f_unknown, f_false)` of `f`, edge version
1810    ///
1811    /// Returns `None` iff `f` references a terminal node. For more details on
1812    /// the semantics of `f_true` and `f_false`, see [`Self::cofactors`].
1813    #[inline]
1814    #[allow(clippy::type_complexity)]
1815    fn cofactors_edge<'a, 'id>(
1816        manager: &'a Self::Manager<'id>,
1817        f: &'a EdgeOfFunc<'id, Self>,
1818    ) -> Option<(
1819        Borrowed<'a, EdgeOfFunc<'id, Self>>,
1820        Borrowed<'a, EdgeOfFunc<'id, Self>>,
1821        Borrowed<'a, EdgeOfFunc<'id, Self>>,
1822    )> {
1823        if let Node::Inner(node) = manager.get_node(f) {
1824            Some(Self::cofactors_node(f.tag(), node))
1825        } else {
1826            None
1827        }
1828    }
1829
1830    /// Get the cofactors `(f_true, f_unknown, f_false)` of `node`, assuming an
1831    /// incoming edge with `EdgeTag`
1832    ///
1833    /// Returns `None` iff `f` references a terminal node. For more details on
1834    /// the semantics of `f_true` and `f_false`, see [`Self::cofactors`].
1835    ///
1836    /// Implementation note: The default implementation assumes that
1837    /// [cofactor 0][DiagramRules::cofactor] corresponds to `f_true`,
1838    /// [cofactor 1][DiagramRules::cofactor] corresponds to `f_unknown`, and
1839    /// [cofactor 2][DiagramRules::cofactor] corresponds to `f_false`.
1840    #[inline]
1841    #[allow(clippy::type_complexity)]
1842    fn cofactors_node<'a, 'id>(
1843        tag: ETagOfFunc<'id, Self>,
1844        node: &'a INodeOfFunc<'id, Self>,
1845    ) -> (
1846        Borrowed<'a, EdgeOfFunc<'id, Self>>,
1847        Borrowed<'a, EdgeOfFunc<'id, Self>>,
1848        Borrowed<'a, EdgeOfFunc<'id, Self>>,
1849    ) {
1850        let cofactor = <<Self::Manager<'id> as Manager>::Rules as DiagramRules<_, _, _>>::cofactor;
1851        (
1852            cofactor(tag, node, 0),
1853            cofactor(tag, node, 1),
1854            cofactor(tag, node, 2),
1855        )
1856    }
1857
1858    /// Edge version of [`Self::var()`]
1859    fn var_edge<'id>(
1860        manager: &Self::Manager<'id>,
1861        var: VarNo,
1862    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1863
1864    /// Compute the negation `¬edge`, edge version
1865    #[must_use]
1866    fn not_edge<'id>(
1867        manager: &Self::Manager<'id>,
1868        edge: &EdgeOfFunc<'id, Self>,
1869    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1870
1871    /// Compute the negation `¬edge`, owned edge version
1872    ///
1873    /// Compared to [`Self::not_edge()`], this method does not need to clone the
1874    /// edge, so when the implementation is using (e.g.) complemented edges,
1875    /// this might be a little bit faster than [`Self::not_edge()`].
1876    #[must_use]
1877    fn not_edge_owned<'id>(
1878        manager: &Self::Manager<'id>,
1879        edge: EdgeOfFunc<'id, Self>,
1880    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1881        Self::not_edge(manager, &edge)
1882    }
1883
1884    /// Compute the conjunction `lhs ∧ rhs`, edge version
1885    #[must_use]
1886    fn and_edge<'id>(
1887        manager: &Self::Manager<'id>,
1888        lhs: &EdgeOfFunc<'id, Self>,
1889        rhs: &EdgeOfFunc<'id, Self>,
1890    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1891    /// Compute the disjunction `lhs ∨ rhs`, edge version
1892    #[must_use]
1893    fn or_edge<'id>(
1894        manager: &Self::Manager<'id>,
1895        lhs: &EdgeOfFunc<'id, Self>,
1896        rhs: &EdgeOfFunc<'id, Self>,
1897    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1898    /// Compute the negated conjunction `lhs ⊼ rhs`, edge version
1899    #[must_use]
1900    fn nand_edge<'id>(
1901        manager: &Self::Manager<'id>,
1902        lhs: &EdgeOfFunc<'id, Self>,
1903        rhs: &EdgeOfFunc<'id, Self>,
1904    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1905    /// Compute the negated disjunction `lhs ⊽ rhs`, edge version
1906    #[must_use]
1907    fn nor_edge<'id>(
1908        manager: &Self::Manager<'id>,
1909        lhs: &EdgeOfFunc<'id, Self>,
1910        rhs: &EdgeOfFunc<'id, Self>,
1911    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1912    /// Compute the exclusive disjunction `lhs ⊕ rhs`, edge version
1913    #[must_use]
1914    fn xor_edge<'id>(
1915        manager: &Self::Manager<'id>,
1916        lhs: &EdgeOfFunc<'id, Self>,
1917        rhs: &EdgeOfFunc<'id, Self>,
1918    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1919    /// Compute the equivalence `lhs ↔ rhs`, edge version
1920    #[must_use]
1921    fn equiv_edge<'id>(
1922        manager: &Self::Manager<'id>,
1923        lhs: &EdgeOfFunc<'id, Self>,
1924        rhs: &EdgeOfFunc<'id, Self>,
1925    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1926    /// Compute the implication `lhs → rhs`, edge version
1927    #[must_use]
1928    fn imp_edge<'id>(
1929        manager: &Self::Manager<'id>,
1930        lhs: &EdgeOfFunc<'id, Self>,
1931        rhs: &EdgeOfFunc<'id, Self>,
1932    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1933    /// Compute the strict implication `lhs < rhs`, edge version
1934    #[must_use]
1935    fn imp_strict_edge<'id>(
1936        manager: &Self::Manager<'id>,
1937        lhs: &EdgeOfFunc<'id, Self>,
1938        rhs: &EdgeOfFunc<'id, Self>,
1939    ) -> AllocResult<EdgeOfFunc<'id, Self>>;
1940
1941    /// Compute `if self { then_case } else { else_case }`
1942    ///
1943    /// This is equivalent to `(self ∧ then_case) ∨ (¬self ∧ else_case)` but
1944    /// possibly more efficient than computing all the
1945    /// conjunctions/disjunctions.
1946    ///
1947    /// Locking behavior: acquires the manager's lock for shared access.
1948    ///
1949    /// Panics if `self`, `then_case`, and `else_case` don't belong to the same
1950    /// manager.
1951    fn ite(&self, then_case: &Self, else_case: &Self) -> AllocResult<Self> {
1952        self.with_manager_shared(|manager, if_edge| {
1953            let then_edge = then_case.as_edge(manager);
1954            let else_edge = else_case.as_edge(manager);
1955            let res = Self::ite_edge(manager, if_edge, then_edge, else_edge)?;
1956            Ok(Self::from_edge(manager, res))
1957        })
1958    }
1959
1960    /// Compute `if if_edge { then_edge } else { else_edge }` (edge version)
1961    ///
1962    /// This is equivalent to `(self ∧ then_case) ∨ (¬self ∧ else_case)` but
1963    /// possibly more efficient than computing all the
1964    /// conjunctions/disjunctions.
1965    #[must_use]
1966    fn ite_edge<'id>(
1967        manager: &Self::Manager<'id>,
1968        if_edge: &EdgeOfFunc<'id, Self>,
1969        then_edge: &EdgeOfFunc<'id, Self>,
1970        else_edge: &EdgeOfFunc<'id, Self>,
1971    ) -> AllocResult<EdgeOfFunc<'id, Self>> {
1972        let f = EdgeDropGuard::new(manager, Self::and_edge(manager, if_edge, then_edge)?);
1973        let g = EdgeDropGuard::new(manager, Self::imp_strict_edge(manager, if_edge, else_edge)?);
1974        Self::or_edge(manager, &*f, &*g)
1975    }
1976
1977    /// Evaluate this function
1978    ///
1979    /// `args` consists of pairs `(variable, value)` and determines the
1980    /// valuation for all variables in the function's domain. The order is
1981    /// irrelevant (except that if the valuation for a variable is given
1982    /// multiple times, the last value counts).
1983    ///
1984    /// Should there be a decision node for a variable not part of the domain,
1985    /// then `unknown` is used as the decision value.
1986    ///
1987    /// Locking behavior: acquires the manager's lock for shared access.
1988    ///
1989    /// Panics if any variable number in `args` is larger that the number of
1990    /// variables in the containing manager.
1991    fn eval(&self, args: impl IntoIterator<Item = (VarNo, Option<bool>)>) -> Option<bool> {
1992        self.with_manager_shared(|manager, edge| Self::eval_edge(manager, edge, args))
1993    }
1994
1995    /// `Edge` version of [`Self::eval()`]
1996    fn eval_edge<'id>(
1997        manager: &Self::Manager<'id>,
1998        edge: &EdgeOfFunc<'id, Self>,
1999        args: impl IntoIterator<Item = (VarNo, Option<bool>)>,
2000    ) -> Option<bool>;
2001}