refactor(bdd): moved duplicate code to restrict_and_prune & union_and…

…_extend

src/bdd/mod.rs

@@ -2,7 +2,8 @@ mod iterators;
 mod traits;
 mod utils;
 
-use crate::bdd::utils::extend_bdd_variables;
+use crate::bdd::utils::{extend_bdd_variables, prune_bdd_variables};
+use crate::traits::BooleanValuation;
 use biodivine_lib_bdd::{Bdd as InnerBdd, BddVariable, BddVariableSet};
 use std::collections::BTreeSet;
 use std::fmt::Debug;
@@ -70,4 +71,53 @@ impl<TLiteral: Debug + Clone + Eq + Ord> Bdd<TLiteral> {
     pub(crate) fn inner(&self) -> &InnerBdd {
         &self.bdd
     }
+
+    fn restrict_and_prune_map(
+        &self,
+        valuation: &BooleanValuation<TLiteral>,
+        new_bdd: &Bdd<TLiteral>,
+    ) -> Bdd<TLiteral> {
+        self.restrict_and_prune_common(valuation, new_bdd, |set, var| set.contains_key(var))
+    }
+
+    fn restrict_and_prune_set(
+        &self,
+        valuation: &BTreeSet<TLiteral>,
+        new_bdd: &Bdd<TLiteral>,
+    ) -> Bdd<TLiteral> {
+        self.restrict_and_prune_common(valuation, new_bdd, |set, var| set.contains(var))
+    }
+
+    fn restrict_and_prune_common<TCollection, P: Fn(&TCollection, &&TLiteral) -> bool>(
+        &self,
+        valuation: &TCollection,
+        new_bdd: &Bdd<TLiteral>,
+        contains: P,
+    ) -> Bdd<TLiteral> {
+        let restricted_inputs = self
+            .inputs
+            .iter()
+            .filter(|var| !contains(valuation, var))
+            .cloned()
+            .collect::<Vec<_>>();
+        prune_bdd_variables(new_bdd, &restricted_inputs)
+    }
+
+    fn union_and_extend(
+        &self,
+        other: &Bdd<TLiteral>,
+    ) -> (Bdd<TLiteral>, Bdd<TLiteral>, Vec<TLiteral>) {
+        let mut common_inputs = self.inputs.clone();
+        for other in &other.inputs {
+            if !common_inputs.contains(other) {
+                common_inputs.push(other.clone());
+            }
+        }
+        common_inputs.sort();
+
+        let self_lifted = extend_bdd_variables(self, &common_inputs);
+        let other_lifted = extend_bdd_variables(other, &common_inputs);
+
+        (self_lifted, other_lifted, common_inputs)
+    }
 }

src/bdd/traits/bit/and.rs

@@ -1,4 +1,4 @@
-use crate::bdd::{extend_bdd_variables, Bdd};
+use crate::bdd::Bdd;
 use std::fmt::Debug;
 use std::ops::BitAnd;
 
