Skip to content

Commit

Permalink
feat(bdd): made iterators work
Browse files Browse the repository at this point in the history
  • Loading branch information
AurumTheEnd committed May 10, 2024
1 parent 176a66d commit 92bbd7f
Show file tree
Hide file tree
Showing 4 changed files with 138 additions and 39 deletions.
97 changes: 97 additions & 0 deletions src/bdd/iterators/image.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,97 @@
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 super::*;
// use crate::expressions::var;
// use crate::traits::BooleanFunction;
// use std::collections::BTreeMap;
//
// #[test]
// fn test_image_ok() {
// let input = var("d") & var("b") | var("a");
//
// 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);
// }
// }
5 changes: 5 additions & 0 deletions src/bdd/iterators/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
pub use image::ImageIterator;
pub use support::SupportIterator;

mod image;
mod support;
22 changes: 22 additions & 0 deletions src/bdd/iterators/support.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
use biodivine_lib_bdd::{Bdd, BddSatisfyingValuations};

pub struct SupportIterator<'a> {
inner: BddSatisfyingValuations<'a>,
}

impl<'a> SupportIterator<'a> {
pub fn new(bdd: &Bdd) -> Self {
let owned = bdd.clone();
Self {
inner: owned.sat_valuations(),
}
}
}

impl Iterator for SupportIterator<'_> {
type Item = Vec<bool>;

fn next(&mut self) -> Option<Self::Item> {
self.inner.next().map(|it| it.vector())
}
}
53 changes: 14 additions & 39 deletions src/bdd/mod.rs
Original file line number Diff line number Diff line change
@@ -1,11 +1,14 @@
mod iterators;

use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
use std::fmt::Debug;
use std::ops::BitAnd;
use std::iter::{zip, Zip};

use crate::bdd::iterators::ImageIterator;
use biodivine_lib_bdd::{Bdd as InnerBdd, BddVariable, BddVariableSet};
use num_bigint::BigUint;

use crate::iterators::{DomainIterator, ImageIterator, RelationIterator, SupportIterator};
use crate::iterators::{DomainIterator, SupportIterator};
use crate::traits::{BooleanFunction, BooleanPoint, BooleanValuation};

/*
Expand Down Expand Up @@ -65,39 +68,10 @@ impl<TLiteral: Debug + Clone + Eq + Ord + 'static> Bdd<TLiteral> {
}
}

impl<TLiteral: Debug + Clone + Eq + Ord + 'static> BitAnd for Bdd<TLiteral> {
type Output = Bdd<TLiteral>;

fn bitand(self, rhs: Self) -> Self::Output {
if self.inputs == rhs.inputs {
Bdd {
inputs: self.inputs.clone(),
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);

Bdd {
inputs: common_inputs,
bdd: self_lifted.bdd.and(&rhs_lifted.bdd),
}
}
}
}

impl<T: Debug + Clone + Eq + Ord + 'static> BooleanFunction<T> for Bdd<T> {
impl<T: Debug + Clone + Ord + 'static> BooleanFunction<T> for Bdd<T> {
type DomainIterator = DomainIterator;
type RangeIterator = ImageIterator<T>;
type RelationIterator = RelationIterator<T>;
type RangeIterator = ImageIterator;
type RelationIterator = Zip<DomainIterator, ImageIterator>;
type SupportIterator = SupportIterator<T>;

fn inputs(&self) -> BTreeSet<T> {
Expand All @@ -124,24 +98,25 @@ impl<T: Debug + Clone + Eq + Ord + 'static> BooleanFunction<T> for Bdd<T> {
}

fn domain(&self) -> Self::DomainIterator {
todo!()
DomainIterator::from_count(self.inputs.len())
}

fn image(&self) -> Self::RangeIterator {
// evaluate for each domain point
// DomainIterator::new(self).map(|it| self.bdd.eval_in(&BddValuation::new(it)));
todo!()
ImageIterator::new(self.inputs.len(), &self.bdd)
}

fn relation(&self) -> Self::RelationIterator {
// zip domain/range
todo!()
zip(self.domain(), self.image())
}

fn support(&self) -> Self::SupportIterator {
// Only points that satisfy the function
self.bdd.sat_valuations().map(|it| it.vector());
todo!()
// SupportIterator::new(&self.bdd)
// self.bdd.sat_valuations().map(|it| it.vector())
todo!("Wait for sat_valuations to be an owned iterator without a lifetime")
}

fn weight(&self) -> BigUint {
Expand Down

0 comments on commit 92bbd7f

Please sign in to comment.