package zdd
Library
Module
Module type
Parameter
Class
Class type
Copyright Inria © 2025
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.
Copyright Inria © 2025
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
Functor that creates a structure of set families using a classic implementation of ZDDs
Functor that creates a structure of upward closed sets