Zdd (zdd.Zdd)

This module implements families of finite sets, implemented as ZDDs (Zero-Suppressed Binary Decision Diagrams).

S.-i. Minato, “Zero-suppressed BDDs for set manipulation in combinatorial problems,” in Proceedings of the 30th international on Design automation conference - DAC ’93, in DAC ’93. ACM Press, 1993, pp. 272–277. doi: 10.1145/157485.164890

S.-i. Minato, “Zero-suppressed BDDs and their applications,” International Journal on Software Tools for Technology Transfer, vol. 3, no. 2, pp. 156–170, May 2001, doi: 10.1007/s100090100038

On top of this implementation, this module also provides structures for upward-closed and downward-closed set families.

Warning: be aware that this implementation is not thread safe, as it uses references and hash tables internally.

module type T = sig ... end

Signature of types for which set families can be created

module type S = sig ... end

The signature of set families

module type UPSET = sig ... end

Signature of upward-closed sets, represented as the set of their minimal elements

module type DOWNSET = sig ... end

Signature of downward-closed sets, represented as the set of their maximal elements

module Make_ZddZE (X : sig ... end) : sig ... end

Functor that creates a structure of set families using an implementation of ZDDs using zero-attributed edges

module Make_Zdd (X : sig ... end) : sig ... end

Functor that creates a structure of set families using a classic implementation of ZDDs

module Make (X : T) : S with type elt = X.t

Functor that creates a structure of set families

module UpSet (X : T) : UPSET with type elt = X.t

Functor that creates a structure of upward closed sets

module DownSet (X : T) : DOWNSET with type elt = X.t

Functor that creates a structure of downward closed sets