MLCUDDIDL

MLCuddIDL is a C library offering an interface to the CUDD BDD library for OCaml version 3.00 or higher. The interface offers access to most of the functions of the library, and in addition implements some new functions. It is provided as a single module Cudd containing submodules. The interface is organized as follows: the module Man implements functions common to all the other modules; (initialization, variable ordering, ...) ; the module Bdd allows to manipulate ordinary BDDs (with complemented edge); the module Add allows to manipulate ADDs (Algebraic Decision Diagrams), the leaves of which are reals; the modules Mtbdd, Mtbddc, User and Mapleaf allows to manipulate MTBDDs (Multi-Terminal Binary Decision Diagram), the leaves of which are a user-defined OCaml datatype; the user can define and register new operations, that will then take advantage of caching techniques . I did not (yet) interfaced ZDDs, but I could do it quite quickly is someone requests it. The interface is clean for garbage collection (it makes use of custom blocks). In addition, the garbage collectors of CUDD and OCaml are synchronized: the OCaml garbage collector is requested to perform a ”full major” cycle before any CUDD garbage collection (in order to allow the later to be more efficient). Serialization and deserialization operations are not implemented.