oxidd/
bcdd.rs

1//! Binary decision diagrams with complemented edges (BCDDs)
2
3cfg_if::cfg_if! {
4    if #[cfg(feature = "manager-pointer")] {
5        pub use pointer::{BCDDFunction, BCDDManagerRef};
6    } else if #[cfg(feature = "manager-index")] {
7        pub use index::{BCDDFunction, BCDDManagerRef};
8    } else {
9        pub type BCDDFunction = ();
10        pub type BCDDManagerRef = ();
11    }
12}
13
14/// Print statistics to stderr
15pub fn print_stats() {
16    #[cfg(not(feature = "statistics"))]
17    eprintln!("[statistics feature disabled]");
18
19    #[cfg(feature = "statistics")]
20    oxidd_rules_bdd::complement_edge::print_stats();
21}
22
23/// Create a new manager for a binary decision diagram with complement edges
24#[allow(unused_variables)]
25pub fn new_manager(
26    inner_node_capacity: usize,
27    apply_cache_capacity: usize,
28    threads: u32,
29) -> BCDDManagerRef {
30    cfg_if::cfg_if! {
31        if #[cfg(feature = "manager-pointer")] {
32            pointer::BCDDManagerRef::new_manager(inner_node_capacity, apply_cache_capacity, threads)
33        } else if #[cfg(feature = "manager-index")] {
34            index::BCDDManagerRef::new_manager(inner_node_capacity, 1, apply_cache_capacity, threads)
35        } else {
36            unreachable!()
37        }
38    }
39}
40
41#[cfg(all(feature = "manager-index", not(feature = "manager-pointer")))]
42mod index {
43    use oxidd_manager_index::node::fixed_arity::NodeWithLevelCons;
44    use oxidd_manager_index::terminal_manager::StaticTerminalManagerCons;
45    use oxidd_rules_bdd::complement_edge::BCDDOp;
46    use oxidd_rules_bdd::complement_edge::BCDDRules;
47    use oxidd_rules_bdd::complement_edge::BCDDTerminal;
48    use oxidd_rules_bdd::complement_edge::EdgeTag;
49
50    use crate::util::type_cons::DD;
51
52    crate::util::dd_index_based!(BCDD {
53        node: NodeWithLevelCons<2>,
54        edge_tag: EdgeTag,
55        terminal_manager: StaticTerminalManagerCons<BCDDTerminal>,
56        rules: BCDDRulesCons for BCDDRules,
57        manager_data: BCDDManagerDataCons for BCDDManagerData,
58        terminals: 1,
59    });
60
61    crate::util::manager_data!(BCDDManagerData for BCDD, operator: BCDDOp, cache_max_arity: 3);
62
63    crate::util::manager_ref_index_based!(pub struct BCDDManagerRef(<BCDD as DD>::ManagerRef) with BCDDManagerData);
64
65    #[cfg(not(feature = "multi-threading"))]
66    type FunctionInner = oxidd_rules_bdd::complement_edge::BCDDFunction<<BCDD as DD>::Function>;
67    #[cfg(feature = "multi-threading")]
68    type FunctionInner = oxidd_rules_bdd::complement_edge::BCDDFunctionMT<<BCDD as DD>::Function>;
69
70    /// Boolean function represented as BCDD
71    #[derive(
72        Clone,
73        PartialEq,
74        Eq,
75        PartialOrd,
76        Ord,
77        Hash,
78        oxidd_derive::Function,
79        oxidd_derive::FunctionSubst,
80        oxidd_derive::BooleanFunction,
81        oxidd_derive::BooleanFunctionQuant,
82    )]
83    #[use_manager_ref(BCDDManagerRef, BCDDManagerRef(inner))]
84    pub struct BCDDFunction(FunctionInner);
85    crate::util::derive_raw_function_index_based!(for: BCDDFunction, inner: FunctionInner);
86
87    // Default implementation suffices
88    impl oxidd_dump::dot::DotStyle<EdgeTag> for BCDDFunction {}
89}
90
91#[cfg(feature = "manager-pointer")]
92mod pointer {
93    use oxidd_manager_pointer::node::fixed_arity::NodeWithLevelCons;
94    use oxidd_manager_pointer::terminal_manager::StaticTerminalManagerCons;
95    use oxidd_rules_bdd::complement_edge::BCDDOp;
96    use oxidd_rules_bdd::complement_edge::BCDDRules;
97    use oxidd_rules_bdd::complement_edge::BCDDTerminal;
98    use oxidd_rules_bdd::complement_edge::EdgeTag;
99
100    use crate::util::type_cons::DD;
101
102    crate::util::dd_pointer_based!(BCDD {
103        node: NodeWithLevelCons<2>,
104        edge_tag: EdgeTag,
105        terminal_manager: StaticTerminalManagerCons<BCDDTerminal>,
106        rules: BCDDRulesCons for BCDDRules,
107        manager_data: BCDDManagerDataCons for BCDDManagerData,
108        tag_bits: 2,
109    });
110
111    crate::util::manager_data!(BCDDManagerData for BCDD, operator: BCDDOp, cache_max_arity: 3);
112
113    crate::util::manager_ref_pointer_based!(pub struct BCDDManagerRef(<BCDD as DD>::ManagerRef) with BCDDManagerData);
114
115    #[cfg(not(feature = "multi-threading"))]
116    type FunctionInner = oxidd_rules_bdd::complement_edge::BCDDFunction<<BCDD as DD>::Function>;
117    #[cfg(feature = "multi-threading")]
118    type FunctionInner = oxidd_rules_bdd::complement_edge::BCDDFunctionMT<<BCDD as DD>::Function>;
119
120    /// Boolean function represented as BCDD
121    #[derive(
122        Clone,
123        PartialEq,
124        Eq,
125        PartialOrd,
126        Ord,
127        Hash,
128        oxidd_derive::Function,
129        oxidd_derive::FunctionSubst,
130        oxidd_derive::BooleanFunction,
131        oxidd_derive::BooleanFunctionQuant,
132    )]
133    #[use_manager_ref(BCDDManagerRef, BCDDManagerRef(inner))]
134    pub struct BCDDFunction(FunctionInner);
135    crate::util::derive_raw_function_pointer_based!(for: BCDDFunction, inner: FunctionInner);
136
137    // Default implementation suffices
138    impl oxidd_dump::dot::DotStyle<EdgeTag> for BCDDFunction {}
139}
oxidd/bcdd.rs

oxidd/
bcdd.rs
