rsdd/builder/bdd/
mod.rs

1use crate::repr::BddPtr;
2use std::cmp::Ordering;
3
4mod builder;
5mod robdd;
6mod stats;
7
8pub use self::builder::*;
9pub use self::robdd::*;
10pub use self::stats::*;
11
12// TODO: move this to a compile module
13
14#[derive(Eq, PartialEq, Debug)]
15struct CompiledCNF<'a> {
16    ptr: BddPtr<'a>,
17    sz: usize,
18}
19
20// The priority queue depends on `Ord`.
21// Explicitly implement the trait so the queue becomes a min-heap
22// instead of a max-heap.
23impl<'a> Ord for CompiledCNF<'a> {
24    fn cmp(&self, other: &Self) -> Ordering {
25        // Notice that the we flip the ordering on costs.
26        // In case of a tie we compare positions - this step is necessary
27        // to make implementations of `PartialEq` and `Ord` consistent.
28        other.sz.cmp(&self.sz)
29    }
30}
31
32// `PartialOrd` needs to be implemented as well.
33impl<'a> PartialOrd for CompiledCNF<'a> {
34    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
35        Some(self.cmp(other))
36    }
37}