taco_bdd/
oxidd.rs

1//! This module implements the BDD trait for the
2//! [OxiDD](https://github.com/OxiDD/oxidd) library
3//!
4//! TODO: With the release of oxidd v0.0.11 the API has changed significantly,
5//! for now everything has only been fixed to "work", but there is a lot of room
6//! for improvement.
7
8use oxidd::{
9    BooleanFunction, BooleanFunctionQuant, FunctionSubst, Manager, ManagerRef, Subst,
10    bdd::{BDDFunction, BDDManagerRef},
11};
12use std::{fmt::Debug, rc::Rc, sync::Mutex};
13
14use super::{Bdd, BddManager};
15
16#[cfg(feature = "config_deserialize")]
17use serde::Deserialize;
18
19/// Maximum number of nodes in the BDD manager
20/// Exceeding this limit will cause the manager to panic
21const INNER_NODE_CAPACITY: usize = 1 << 20;
22/// Maximum number of nodes in the apply cache
23const APPLY_CACHE_CAPACITY: usize = 1024;
24/// Number of threads used for parallel operations
25const THREADS: u32 = 8;
26
27/// BDD type for OxiDD BDDs
28#[derive(Clone)]
29pub struct OxiDD {
30    /// BDD representation of the variable
31    bdd: oxidd::bdd::BDDFunction,
32    /// If the BDD is a variable, contains the variable id
33    var_id: Option<u32>,
34}
35
36impl Debug for OxiDD {
37    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
38        write!(f, "OxiDD does not support prints")
39    }
40}
41
42impl Bdd for OxiDD {
43    fn not(&self) -> Self {
44        OxiDD {
45            bdd: self
46                .bdd
47                .not()
48                .expect("OxiDD ran out of memory. Consider trying again with increased capacity"),
49            var_id: None,
50        }
51    }
52
53    fn and(&self, rhs: &Self) -> Self {
54        OxiDD {
55            bdd: self
56                .bdd
57                .and(&rhs.bdd)
58                .expect("OxiDD ran out of memory. Consider trying again with increased capacity"),
59            var_id: None,
60        }
61    }
62
63    fn or(&self, rhs: &Self) -> Self {
64        OxiDD {
65            bdd: self
66                .bdd
67                .or(&rhs.bdd)
68                .expect("OxiDD ran out of memory. Consider trying again with increased capacity"),
69            var_id: None,
70        }
71    }
72
73    fn exists<'a, I: IntoIterator<Item = &'a Self>>(&'a self, vars: I) -> Self {
74        let mut vars = vars.into_iter().map(|dd| dd.bdd.clone());
75
76        let first = vars.next();
77        if first.is_none() {
78            panic!("No variable for existential quantification");
79        }
80        let first =
81            first.expect("OxiDD ran out of memory. Consider trying again with increased capacity");
82
83        let vars = vars.fold(first, |acc, x| {
84            acc.and(&x)
85                .expect("OxiDD ran out of memory. Consider trying again with increased capacity")
86        });
87
88        OxiDD {
89            bdd: self
90                .bdd
91                .exists(&vars)
92                .expect("OxiDD ran out of memory. Consider trying again with increased capacity"),
93            var_id: None,
94        }
95    }
96
97    fn satisfiable(&self) -> bool {
98        self.bdd.satisfiable()
99    }
100
101    fn implies(&self, rhs: &Self) -> Self {
102        OxiDD {
103            bdd: self
104                .bdd
105                .imp(&rhs.bdd)
106                .expect("OxiDD ran out of memory. Consider trying again with increased capacity"),
107            var_id: None,
108        }
109    }
110
111    fn equiv(&self, rhs: &Self) -> Self {
112        OxiDD {
113            bdd: self
114                .bdd
115                .equiv(&rhs.bdd)
116                .expect("OxiDD ran out of memory. Consider trying again with increased capacity"),
117            var_id: None,
118        }
119    }
120
121    fn swap<'a, I: IntoIterator<Item = &'a Self>>(&'a self, from: I, to: I) -> Self {
122        let mut vars = Vec::new();
123        let mut replacements = Vec::new();
124
125        from.into_iter().zip(to).for_each(|(from, to)| {
126            let var_id_from = from.var_id.expect("Substitution not on variable");
127
128            vars.push(var_id_from);
129            replacements.push(to.bdd.clone());
130
131            let var_id_to = to.var_id.expect("Substitution not on variable");
132            vars.push(var_id_to);
133            replacements.push(from.bdd.clone());
134        });
135
136        let subs = Subst::new(vars, replacements);
137        let bdd = self
138            .bdd
139            .substitute(&subs)
140            .expect("OxiDD ran out of memory. Consider trying again with increased capacity");
141
142        OxiDD { bdd, var_id: None }
143    }
144}
145
146impl PartialEq for OxiDD {
147    // We consider two bdds `a` and `b` are equal  if they are equivalent, i.e.,
148    // iff: (a <=> b).is_sat() & !(a <=> b).is_unsat()
149    fn eq(&self, other: &Self) -> bool {
150        let equiv = self.equiv(other);
151        let equiv_sat = equiv.satisfiable();
152        let n_equiv_unsat = !equiv.not().satisfiable();
153        equiv_sat && n_equiv_unsat
154    }
155}
156
157/// Configuration for the OxiDD BDD manager
158///
159/// See <https://docs.rs/oxidd/latest/oxidd/bdd/fn.new_manager.html>
160#[derive(Debug, Clone, PartialEq)]
161#[cfg_attr(feature = "config_deserialize", derive(Deserialize))]
162pub struct OxiddManagerConfig {
163    #[cfg_attr(
164        feature = "config_deserialize",
165        serde(default = "default_inner_node_capacity")
166    )]
167    pub inner_node_capacity: usize,
168    #[cfg_attr(
169        feature = "config_deserialize",
170        serde(default = "default_apply_cache_capacity")
171    )]
172    pub apply_cache_capacity: usize,
173    #[cfg_attr(feature = "config_deserialize", serde(default = "default_threads"))]
174    pub threads: u32,
175}
176
177/// Function to get default inner node capacity for the BDD manager
178fn default_inner_node_capacity() -> usize {
179    INNER_NODE_CAPACITY
180}
181
182/// Function to get default apply cache capacity for the BDD manager
183fn default_apply_cache_capacity() -> usize {
184    APPLY_CACHE_CAPACITY
185}
186
187/// Function to get default number of threads for the BDD manager
188fn default_threads() -> u32 {
189    THREADS
190}
191
192impl Default for OxiddManagerConfig {
193    fn default() -> Self {
194        Self {
195            inner_node_capacity: default_inner_node_capacity(),
196            apply_cache_capacity: default_apply_cache_capacity(),
197            threads: default_threads(),
198        }
199    }
200}
201
202/// BDD manager for OxiDD BDDs
203///
204/// This manager is a wrapper around the OxiDD BDD manager. It panics if the BDD
205/// manager runs out of memory.
206///
207/// By default the manager is configured to have a maximum of 2^30 nodes and 2^10
208/// nodes in the apply cache.
209#[derive(Clone)]
210pub struct OxiddManager {
211    /// Reference to the manager
212    mgr: BDDManagerRef,
213    /// Index of the next variable to be created
214    next_var_index: Rc<Mutex<u32>>,
215}
216
217impl PartialEq for OxiddManager {
218    /// Compare based on the manager objects
219    fn eq(&self, other: &Self) -> bool {
220        self.mgr == other.mgr
221    }
222}
223
224impl OxiddManager {
225    /// Create a new Oxidd BDD manager with default configuration
226    ///
227    /// This manager internally uses the
228    /// [OxiDD BDD library](https://github.com/OxiDD/oxidd/tree/main)
229    /// to create and manipulate BDDs.
230    ///
231    /// This manager panics if it runs out of memory. By default the manager is
232    /// configured to have a maximum of 2^30 nodes and 2^10 nodes in the apply
233    /// cache.
234    pub fn new() -> Self {
235        Self {
236            mgr: oxidd::bdd::new_manager(INNER_NODE_CAPACITY, APPLY_CACHE_CAPACITY, THREADS),
237            next_var_index: Rc::new(Mutex::new(0)),
238        }
239    }
240
241    /// Create a new Oxidd BDD manager with custom configuration
242    pub fn new_with_config(config: &OxiddManagerConfig) -> Self {
243        Self {
244            mgr: oxidd::bdd::new_manager(
245                config.inner_node_capacity,
246                config.apply_cache_capacity,
247                config.threads,
248            ),
249            next_var_index: Rc::new(Mutex::new(0)),
250        }
251    }
252}
253
254impl Default for OxiddManager {
255    fn default() -> Self {
256        Self::new()
257    }
258}
259
260impl Debug for OxiddManager {
261    fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
262        oxidd::bdd::print_stats();
263        Ok(())
264    }
265}
266
267impl BddManager for OxiddManager {
268    type DD = OxiDD;
269
270    fn new_var(&mut self) -> Self::DD {
271        let mut index = self.next_var_index.lock().unwrap();
272        let new_var_index = *index;
273        *index += 1;
274
275        let inner = self.mgr.with_manager_exclusive(|mgr| {
276            mgr.add_named_vars([new_var_index.to_string()])
277                .expect("OxiDD ran out of memory. Consider trying again with increased capacity");
278
279            BDDFunction::var(mgr, new_var_index)
280                .expect("OxiDD ran out of memory. Consider trying again with increased capacity")
281        });
282        OxiDD {
283            bdd: inner,
284            var_id: Some(new_var_index),
285        }
286    }
287
288    fn get_bdd_false(&self) -> Self::DD {
289        let inner = self.mgr.with_manager_exclusive(|mgr| BDDFunction::f(mgr));
290        OxiDD {
291            bdd: inner,
292            var_id: None,
293        }
294    }
295
296    fn get_bdd_true(&self) -> Self::DD {
297        let inner = self.mgr.with_manager_exclusive(|mgr| BDDFunction::t(mgr));
298        OxiDD {
299            bdd: inner,
300            var_id: None,
301        }
302    }
303
304    #[cfg(feature = "visualize")]
305    fn dump_dot<'a, VN, BD>(
306        &'a self,
307        file: std::fs::File,
308        _bdds: impl IntoIterator<Item = (&'a Self::DD, BD)>,
309        var_name: impl IntoIterator<Item = (&'a Self::DD, VN)>,
310    ) -> std::io::Result<()>
311    where
312        VN: std::fmt::Display + Clone,
313        BD: std::fmt::Display,
314    {
315        self.mgr.with_manager_shared(|manager| {
316            let var_name = var_name.into_iter().map(|(dd, vn)| (&dd.bdd, vn));
317
318            oxidd_dump::dot::dump_all(file, manager, var_name)
319        })
320    }
321}
322
323#[cfg(test)]
324mod test {
325    use crate::{
326        BddManager,
327        bdd_test_utils::{self, test_mgr_eq_and_clone},
328    };
329
330    use super::OxiddManager;
331
332    #[test]
333    fn test_mgr_eq() {
334        let mgr1 = OxiddManager::default();
335        let mgr2 = OxiddManager::default();
336
337        test_mgr_eq_and_clone(mgr1, mgr2);
338    }
339
340    #[test]
341    fn test_mgr_get() {
342        let mgr = OxiddManager::default();
343        bdd_test_utils::test_mgr_get(mgr)
344    }
345
346    #[test]
347    fn test_not() {
348        let mgr = OxiddManager::default();
349        bdd_test_utils::test_not(mgr)
350    }
351
352    #[test]
353    fn test_and() {
354        let mgr = OxiddManager::default();
355        bdd_test_utils::test_and(mgr)
356    }
357
358    #[test]
359    fn test_or() {
360        let mgr = OxiddManager::default();
361        bdd_test_utils::test_or(mgr)
362    }
363
364    #[test]
365    fn test_exists() {
366        let mgr = OxiddManager::default();
367        bdd_test_utils::test_exists(mgr)
368    }
369
370    #[test]
371    fn test_implies() {
372        let mgr = OxiddManager::default();
373        bdd_test_utils::test_implies(mgr)
374    }
375
376    #[test]
377    fn test_equiv() {
378        let mgr = OxiddManager::default();
379        bdd_test_utils::test_equiv(mgr)
380    }
381
382    #[test]
383    fn test_swap() {
384        let mgr = OxiddManager::default();
385        bdd_test_utils::test_swap(mgr)
386    }
387
388    #[test]
389    #[should_panic]
390    fn test_panic_on_bdd_of_mixed_mgrs() {
391        let mgr1 = OxiddManager::default();
392        let mgr2 = OxiddManager::default();
393        bdd_test_utils::panic_on_bdd_of_mixed_mgrs(mgr1, mgr2)
394    }
395
396    #[test]
397    fn print_funcs_work() {
398        let mut mgr = OxiddManager::new();
399        let v = mgr.new_var();
400
401        println!("Debug: {v:?}");
402        println!("Mgr Debug: {mgr:?}");
403    }
404}
taco_bdd/oxidd.rs

taco_bdd/
oxidd.rs
