#[macro_use]
extern crate hashconsing;
use std::cmp::Eq;
use std::collections::BTreeSet;
use std::fmt;
use hashconsing::HConsed;
mod print;
pub use print::ZddPrint;
#[macro_use]
mod zip;
pub mod factory;
pub use factory::{
Factory, FactoryBinOps, FactoryBuilder, FactoryUnLblOps, FactoryUnOps, ZddMaker,
};
pub mod wrapped;
pub type Zdd<Label> = HConsed<ZddTree<Label>>;
#[derive(Clone, PartialEq, Hash)]
pub enum ZddTree<Label> {
Node(Label, Zdd<Label>, Zdd<Label>),
HasOne(Zdd<Label>),
Zero,
}
impl<Label: Ord + Clone> ZddTree<Label> {
pub fn iter(&self) -> Iterator<Label> {
let stack = match *self {
ZddTree::Node(ref lbl, ref lft, ref rgt) => {
vec![(vec![], lft.clone()), (vec![lbl.clone()], rgt.clone())]
}
ZddTree::HasOne(ref kid) => vec![(vec![], kid.clone())],
ZddTree::Zero => vec![],
};
Iterator { stack: stack }
}
}
impl<Label: Ord + Clone + fmt::Display> fmt::Display for ZddTree<Label> {
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
write!(fmt, "{{ ")?;
let mut is_fst = true;
let stack = match *self {
ZddTree::HasOne(ref kid) => {
write!(fmt, "{{}}")?;
if kid.is_zero() {
return write!(fmt, " }}");
} else {
write!(fmt, ", ")?;
vec![(vec![], kid.clone())]
}
}
ZddTree::Node(ref lbl, ref lft, ref rgt) => {
vec![(vec![], lft.clone()), (vec![lbl.clone()], rgt.clone())]
}
ZddTree::Zero => return write!(fmt, " }}"),
};
let iter = Iterator { stack: stack };
for vec in iter {
if is_fst {
is_fst = false
} else {
write!(fmt, ", ")?
};
write!(fmt, "{{")?;
let mut is_fst = true;
for e in vec.into_iter() {
if is_fst {
is_fst = false
} else {
write!(fmt, ", ")?
};
write!(fmt, "{}", e)?;
}
write!(fmt, "}}")?;
}
write!(fmt, " }}")
}
}
impl<Label: Clone + Eq> Eq for ZddTree<Label> {}
pub trait ZddTreeOps<Label: Ord + Clone> {
fn is_zero(&self) -> bool;
fn is_one(&self) -> bool;
fn has_one(&self) -> bool;
fn top(&self) -> Result<Label, bool>;
fn to_set(&self) -> BTreeSet<BTreeSet<Label>>;
fn iter(&self) -> Iterator<Label>;
}
impl<Label: Ord + Clone> ZddTreeOps<Label> for Zdd<Label> {
fn is_zero(&self) -> bool {
self.top() == Err(false)
}
fn is_one(&self) -> bool {
self.top() == Err(true)
}
fn has_one(&self) -> bool {
match **self {
ZddTree::HasOne(_) => true,
_ => false,
}
}
fn top(&self) -> Result<Label, bool> {
match **self {
ZddTree::Zero => Err(false),
ZddTree::HasOne(ref kid) => match **kid {
ZddTree::Zero => Err(true),
ZddTree::Node(ref lbl, _, _) => Ok(lbl.clone()),
_ => panic!("[top] ZDD is ill-formed"),
},
ZddTree::Node(ref lbl, _, _) => Ok(lbl.clone()),
}
}
fn to_set(&self) -> BTreeSet<BTreeSet<Label>> {
match self.top() {
Err(false) => BTreeSet::new(),
Err(true) => {
let mut sset = BTreeSet::new();
sset.insert(BTreeSet::new());
sset
}
_ => {
let mut set = BTreeSet::new();
let mut path = vec![];
let mut res = BTreeSet::new();
let mut zdd = self.clone();
loop {
zdd = match *zdd {
ZddTree::Node(ref top, ref lft, ref rgt) => {
let mut rgt_set = set.clone();
rgt_set.insert(top.clone());
path.push((rgt.clone(), rgt_set));
lft.clone()
}
ZddTree::HasOne(ref kid) => {
res.insert(set.clone());
kid.clone()
}
ZddTree::Zero => {
if let Some((nu_zdd, nu_set)) = path.pop() {
set = nu_set;
nu_zdd
} else {
return res;
}
}
}
}
}
}
}
fn iter(&self) -> Iterator<Label> {
Iterator {
stack: vec![(vec![], self.clone())],
}
}
}
pub struct Iterator<Label: Clone> {
stack: Vec<(Vec<Label>, Zdd<Label>)>,
}
impl<Label: Ord + Clone> std::iter::Iterator for Iterator<Label> {
type Item = Vec<Label>;
fn next(&mut self) -> Option<Vec<Label>> {
if let Some((prefix, zdd)) = self.stack.pop() {
let mut pair = (prefix, zdd);
loop {
let (mut prefix, zdd) = pair;
pair = if zdd.is_one() {
return Some(prefix);
} else {
if zdd.is_zero() {
if let Some((prefix, zdd)) = self.stack.pop() {
(prefix, zdd)
} else {
return None;
}
} else {
match *zdd {
ZddTree::HasOne(ref zdd) => {
self.stack.push((prefix.clone(), zdd.clone()));
return Some(prefix);
}
ZddTree::Node(ref lbl, ref lft, ref rgt) => {
let lft_prefix = prefix.clone();
prefix.push(lbl.clone());
self.stack.push((lft_prefix, lft.clone()));
(prefix, rgt.clone())
}
_ => unreachable!(),
}
}
};
}
} else {
None
}
}
}