diff --git a/lib/src/adf.rs b/lib/src/adf.rs index b0e8487..92ab300 100644 --- a/lib/src/adf.rs +++ b/lib/src/adf.rs @@ -614,7 +614,6 @@ mod test { let _adf = Adf::default(); } - #[cfg(feature = "variablelist")] #[test] fn facet_counts() { let parser = AdfParser::default(); diff --git a/lib/src/datatypes/bdd.rs b/lib/src/datatypes/bdd.rs index c313008..2f1dedb 100644 --- a/lib/src/datatypes/bdd.rs +++ b/lib/src/datatypes/bdd.rs @@ -113,6 +113,11 @@ impl Var { pub fn value(self) -> usize { self.0 } + + /// Returns true if the value of the variable is a constant (i.e. Top or Bot) + pub fn is_constant(&self) -> bool { + self.value() >= Var::BOT.value() + } } /// A [BddNode] is representing one Node in the decision diagram @@ -216,6 +221,17 @@ mod test { assert_eq!(*node.var(), var); assert_eq!(*node.lo(), lo); assert_eq!(*node.hi(), hi); + match node.var() { + Var::TOP => { + assert!(node.var().is_constant()); + } + Var::BOT => { + assert!(node.var().is_constant()); + } + val => { + assert!(!val.is_constant()); + } + } true } } diff --git a/lib/src/obdd.rs b/lib/src/obdd.rs index 008920a..d22a61d 100644 --- a/lib/src/obdd.rs +++ b/lib/src/obdd.rs @@ -323,10 +323,18 @@ impl Bdd { } #[cfg(not(feature = "variablelist"))] { - let _ = tree; - HashSet::new() + let node = self.nodes[tree.value()]; + if node.var().is_constant() { + return HashSet::new(); + } + let mut var_set = self + .var_dependencies(node.lo()) + .union(&self.var_dependencies(node.hi())) + .copied() + .collect::>(); + var_set.insert(node.var()); + var_set } - // TODO! } }