Bdds

Cargo.toml

@@ -22,6 +22,7 @@ tabled = "0.15.0"
 csv = { version = "1.3.0", optional = true }
 tempfile = { version = "3.10.1", optional = true }
 num-bigint = "0.4.4"
+biodivine-lib-bdd = "0.5.16"
 
 pyo3 = { version = "0.21.2", features = ["abi3-py37", "extension-module", "num-bigint"], optional = true }
 

src/bdd/iterators/image.rs

@@ -0,0 +1,96 @@
+use crate::iterators::DomainIterator;
+use biodivine_lib_bdd::Bdd;
+use biodivine_lib_bdd::BddValuation;
+
+pub struct ImageIterator {
+    domain_iterator: Box<dyn Iterator<Item = Vec<bool>>>,
+    bdd: Bdd,
+}
+
+impl ImageIterator {
+    pub(crate) fn new(input_count: usize, bdd: &Bdd) -> Self {
+        Self {
+            domain_iterator: Box::new(DomainIterator::from_count(input_count)),
+            bdd: bdd.clone(),
+        }
+    }
+}
+
+impl Iterator for ImageIterator {
+    type Item = bool;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        self.domain_iterator
+            .next()
+            .map(|it| self.bdd.eval_in(&BddValuation::new(it)))
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::var;
+    use crate::traits::{BooleanFunction, Evaluate};
+    use std::collections::BTreeMap;
+
+    #[test]
+    fn test_image_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic");
+
+        let mut actual = input.image();
+        let expected = [
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+        ];
+
+        assert_eq!(actual.next(), expected[0]);
+        assert_eq!(actual.next(), expected[1]);
+        assert_eq!(actual.next(), expected[2]);
+        assert_eq!(actual.next(), expected[3]);
+        assert_eq!(actual.next(), expected[4]);
+        assert_eq!(actual.next(), expected[5]);
+        assert_eq!(actual.next(), expected[6]);
+        assert_eq!(actual.next(), expected[7]);
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+}

src/bdd/iterators/mod.rs

@@ -0,0 +1,5 @@
+pub use image::ImageIterator;
+pub use support::SupportIterator;
+
+mod image;
+mod support;

src/bdd/iterators/support.rs

@@ -0,0 +1,90 @@
+use biodivine_lib_bdd::{Bdd, OwnedBddSatisfyingValuations};
+
+pub struct SupportIterator {
+    iterator: OwnedBddSatisfyingValuations,
+}
+
+impl SupportIterator {
+    pub(crate) fn new(bdd: &Bdd) -> Self {
+        Self {
+            iterator: bdd.clone().into_sat_valuations(),
+        }
+    }
+}
+
+impl Iterator for SupportIterator {
+    type Item = Vec<bool>;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        self.iterator.next().map(|it| it.vector())
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use crate::bdd::Bdd;
+    use crate::expressions::var;
+    use crate::traits::{BooleanFunction, Evaluate};
+    use std::collections::BTreeMap;
+
+    #[test]
+    fn test_image_ok() {
+        let input = Bdd::try_from(var("d") & var("b") | var("a")).expect("Should not panic here");
+
+        let mut actual = input.image();
+        let expected = [
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), false),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), false),
+                ("d".to_string(), true),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), false),
+            ]))),
+            Some(input.evaluate(&BTreeMap::from([
+                ("a".to_string(), true),
+                ("b".to_string(), true),
+                ("d".to_string(), true),
+            ]))),
+        ];
+
+        assert_eq!(actual.next(), expected[0]);
+        assert_eq!(actual.next(), expected[1]);
+        assert_eq!(actual.next(), expected[2]);
+        assert_eq!(actual.next(), expected[3]);
+        assert_eq!(actual.next(), expected[4]);
+        assert_eq!(actual.next(), expected[5]);
+        assert_eq!(actual.next(), expected[6]);
+        assert_eq!(actual.next(), expected[7]);
+
+        assert_eq!(actual.next(), None);
+        assert_eq!(actual.next(), None);
+    }
+}

src/bdd/mod.rs

