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}