[−][src]Crate zdd

A ZDD library, based on this paper by Shin-Ichi Minato.

ZDDs are hash consed so equality is constant time. All operations on ZDDs provided by Factory are cached: count, offset, onset, change, union, inter, minus and subset.

Warning

I wrote this crate a very long time ago, when I was a Rust newbie. There seems to be little interest in this library, so I only barely maintain it. If you are serious about using it, consider letting me know to see if I or someone else can improve or rewrite it.

Factory

A Factory maintains the hash cons table for the ZDDs, as well as the caches for basic operations. A factory is thread-safe. Usage is Caml-module-like

use zdd::* ;
let f = Factory::<&'static str>::mk(7) ;

let ref zero = f.zero() ;
let ref one = f.one() ;

let ref x = f.mk_node("x", zero, one) ;
let ref _x = f.change(one, "x") ;
println!(" x: {}",  x) ;
println!("_x: {}", _x) ;
assert!(x == _x) ;

let ref y = f.change(one, "y") ;
let ref x_u_y = f.union(x, y) ;
let ref z = f.change(one, "z") ;
let ref x_u_y_m_z = f.minus(x_u_y, z) ;
assert!(x_u_y_m_z == x_u_y) ;

Wrapped

The easiest way to manipulate ZDDs is to use wrapped::Zdd which is wrapper around a ZDD and its associated factory.

use zdd::wrapped::* ;
let f = mk_factory::<&'static str>(7) ;

let ref one = Zdd::one(&f) ;

let ref x = one ^ "x"         ; // Change "x" in one.
let ref y = one ^ "y"         ; // change "y" in one.
let ref z = one ^ "z"         ; // Change "z" in one.
let ref x_u_y = x + y         ; // Union.
let ref x_u_y_m_z = x_u_y - z ; // Difference.
assert!(x_u_y_m_z == x_u_y) ;

Re-exports

pub use factory::Factory;

pub use factory::FactoryBinOps;

pub use factory::FactoryBuilder;

pub use factory::FactoryUnLblOps;

pub use factory::FactoryUnOps;

pub use factory::ZddMaker;

Modules

factory	ZDD factory.
wrapped	ZDDs containing their factory.

ZddPrint	Printing and logging to graphviz.
ZddTreeOps	Basic operations on ZDD.

Type Definitions

Zdd	A hash consed ZDD.