Module Zdd


module Zdd: sig .. end

Zero-suppressed binary decision diagrams.

See for instance The Art of Computer Programming, volume 4A p. 249

type unique = int 

type t = private
| Bottom
| Top
| Node of unique * int * t * t
val bottom : t
val top : t
val construct : int -> t -> t -> t
Smart constructors for ZDD. construct i z1 z2 raises Invalid_argument if i is not smaller than roots of z1 and z2.
val unique : t -> int
Each ZDD has a unique integer

A ZDD represents a set of sets of integers.

Hence this module provides all operations from OCaml's Set, with elements being sets of integers (see type elt below)
module S: Set.S  with type elt = int
type elt = S.t 
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val choose_list : t -> int list
val iter_list : (int list -> unit) -> t -> unit

Memoization

The following functions are fixpoint operators to build recursive functions over ZDDs using memoization.
val memo_rec1 : ((t -> 'a) -> t -> 'a) -> t -> 'a
val memo_rec2 : ((t * t -> 'a) -> t * t -> 'a) -> t * t -> 'a

Cardinal using big integers

Function cardinal above may easily overflow. Therefore, we also provide a functor to compute the cardinal of a ZDD using any arithmetic (e.g. Num, Gmp, Zarith, etc.)
module type ARITH = sig .. end
module Cardinal: 
functor (A : ARITH) -> sig .. end

Other functions


val size : t -> int
Number of internal nodes of a given ZDD. Each node occupies 5 words, so the total space used by a ZDD z is size z * 5 * Sys.word_size/8 bytes.
val print : Format.formatter -> t -> unit
Prints a ZDD as a set of sets of integers, e.g. { {0}, {1}, {1,2} }.
val print_to_dot : Format.formatter -> t -> unit
print_to_dot fmt z prints a ZDD z in DOT format
val print_to_dot_file : string -> t -> unit
print_to_dot f z outputs ZDD z in DOT format in file f
val stat : unit -> int
Returns the total number of unique ZDD built so far