oxidd/
zbdd.rs

1//! Zero-suppressed binary decision diagrams (ZBDDs)
2
3#[allow(unused)] // unused in case no manager impl is selected
4macro_rules! manager_data {
5    ($name:ident for $dd:ident, operator: $op:ty, cache_max_arity: $arity:expr) => {
6        #[derive(::oxidd_derive::ManagerEventSubscriber)]
7        #[subscribe(manager = <$dd as $crate::util::type_cons::DD>::Manager<'id>, no_trait_bounds)]
8        pub struct $name<'id> {
9            apply_cache: $crate::util::apply_cache::ApplyCache<
10                <$dd as $crate::util::type_cons::DD>::Manager<'id>,
11                $op,
12                $arity,
13            >,
14            zbdd_cache:
15                ::oxidd_rules_zbdd::ZBDDCache<<$dd as $crate::util::type_cons::DD>::Edge<'id>>,
16        }
17
18        impl<'id> $name<'id> {
19            /// SAFETY: The manager data must only be used inside a manager that
20            /// guarantees all node deletions to be wrapped inside a
21            /// [`oxidd_core::ApplyCache::pre_gc()`] /
22            /// [`oxidd_core::ApplyCache::post_gc()`]
23            /// pair for the contained apply cache.
24            unsafe fn new(apply_cache_capacity: usize) -> Self {
25                Self {
26                    // SAFETY: see above
27                    apply_cache: unsafe {
28                        $crate::util::apply_cache::new_apply_cache(apply_cache_capacity)
29                    },
30                    zbdd_cache: ::oxidd_rules_zbdd::ZBDDCache::new(),
31                }
32            }
33        }
34
35        impl<'id> ::oxidd_core::util::DropWith<<$dd as $crate::util::type_cons::DD>::Edge<'id>>
36            for $name<'id>
37        {
38            fn drop_with(
39                self,
40                drop_edge: impl Fn(<$dd as $crate::util::type_cons::DD>::Edge<'id>),
41            ) {
42                self.apply_cache.drop_with(&drop_edge);
43                self.zbdd_cache.drop_with(drop_edge);
44            }
45        }
46
47        impl<'id>
48            ::oxidd_core::HasApplyCache<<$dd as $crate::util::type_cons::DD>::Manager<'id>, $op>
49            for $name<'id>
50        {
51            type ApplyCache = $crate::util::apply_cache::ApplyCache<
52                <$dd as $crate::util::type_cons::DD>::Manager<'id>,
53                $op,
54                $arity,
55            >;
56
57            #[inline]
58            fn apply_cache(&self) -> &Self::ApplyCache {
59                &self.apply_cache
60            }
61
62            #[inline]
63            fn apply_cache_mut(&mut self) -> &mut Self::ApplyCache {
64                &mut self.apply_cache
65            }
66        }
67
68        impl<'id>
69            AsRef<::oxidd_rules_zbdd::ZBDDCache<<$dd as $crate::util::type_cons::DD>::Edge<'id>>>
70            for $name<'id>
71        {
72            #[inline(always)]
73            fn as_ref(
74                &self,
75            ) -> &::oxidd_rules_zbdd::ZBDDCache<<$dd as $crate::util::type_cons::DD>::Edge<'id>>
76            {
77                &self.zbdd_cache
78            }
79        }
80        impl<'id>
81            AsMut<::oxidd_rules_zbdd::ZBDDCache<<$dd as $crate::util::type_cons::DD>::Edge<'id>>>
82            for $name<'id>
83        {
84            #[inline(always)]
85            fn as_mut(
86                &mut self,
87            ) -> &mut ::oxidd_rules_zbdd::ZBDDCache<<$dd as $crate::util::type_cons::DD>::Edge<'id>>
88            {
89                &mut self.zbdd_cache
90            }
91        }
92    };
93}
94
95cfg_if::cfg_if! {
96    if #[cfg(feature = "manager-pointer")] {
97        pub use pointer::{ZBDDFunction, ZBDDManagerRef};
98    } else if #[cfg(feature = "manager-index")] {
99        pub use index::{ZBDDFunction, ZBDDManagerRef};
100    } else {
101        pub type ZBDDFunction = ();
102        pub type ZBDDManagerRef = ();
103    }
104}
105
106#[allow(missing_docs)]
107#[deprecated = "use ZBDDFunction instead"]
108pub type ZBDDSet = ZBDDFunction;
109
110/// Create a new manager for a simple binary decision diagram
111#[allow(unused_variables)]
112pub fn new_manager(
113    inner_node_capacity: usize,
114    apply_cache_capacity: usize,
115    threads: u32,
116) -> ZBDDManagerRef {
117    cfg_if::cfg_if! {
118        if #[cfg(feature = "manager-pointer")] {
119            pointer::ZBDDManagerRef::new_manager(inner_node_capacity, apply_cache_capacity, threads)
120        } else if #[cfg(feature = "manager-index")] {
121            index::ZBDDManagerRef::new_manager(inner_node_capacity, 2, apply_cache_capacity, threads)
122        } else {
123            unreachable!()
124        }
125    }
126}
127
128/// Print statistics to stderr
129pub fn print_stats() {
130    #[cfg(not(feature = "statistics"))]
131    eprintln!("[statistics feature disabled]");
132
133    #[cfg(feature = "statistics")]
134    oxidd_rules_zbdd::print_stats();
135}
136
137#[cfg(all(feature = "manager-index", not(feature = "manager-pointer")))]
138mod index {
139    use oxidd_manager_index::node::fixed_arity::NodeWithLevelCons;
140    use oxidd_manager_index::terminal_manager::StaticTerminalManagerCons;
141    use oxidd_rules_zbdd::ZBDDOp;
142    use oxidd_rules_zbdd::ZBDDRules;
143    use oxidd_rules_zbdd::ZBDDTerminal;
144
145    use crate::util::type_cons::DD;
146
147    crate::util::dd_index_based!(ZBDD {
148        node: NodeWithLevelCons<2>,
149        edge_tag: (),
150        terminal_manager: StaticTerminalManagerCons<ZBDDTerminal>,
151        rules: ZBDDRulesCons for ZBDDRules,
152        manager_data: ZBDDManagerDataCons for ZBDDManagerData,
153        terminals: 2,
154    });
155
156    manager_data!(ZBDDManagerData for ZBDD, operator: ZBDDOp, cache_max_arity: 3);
157
158    crate::util::manager_ref_index_based!(pub struct ZBDDManagerRef(<ZBDD as DD>::ManagerRef) with ZBDDManagerData);
159
160    #[cfg(not(feature = "multi-threading"))]
161    type FunctionInner = oxidd_rules_zbdd::ZBDDFunction<<ZBDD as DD>::Function>;
162    #[cfg(feature = "multi-threading")]
163    type FunctionInner = oxidd_rules_zbdd::ZBDDFunctionMT<<ZBDD as DD>::Function>;
164
165    /// Boolean function (or bit vector set) represented as ZBDD
166    #[derive(
167        Clone,
168        PartialEq,
169        Eq,
170        PartialOrd,
171        Ord,
172        Hash,
173        oxidd_derive::Function,
174        oxidd_derive::BooleanFunction,
175        oxidd_derive::BooleanVecSet,
176    )]
177    #[use_manager_ref(ZBDDManagerRef, ZBDDManagerRef(inner))]
178    pub struct ZBDDFunction(FunctionInner);
179    crate::util::derive_raw_function_index_based!(for: ZBDDFunction, inner: FunctionInner);
180
181    // Default implementation suffices
182    impl oxidd_dump::dot::DotStyle<()> for ZBDDFunction {}
183}
184
185#[cfg(feature = "manager-pointer")]
186mod pointer {
187    use oxidd_manager_pointer::node::fixed_arity::NodeWithLevelCons;
188    use oxidd_manager_pointer::terminal_manager::StaticTerminalManagerCons;
189    use oxidd_rules_zbdd::ZBDDOp;
190    use oxidd_rules_zbdd::ZBDDRules;
191    use oxidd_rules_zbdd::ZBDDTerminal;
192
193    use crate::util::type_cons::DD;
194
195    crate::util::dd_pointer_based!(ZBDD {
196        node: NodeWithLevelCons<2>,
197        edge_tag: (),
198        terminal_manager: StaticTerminalManagerCons<ZBDDTerminal>,
199        rules: ZBDDRulesCons for ZBDDRules,
200        manager_data: ZBDDManagerDataCons for ZBDDManagerData,
201        tag_bits: 2,
202    });
203
204    manager_data!(ZBDDManagerData for ZBDD, operator: ZBDDOp, cache_max_arity: 3);
205
206    crate::util::manager_ref_pointer_based!(pub struct ZBDDManagerRef(<ZBDD as DD>::ManagerRef) with ZBDDManagerData);
207
208    #[cfg(not(feature = "multi-threading"))]
209    type FunctionInner = oxidd_rules_zbdd::ZBDDFunction<<ZBDD as DD>::Function>;
210    #[cfg(feature = "multi-threading")]
211    type FunctionInner = oxidd_rules_zbdd::ZBDDFunctionMT<<ZBDD as DD>::Function>;
212
213    /// Boolean function (or bit vector set) represented as ZBDD
214    #[derive(
215        Clone,
216        PartialEq,
217        Eq,
218        PartialOrd,
219        Ord,
220        Hash,
221        oxidd_derive::Function,
222        oxidd_derive::BooleanFunction,
223        oxidd_derive::BooleanVecSet,
224    )]
225    #[use_manager_ref(ZBDDManagerRef, ZBDDManagerRef(inner))]
226    pub struct ZBDDFunction(FunctionInner);
227    crate::util::derive_raw_function_pointer_based!(for: ZBDDFunction, inner: FunctionInner);
228
229    // Default implementation suffices
230    impl oxidd_dump::dot::DotStyle<()> for ZBDDFunction {}
231}
232
233pub use oxidd_rules_zbdd::make_node;
234#[allow(deprecated)]
235pub use oxidd_rules_zbdd::var_boolean_function;
oxidd/zbdd.rs

oxidd/
zbdd.rs
