taco_bdd/
cudd.rs

1//! BDD interface implementation for [CUDD](https://github.com/ivmai/cudd)
2//!
3//! The bindings to the C library, as well as the build mechanisms are provided
4//! by the `cudd-sys` crate.
5//!
6//! The [`CuddManager`] struct is the manager for the CUDD BDDs and implements
7//! the [`BDDManager`] trait. The [`CuddDD`] struct is the BDD type for CUDD
8//! BDDs and implements the [`BDD`] trait.
9//!
10//! Note that this module uses unsafe code to interact with the CUDD library.
11
12#[cfg(feature = "visualize")]
13use std::{ffi::CString, os::fd::AsRawFd};
14
15#[cfg(feature = "config_deserialize")]
16use serde::Deserialize;
17
18use std::{
19    fmt::{Debug, Display},
20    ptr::null,
21    rc::Rc,
22    sync::Mutex,
23};
24
25use cudd_sys::cudd::{
26    Cudd_CountPathsToNonZero, Cudd_Init, Cudd_Not, Cudd_PrintDebug, Cudd_PrintInfo,
27    Cudd_PrintMinterm, Cudd_Quit, Cudd_ReadLogicZero, Cudd_ReadOne, Cudd_RecursiveDeref, Cudd_Ref,
28    Cudd_bddAnd, Cudd_bddComputeCube, Cudd_bddExistAbstract, Cudd_bddIthVar, Cudd_bddOr,
29    Cudd_bddSwapVariables,
30};
31
32#[cfg(feature = "visualize")]
33use cudd_sys::cudd::Cudd_DumpDot;
34
35// Re-export the CUDD constants
36pub use cudd_sys::cudd::{CUDD_CACHE_SLOTS, CUDD_UNIQUE_SLOTS};
37
38use super::{Bdd, BddManager};
39
40type InternalCuddDD = *mut cudd_sys::DdNode;
41
42/// BDD type for CUDD BDDs
43pub struct CuddDD {
44    mgr: InternalCuddMgr,
45    node: InternalCuddDD,
46}
47
48impl CuddDD {
49    fn new(mgr: InternalCuddMgr, node: InternalCuddDD) -> Self {
50        assert!(!node.is_null());
51
52        unsafe { Cudd_Ref(node) };
53
54        CuddDD { mgr, node }
55    }
56}
57
58impl Clone for CuddDD {
59    fn clone(&self) -> Self {
60        unsafe { Cudd_Ref(self.node) };
61        Self {
62            mgr: self.mgr.clone(),
63            node: self.node,
64        }
65    }
66}
67
68impl Drop for CuddDD {
69    fn drop(&mut self) {
70        assert!(!self.node.is_null());
71        unsafe { Cudd_RecursiveDeref(self.mgr.0, self.node) };
72    }
73}
74
75impl PartialEq for CuddDD {
76    // Two bdds `a` and `b` are equal iff: (a <=> b).is_sat() & !(a <=> b).is_unsat()
77    fn eq(&self, other: &Self) -> bool {
78        let eq = self.equiv(other);
79        eq.satisfiable() && !eq.not().satisfiable()
80    }
81}
82
83impl Debug for CuddDD {
84    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
85        write!(f, "CUDD Debug Info: ")?;
86        unsafe { Cudd_PrintDebug(self.mgr.0, self.node, 0, 10) };
87        write!(f, ", Node Addr: {:#?}", self.node)
88    }
89}
90
91impl Display for CuddDD {
92    fn fmt(&self, _f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
93        unsafe { Cudd_PrintMinterm(self.mgr.0, self.node) };
94        Ok(())
95    }
96}
97
98impl Bdd for CuddDD {
99    fn and(&self, rhs: &Self) -> Self {
100        assert!(self.mgr == rhs.mgr);
101
102        let new_node = unsafe { Cudd_bddAnd(self.mgr.0, self.node, rhs.node) };
103        Self::new(self.mgr.clone(), new_node)
104    }
105
106    fn or(&self, rhs: &Self) -> Self {
107        assert!(self.mgr == rhs.mgr);
108
109        let new_node = unsafe { Cudd_bddOr(self.mgr.0, self.node, rhs.node) };
110        CuddDD::new(self.mgr.clone(), new_node)
111    }
112
113    fn not(&self) -> Self {
114        let new_node = unsafe { Cudd_Not(self.node) };
115        Self::new(self.mgr.clone(), new_node)
116    }
117
118    fn exists<'a, I: IntoIterator<Item = &'a Self>>(&'a self, vars: I) -> Self {
119        let mut vars = vars
120            .into_iter()
121            .map(|dd| {
122                assert!(self.mgr == dd.mgr);
123                dd.node
124            })
125            .collect::<Vec<_>>();
126
127        let cube = unsafe {
128            Cudd_bddComputeCube(
129                self.mgr.0,
130                vars.as_mut_ptr(),
131                null::<i32>() as _,
132                vars.len() as _,
133            )
134        };
135        let cube = CuddDD::new(self.mgr.clone(), cube);
136
137        let exist_node = unsafe { Cudd_bddExistAbstract(self.mgr.0, self.node, cube.node) };
138        CuddDD::new(self.mgr.clone(), exist_node)
139    }
140
141    fn satisfiable(&self) -> bool {
142        let n = unsafe { Cudd_CountPathsToNonZero(self.node) };
143        n > 0.0
144    }
145
146    fn implies(&self, other: &Self) -> Self {
147        // no built in support, construct manually
148        (self.not()).or(other)
149    }
150
151    fn equiv(&self, other: &Self) -> Self {
152        // no built in support, construct manually
153        (self.and(other)).or(&self.not().and(&other.not()))
154    }
155
156    fn swap<'a, I: IntoIterator<Item = &'a Self>>(&'a self, from: I, to: I) -> Self {
157        let mut from = from
158            .into_iter()
159            .map(|dd| {
160                assert!(dd.mgr == self.mgr);
161                dd.node
162            })
163            .collect::<Vec<_>>();
164
165        let mut to = to
166            .into_iter()
167            .map(|bdd| {
168                assert!(bdd.mgr == self.mgr);
169                bdd.node
170            })
171            .collect::<Vec<_>>();
172
173        assert!(to.len() == from.len(), "Invalid permutation handed to CUDD");
174
175        let new_node = unsafe {
176            Cudd_bddSwapVariables(
177                self.mgr.0,
178                self.node,
179                from.as_mut_ptr(),
180                to.as_mut_ptr(),
181                from.len() as _,
182            )
183        };
184
185        CuddDD::new(self.mgr.clone(), new_node)
186    }
187}
188
189/// Internal Handler around the pointer to the CUDD Manager object
190#[derive(PartialEq)]
191struct InternalCuddMgrPtr(*mut cudd_sys::DdManager);
192
193impl InternalCuddMgrPtr {
194    /// Create a new CUDD manager with default configuration
195    fn new() -> Self {
196        Self::new_with_config(&CuddManagerConfig::default())
197    }
198
199    /// Create a new CUDD manager with the given configuration
200    fn new_with_config(config: &CuddManagerConfig) -> Self {
201        let mgr = unsafe {
202            Cudd_Init(
203                config.num_vars as _,
204                config.num_vars_z as _,
205                config.num_slots as _,
206                config.cache_slots as _,
207                config.max_memory as _,
208            )
209        };
210
211        assert!(!mgr.is_null(), "Failed to create CUDD Manager");
212
213        // enable reordering
214        let reorder_method = config.reorder_method.into();
215        unsafe { cudd_sys::cudd::Cudd_AutodynEnable(mgr, reorder_method) };
216
217        InternalCuddMgrPtr(mgr)
218    }
219}
220
221// Quit the actual CUDD manager when the `InternalCuddMgrPtr` is dropped
222impl Drop for InternalCuddMgrPtr {
223    fn drop(&mut self) {
224        unsafe { Cudd_Quit(self.0) };
225    }
226}
227
228/// Internal representation of the CUDD manager
229type InternalCuddMgr = Rc<InternalCuddMgrPtr>;
230
231/// Configuration for the CUDD manager
232///
233/// The documentation for these struct values has been taken from the CUDD user's manual
234///
235/// See for example <http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/node3.html>
236#[derive(Debug, Clone, PartialEq)]
237#[cfg_attr(feature = "config_deserialize", derive(Deserialize))]
238pub struct CuddManagerConfig {
239    /// It is the initial number of variables for BDDs and ADDs. If the total number of variables needed by the application is known, then it is slightly more efficient to create a manager with that number of variables. If the number is unknown, it can be set to 0, or to any other lower bound on the number of variables. Requesting more variables than are actually needed is not incorrect, but is not efficient.
240    /// Default value: 0
241    #[cfg_attr(feature = "config_deserialize", serde(default = "default_num_vars"))]
242    pub num_vars: usize,
243    /// It is the initial number of variables for ZDDs.
244    /// Default value: 0
245    #[cfg_attr(feature = "config_deserialize", serde(default = "default_num_vars_z"))]
246    pub num_vars_z: usize,
247    /// Determines the initial size of each subtable of the unique table. There is a subtable for each variable. The size of each subtable is dynamically adjusted to reflect the number of nodes. It is normally O.K. to use the default value for this parameter, which is CUDD_UNIQUE_SLOTS.
248    /// Default value: `CUDD_UNIQUE_SLOTS`.
249    #[cfg_attr(feature = "config_deserialize", serde(default = "default_num_slots"))]
250    pub num_slots: usize,
251    /// It is the initial size (number of entries) of the cache.  
252    /// Default value: `CUDD_CACHE_SLOTS`.
253    #[cfg_attr(feature = "config_deserialize", serde(default = "default_cache_slots"))]
254    pub cache_slots: usize,
255    /// It is the target value for the maximum memory occupation (in bytes). The package uses this value to decide two parameters.
256    ///     - the maximum size to which the cache will grow, regardless of the hit rate or the size of the unique table.  
257    ///     - the maximum size to which growth of the unique table will be preferred to garbage collection.
258    /// Default value: 0
259    #[cfg_attr(feature = "config_deserialize", serde(default = "default_max_memory"))]
260    pub max_memory: usize,
261    /// Reordering method to be used by the CUDD manager
262    /// Default value: `CuddReorderMethod::Sift`
263    #[cfg_attr(
264        feature = "config_deserialize",
265        serde(default = "default_reorder_method")
266    )]
267    pub reorder_method: CuddReorderMethod,
268}
269
270/// Function to get default num vars for the CUDD manager
271fn default_num_vars() -> usize {
272    0
273}
274
275/// Function to get default num vars for the CUDD manager
276fn default_num_vars_z() -> usize {
277    0
278}
279
280/// Function to get default num slots for the CUDD manager
281fn default_num_slots() -> usize {
282    CUDD_UNIQUE_SLOTS as usize
283}
284/// Function to get default cache slots for the CUDD manager
285fn default_cache_slots() -> usize {
286    CUDD_CACHE_SLOTS as usize
287}
288
289/// Function to get default max memory for the CUDD manager
290fn default_max_memory() -> usize {
291    0
292}
293
294/// Function to get default reordering method for the CUDD manager
295fn default_reorder_method() -> CuddReorderMethod {
296    CuddReorderMethod::Sift
297}
298
299impl Default for CuddManagerConfig {
300    fn default() -> Self {
301        Self {
302            num_vars: default_num_vars(),
303            num_vars_z: default_num_vars_z(),
304            num_slots: default_num_slots(),
305            cache_slots: default_cache_slots(),
306            max_memory: default_max_memory(),
307            reorder_method: default_reorder_method(),
308        }
309    }
310}
311
312/// Dynamic reordering methods supported by the CUDD manager
313///
314/// The documentation for these enum values has been taken from the CUDD user's manual
315///
316/// See for example <http://web.mit.edu/sage/export/tmp/y/usr/share/doc/polybori/cudd/node3.html>
317#[derive(Debug, Clone, Copy, PartialEq)]
318#[cfg_attr(feature = "config_deserialize", derive(Deserialize))]
319pub enum CuddReorderMethod {
320    /// Disable reordering in the CUDD library
321    Disabled,
322    /// `CUDD_REORDER_RANDOM`
323    Random,
324    /// `CUDD_REORDER_RANDOM_PIVOT`
325    RandomPivot,
326    /// `CUDD_REORDER_SIFT`
327    Sift,
328    /// `CUDD_REORDER_SIFT_CONVERGE`
329    SiftConverge,
330    /// `CUDD_REORDER_SYMM_SIFT`
331    SymmSift,
332    /// `CUDD_REORDER_SYMM_SIFT_CONV`
333    SymmSiftConverge,
334    /// `CUDD_REORDER_WINDOW2`
335    Window2,
336    /// `CUDD_REORDER_WINDOW3`
337    Window3,
338    /// `CUDD_REORDER_WINDOW4`
339    Window4,
340    /// `CUDD_REORDER_WINDOW2_CONV`
341    Window2Converge,
342    /// `CUDD_REORDER_WINDOW3_CONV`
343    Window3Converge,
344    /// `CUDD_REORDER_WINDOW4_CONV`
345    Window4Converge,
346    /// `CUDD_REORDER_ANNEALING`
347    Annealing,
348    /// `CUDD_REORDER_GENETIC`
349    Genetic,
350    /// `CUDD_REORDER_EXACT`
351    Exact,
352}
353
354impl From<CuddReorderMethod> for cudd_sys::cudd::Cudd_ReorderingType {
355    fn from(val: CuddReorderMethod) -> cudd_sys::cudd::Cudd_ReorderingType {
356        match val {
357            CuddReorderMethod::Disabled => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_NONE,
358            CuddReorderMethod::Random => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_RANDOM,
359            CuddReorderMethod::RandomPivot => {
360                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_RANDOM_PIVOT
361            }
362            CuddReorderMethod::Sift => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_SIFT,
363            CuddReorderMethod::SiftConverge => {
364                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_SIFT_CONVERGE
365            }
366            CuddReorderMethod::SymmSift => {
367                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_SYMM_SIFT
368            }
369            CuddReorderMethod::SymmSiftConverge => {
370                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_SYMM_SIFT_CONV
371            }
372            CuddReorderMethod::Window2 => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_WINDOW2,
373            CuddReorderMethod::Window3 => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_WINDOW3,
374            CuddReorderMethod::Window4 => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_WINDOW4,
375            CuddReorderMethod::Window2Converge => {
376                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_WINDOW2_CONV
377            }
378            CuddReorderMethod::Window3Converge => {
379                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_WINDOW3_CONV
380            }
381            CuddReorderMethod::Window4Converge => {
382                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_WINDOW4_CONV
383            }
384            CuddReorderMethod::Annealing => {
385                cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_ANNEALING
386            }
387            CuddReorderMethod::Genetic => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_GENETIC,
388            CuddReorderMethod::Exact => cudd_sys::cudd::Cudd_ReorderingType::CUDD_REORDER_EXACT,
389        }
390    }
391}
392
393/// Manager type for CUDD Decision Diagrams
394///
395/// This manager internally uses the [CUDD](https://github.com/ivmai/cudd)
396/// library to create and manipulate BDDs.
397///
398/// Note that this manager uses unsafe code to interact with the CUDD library.
399pub struct CuddManager {
400    /// CUDD manager object
401    mgr: InternalCuddMgr,
402    /// Index of the next variable to be created
403    next_var_index: Rc<Mutex<usize>>,
404}
405
406impl CuddManager {
407    pub fn new() -> Self {
408        let mgr = InternalCuddMgrPtr::new();
409
410        CuddManager {
411            mgr: Rc::new(mgr),
412            next_var_index: Rc::new(Mutex::new(0)),
413        }
414    }
415
416    pub fn new_with_config(cfg: &CuddManagerConfig) -> Self {
417        let mgr = InternalCuddMgrPtr::new_with_config(cfg);
418
419        CuddManager {
420            mgr: Rc::new(mgr),
421            next_var_index: Rc::new(Mutex::new(0)),
422        }
423    }
424}
425
426impl Default for CuddManager {
427    fn default() -> Self {
428        Self::new()
429    }
430}
431
432impl Clone for CuddManager {
433    /// Clone of a CUDD manager creates a shallow copy of the manager
434    ///
435    /// It does therefore not clone the CUDD manager itself, all modifications
436    /// to the manager and BDDs will be reflected in all clones.
437    fn clone(&self) -> Self {
438        CuddManager {
439            mgr: Rc::clone(&self.mgr),
440            next_var_index: Rc::clone(&self.next_var_index),
441        }
442    }
443}
444
445impl PartialEq for CuddManager {
446    /// Two CUDD managers are equal if they share the same CUDD manager object
447    fn eq(&self, other: &Self) -> bool {
448        self.mgr == other.mgr
449    }
450}
451
452impl Debug for CuddManager {
453    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
454        writeln!(f, "CUDD manager Info: ")?;
455        unsafe { Cudd_PrintInfo(self.mgr.0, libc_stdhandle::stdout()) };
456        writeln!(
457            f,
458            "Mgr Addr: {:#?}, Number of variables: {}",
459            self.mgr.0,
460            self.next_var_index.lock().unwrap()
461        )
462    }
463}
464
465impl BddManager for CuddManager {
466    type DD = CuddDD;
467
468    fn new_var(&mut self) -> Self::DD {
469        let mut index = self.next_var_index.lock().unwrap();
470        let new_node = unsafe { Cudd_bddIthVar(self.mgr.0, *index as i32) };
471        *index += 1;
472
473        CuddDD::new(self.mgr.clone(), new_node)
474    }
475
476    fn get_bdd_false(&self) -> Self::DD {
477        let new_node = unsafe { Cudd_ReadLogicZero(self.mgr.0) };
478
479        CuddDD::new(self.mgr.clone(), new_node)
480    }
481
482    fn get_bdd_true(&self) -> Self::DD {
483        let new_node = unsafe { Cudd_ReadOne(self.mgr.0) };
484
485        CuddDD::new(self.mgr.clone(), new_node)
486    }
487
488    #[cfg(feature = "visualize")]
489    fn dump_dot<'a, VN, BN>(
490        &'a self,
491        file: std::fs::File,
492        bdd_names: impl IntoIterator<Item = (&'a Self::DD, BN)>,
493        variable_names: impl IntoIterator<Item = (&'a Self::DD, VN)>,
494    ) -> std::io::Result<()>
495    where
496        VN: std::fmt::Display + Clone,
497        BN: std::fmt::Display,
498    {
499        let res;
500        let (bdds_to_be_dumped, bdd_names) = bdd_names
501            .into_iter()
502            .map(|(dd, dn)| (dd.node, CString::new(dn.to_string()).unwrap()))
503            .collect::<(Vec<_>, Vec<_>)>();
504
505        let variable_names = variable_names
506            .into_iter()
507            .map(|(_, vn)| CString::new(vn.to_string()).unwrap())
508            .collect::<Vec<_>>();
509
510        if variable_names.len() < *self.next_var_index.lock().unwrap() && !variable_names.is_empty()
511        {
512            return Err(std::io::Error::other(
513                "Number of variable names does not match number of variables! Aborting as this will lead to a segfault",
514            ));
515        }
516
517        unsafe {
518            let file = libc::fdopen(file.as_raw_fd(), "w".as_ptr() as _);
519
520            let bdd_names = bdd_names
521                .into_iter()
522                .map(|n| n.into_raw())
523                .collect::<Vec<_>>();
524
525            let mut var_names_ptr = null();
526
527            let var_names = variable_names
528                .into_iter()
529                .map(|n| n.into_raw())
530                .collect::<Vec<_>>();
531
532            if !var_names.is_empty() {
533                var_names_ptr = var_names.as_ptr() as *const *const i8;
534            }
535
536            res = Cudd_DumpDot(
537                self.mgr.0,
538                bdds_to_be_dumped.len() as i32,
539                bdds_to_be_dumped.as_ptr() as *mut *mut cudd_sys::DdNode,
540                var_names_ptr,
541                bdd_names.as_ptr() as *const *const i8,
542                file,
543            );
544
545            libc::fflush(file);
546
547            let _ = var_names.into_iter().map(|p| CString::from_raw(p));
548            let _ = bdd_names.into_iter().map(|p| CString::from_raw(p));
549        };
550
551        if res == 1 {
552            Ok(())
553        } else {
554            Err(std::io::Error::other("Failed to dump DOT file"))
555        }
556    }
557}
558
559#[cfg(test)]
560mod test {
561    use crate::{
562        BddManager,
563        bdd_test_utils::{self, test_mgr_eq_and_clone},
564    };
565
566    use super::{CuddManager, CuddManagerConfig, CuddReorderMethod};
567
568    #[test]
569    fn test_mgr_eq() {
570        let mgr1 = CuddManager::default();
571        let mgr2 = CuddManager::default();
572
573        test_mgr_eq_and_clone(mgr1, mgr2);
574    }
575
576    #[test]
577    fn test_mgr_get() {
578        let mgr = CuddManager::default();
579        bdd_test_utils::test_mgr_get(mgr)
580    }
581
582    #[test]
583    fn test_not() {
584        let mgr = CuddManager::default();
585        bdd_test_utils::test_not(mgr)
586    }
587
588    #[test]
589    fn test_and() {
590        let mgr = CuddManager::default();
591        bdd_test_utils::test_and(mgr)
592    }
593
594    #[test]
595    fn test_or() {
596        let mgr = CuddManager::default();
597        bdd_test_utils::test_or(mgr)
598    }
599
600    #[test]
601    fn test_exists() {
602        let mgr = CuddManager::default();
603        bdd_test_utils::test_exists(mgr)
604    }
605
606    #[test]
607    fn test_implies() {
608        let mgr = CuddManager::default();
609        bdd_test_utils::test_implies(mgr)
610    }
611
612    #[test]
613    fn test_equiv() {
614        let mgr = CuddManager::default();
615        bdd_test_utils::test_equiv(mgr)
616    }
617
618    #[test]
619    fn test_swap() {
620        let mgr = CuddManager::default();
621        bdd_test_utils::test_swap(mgr)
622    }
623
624    #[test]
625    fn test_manager_with_custom_config() {
626        let cfg = CuddManagerConfig {
627            num_vars: 10,
628            num_vars_z: 0,
629            num_slots: 1000,
630            cache_slots: 1000,
631            max_memory: 0,
632            reorder_method: CuddReorderMethod::Disabled,
633        };
634
635        let mgr = CuddManager::new_with_config(&cfg);
636
637        bdd_test_utils::test_mgr_get(mgr.clone());
638        bdd_test_utils::test_not(mgr.clone());
639        bdd_test_utils::test_and(mgr.clone());
640        bdd_test_utils::test_or(mgr.clone());
641        bdd_test_utils::test_exists(mgr.clone());
642    }
643
644    #[test]
645    #[should_panic]
646    fn test_panic_on_bdd_of_mixed_mgrs() {
647        let mgr1 = CuddManager::default();
648        let mgr2 = CuddManager::default();
649        bdd_test_utils::panic_on_bdd_of_mixed_mgrs(mgr1, mgr2)
650    }
651
652    #[test]
653    fn print_funcs_work() {
654        let mut mgr = CuddManager::new();
655        let v = mgr.new_var();
656
657        println!("Var: {v}, Debug: {v:?}");
658        println!("Mgr Debug: {mgr:?}");
659    }
660
661    #[cfg(feature = "visualize")]
662    #[test]
663    fn test_abort_if_not_enough_var_names() {
664        let mut mgr = CuddManager::default();
665        let bdd1 = mgr.new_var();
666        let _ = mgr.new_var();
667
668        let file = std::fs::File::create("test.dot").unwrap();
669
670        let res = mgr.dump_dot(file, vec![(&bdd1, "BDD1")], vec![(&bdd1, "Var1")]);
671
672        assert!(res.is_err());
673    }
674}
taco_bdd/cudd.rs

taco_bdd/
cudd.rs