@@ -12,16 +12,7 @@ impl<TLiteral: Debug + Clone + Eq + Ord + 'static> BitAnd for Bdd<TLiteral> {
                 bdd: self.bdd.and(&rhs.bdd),
             }
         } else {
-            let mut common_inputs = self.inputs.clone();
-            for other in &rhs.inputs {
-                if !common_inputs.contains(other) {
-                    common_inputs.push(other.clone());
-                }
-            }
-            common_inputs.sort();
-
-            let self_lifted = extend_bdd_variables(&self, &common_inputs);
-            let rhs_lifted = extend_bdd_variables(&rhs, &common_inputs);
+            let (self_lifted, rhs_lifted, common_inputs) = self.union_and_extend(&rhs);
 
             Bdd {
                 inputs: common_inputs,

src/bdd/traits/boolean_function.rs

@@ -1,5 +1,4 @@
 use crate::bdd::iterators::{ImageIterator, SupportIterator};
-use crate::bdd::utils::{extend_bdd_variables, prune_bdd_variables};
 use crate::bdd::Bdd;
 use crate::iterators::DomainIterator;
 use crate::traits::{BooleanFunction, BooleanPoint, BooleanValuation};
@@ -71,13 +70,8 @@ impl<T: Debug + Clone + Ord> BooleanFunction<T> for Bdd<T> {
             inputs: self.inputs.clone(),
             bdd: self.bdd.restrict(&lib_bdd_valuation),
         };
-        let restricted_inputs = self
-            .inputs
-            .iter()
-            .filter(|var| !valuation.contains_key(var))
-            .cloned()
-            .collect::<Vec<_>>();
-        prune_bdd_variables(&new_bdd, &restricted_inputs)
+
+        self.restrict_and_prune_map(valuation, &new_bdd)
     }
 
     fn substitute(&self, _mapping: &BTreeMap<T, Self>) -> Self {
@@ -102,13 +96,8 @@ impl<T: Debug + Clone + Ord> BooleanFunction<T> for Bdd<T> {
             inputs: self.inputs.clone(),
             bdd: self.bdd.exists(&lib_bdd_variables),
         };
-        let restricted_inputs = self
-            .inputs
-            .iter()
-            .filter(|var| !variables.contains(var))
-            .cloned()
-            .collect::<Vec<_>>();
-        prune_bdd_variables(&new_bdd, &restricted_inputs)
+
+        self.restrict_and_prune_set(&variables, &new_bdd)
     }
 
     fn universal_quantification(&self, variables: BTreeSet<T>) -> Self {
@@ -120,13 +109,8 @@ impl<T: Debug + Clone + Ord> BooleanFunction<T> for Bdd<T> {
             inputs: self.inputs.clone(),
             bdd: self.bdd.for_all(&lib_bdd_variables),
         };
-        let restricted_inputs = self
-            .inputs
-            .iter()
-            .filter(|var| !variables.contains(var))
-            .cloned()
-            .collect::<Vec<_>>();
-        prune_bdd_variables(&new_bdd, &restricted_inputs)
+
+        self.restrict_and_prune_set(&variables, &new_bdd)
     }
 
     fn derivative(&self, variables: BTreeSet<T>) -> Self {
@@ -147,40 +131,18 @@ impl<T: Debug + Clone + Ord> BooleanFunction<T> for Bdd<T> {
             ),
         };
 
-        let restricted_inputs = self
-            .inputs
-            .iter()
-            .filter(|var| !variables.contains(var))
-            .cloned()
-            .collect::<Vec<_>>();
-        prune_bdd_variables(&new_bdd, &restricted_inputs)
+        self.restrict_and_prune_set(&variables, &new_bdd)
     }
 
     fn is_equivalent(&self, other: &Self) -> bool {
-        let mut common_inputs = self.inputs.clone();
-        for other in &other.inputs {
-            if !common_inputs.contains(other) {
-                common_inputs.push(other.clone());
-            }
-        }
-        common_inputs.sort();
-
-        let self_lifted = extend_bdd_variables(self, &common_inputs);
-        let other_lifted = extend_bdd_variables(other, &common_inputs);
+        let (self_lifted, other_lifted, _common_inputs) = self.union_and_extend(other);
+
         self_lifted.bdd == other_lifted.bdd
     }
 
     fn is_implied_by(&self, other: &Self) -> bool {
-        let mut common_inputs = self.inputs.clone();
-        for other in &other.inputs {
-            if !common_inputs.contains(other) {
-                common_inputs.push(other.clone());
-            }
-        }
-        common_inputs.sort();
-
-        let self_lifted = extend_bdd_variables(self, &common_inputs);
-        let other_lifted = extend_bdd_variables(other, &common_inputs);
+        let (self_lifted, other_lifted, _common_inputs) = self.union_and_extend(other);
+
         other_lifted.bdd.imp(&self_lifted.bdd).is_true()
     }
 }