module Cudd:Interface to CUDD library
Cudd.Man: CUDD managers;
Cudd.Bdd: CUDD BDDs;
Cudd.Add: CUDD ADDs;
Cudd.Mtbddc: MTBDDs on OCaml values;
Cudd.User: maps user operations from leaves to MTBDDs on such leaves.
Cudd.Memo, relying on
Cudd.Cache: allows the control of memoization techniques, for permutation and vector composition functions on BDDs and MTBDDs, and user operations.
Cudd.Vdd: MTBDDs on unhashed OCaml values;
Cudd.Custom: for user operations on ADDs and MTBDDs;
Cudd.PWeakke: for polymorphic weak hashtables.
Most functions of the CUDD library are interfaced; with the exception of ZDDs functions. If you need it, please tell me, I can do it quickly.
The diagrams are implemented as abstract types, and more precisely as OCAML custom objects. These objects contain both the manager which owns the diagram and the diagram itself. They are garbage collected by the OCAML garbage collection. The effect of the OCAML garbage collection is to decrease the reference count of the diagram if it has become unreachable from the OCAML heap, and to remove the OCAML custom object from the OCAML heap. Later, the CUDD may possibly garbage the diagram in the C heap, if its reference count is zero.
For technical reasons, CUDD managers come in two different flavors in the
OCaml interface: one dedicated to BDDs and standard CUDD ADDs (Algebraic
Decision Diagrams, with C double values at leaves) , which has the type
Man.d Man.t, and one dedicated to BDDs and so-called VDDs, with OCaml values at leaves., which has the type
Man.v Man.t, see
For efficiency reasons, it is better to link in some way the two garbage collectors. So, when the CUDD garbage collector is triggered, in a normal situation (during the creation of a new node) or because of a reordering operation, it first calls the OCAML garbage collector, in order to be able to garbage collect as many nodes as possible.
Cudd.Man.set_gc allows to tune the OCAML garbage
collection of diagrams and the link with the CUDD garbage
It is possible to apply to the diagrams the polymorphic comparison
Pervasives.compare, from which are derived
and polymorphic hash function (polymorphic
comparison function compares lexicographically the pair
of the manager, address of the node). The hash function returns
the address of the node.
Each module is described separately. For each Ocaml function, we indicate below in typewriter font the CUDD function to which it corresponds, whenever possible. If the order of the arguments has been changed, we usually specify ``variation of'' before.
We do not describe in detail the functions which have a direct CUDD equivalent. Instead, we refer the user to the original CUDD documentation.
Organization of the code
The interface has been written with the help of the CamlIDL tool,
the input files of which are suffixed with
automatizes most of the cumbersome task of writing stub codes and
converting datatypes back and forth between C and OCAML. However,
as we implemented more than a direct interface, we also used the
M4 preprocessor on
.idl files to simplify the task (instead of
the default cpp C preprocessor).
.idl files are thus filtered through M4 and transformed
according to the macro file
macros.m4, then CamlIDL generates
from them four files, suffixed with
are not generated from a
.idl file and contain code common to
all the other files.
The normal user doesn't need to understand this process, as the library is distributed with all the C and OCAML files already generated.
Installation and Use
CUDD BDD library is now included in the distribution.
Flags should be properly set in
Makefile.config (starting from
Also, the Make rules for some
example.ml file shows how to compile
a program with the interface.
Hash: User hashtables
Cache: Local caches
Memo: Memoization policy
Man: CUDD Manager
Bdd: Binary Decision Diagrams
Vdd: MTBDDs with OCaml values (INTERNAL)
Custom: Type of identifiers
Weakke: Hash tables of weak pointers.
PWeakke: Hash tables of weak pointers, parametrized polymorphic version.
Mtbdd: MTBDDs with OCaml values
Mtbddc: MTBDDs with finalized OCaml values.
User: Custom operations for MTBDDs
Mapleaf: Lifting operation on leaves to operations on MTBDDs
Add: MTBDDs with floats (CUDD ADDs)