@@ -0,0 +1,150 @@
+mod iterators;
+mod traits;
+mod utils;
+
+use crate::bdd::utils::{extend_bdd_variables, prune_bdd_variables};
+use biodivine_lib_bdd::{Bdd as InnerBdd, BddVariable, BddVariableSet};
+use std::collections::{BTreeMap, BTreeSet};
+use std::fmt::Debug;
+use std::num::TryFromIntError;
+
+/*
+   Conversions:
+
+   Bdd -> Table: iterate support and use it to fill the table with ones.
+
+   Table -> Bdd: Build a `BddPartialValuation` for each one-row in the table and then
+   use `BddVariableSet::mk_dnf` to build `Bdd`.
+
+   Bdd -> Expression: `Bdd.to_optimized_dnf()` to convert to `Vec<BddPartialValuation>`, then
+   convert each partial valuation to one AND-clause and the whole vector to a disjunction.
+
+   Expression -> Bdd: Run gather literals, create a BddVariableSet, then recursively follow
+   the expression structure. Literal/Constant correspond to BddVariableSet.mk_literal/mk_constant,
+   not/and/or operators correspond to Bdd.not/and/or.
+
+*/
+
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub struct Bdd<TLiteral>
+where
+    TLiteral: Debug + Clone + Eq + Ord,
+{
+    /// Always-sorted vector of no more than 65k variables (see `lib-bdd`).
+    inputs: Vec<TLiteral>,
+    /// Holds the `lib_bdd` representation.
+    bdd: InnerBdd,
+}
+
+impl<TLiteral: Debug + Clone + Eq + Ord> Bdd<TLiteral> {
+    pub(crate) fn new(inner: InnerBdd, inputs: Vec<TLiteral>) -> Self {
+        Self { bdd: inner, inputs }
+    }
+
+    /// Converts a literal representation as a generic user struct
+    /// into `BddVariable` used by `lib_bdd::Bdd`.
+    ///
+    /// If such a variable isn't used in this `Bdd`, the method returns `None`.
+    fn map_var_outer_to_inner(&self, variable: &TLiteral) -> Option<BddVariable> {
+        self.inputs
+            .binary_search(variable)
+            .ok()
+            .map(BddVariable::from_index)
+    }
+
+    /// Converts a `BddVariable` used by `lib_bdd::Bdd` into a literal representation
+    /// used by `self`.
+    ///
+    /// If such a variable isn't used in this `Bdd`, the method returns `None`.
+    pub(crate) fn map_var_inner_to_outer(&self, variable: BddVariable) -> Option<TLiteral> {
+        self.inputs.get(variable.to_index()).cloned()
+    }
+
+    /// Creates a `BddVariableSet` used by `lib_bdd::Bdd`.
+    ///
+    /// Since `lib_bdd` only supports up to 2<sup>16</sup> variables, this method returns an `Err` if
+    /// the number of `variables` is above that.
+    fn make_inner_variable_set(
+        variables: BTreeSet<TLiteral>,
+    ) -> Result<BddVariableSet, TryFromIntError> {
+        let num_vars = u16::try_from(variables.len())?;
+        Ok(BddVariableSet::new_anonymous(num_vars))
+    }
+
+    pub(crate) fn inner(&self) -> &InnerBdd {
+        &self.bdd
+    }
+
+    fn restrict_and_prune_map<TValue>(
+        &self,
+        valuation: &BTreeMap<TLiteral, TValue>,
+        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)
+    }
+
+    fn union_and_extend_n_ary(
+        &self,
+        others: &mut BTreeMap<TLiteral, Bdd<TLiteral>>,
+    ) -> (Bdd<TLiteral>, Vec<TLiteral>) {
+        let mut common_inputs = self.inputs.clone();
+
+        for other in others.values() {
+            for input in &other.inputs {
+                if !common_inputs.contains(input) {
+                    common_inputs.push(input.clone());
+                }
+            }
+        }
+
+        common_inputs.sort();
+
+        let self_lifted = extend_bdd_variables(self, &common_inputs);
+        for other in others.values_mut() {
+            *other = extend_bdd_variables(other, &common_inputs);
+        }
+
+        (self_lifted, common_inputs)
+    }
+}