module Cudd:Interface to CUDD librarysig
..end
User modules:
Cudd.Man
: CUDD managers;Cudd.Bdd
: CUDD BDDs;Cudd.Add
: CUDD ADDs;Cudd.Mtbdd
, Cudd.Mtbddc
: MTBDDs on OCaml values;Cudd.Mapleaf
, Cudd.User
: maps user operations from leaves to
MTBDDs on such leaves.Cudd.Memo
, relying on Cudd.Hash
and 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.Weakke
and 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.
Memory management
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 Cudd.Man.d
, Cudd.Man.v
and Cudd.Man.t
.
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.
The function Cudd.Man.set_gc
allows to tune the OCAML garbage
collection of diagrams and the link with the CUDD garbage
collection.
It is possible to apply to the diagrams the polymorphic comparison
test (Pervasives.compare
, from which are derived =,<=,>=,<,>
)
and polymorphic hash function (polymorphic Hashtbl.hash
). The
comparison function compares lexicographically the pair address
of the manager, address of the node
). The hash function returns
the address of the node.
This document
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 .idl
. CamlIDL
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 .c
, .h
, .ml
and .mli
.
cudd_caml.c
, cudd_caml.h
custom_caml.c
and custom_caml.h
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
See the README
file.
You need:
CUDD BDD library is now included in the distribution.
Flags should be properly set in Makefile.config
(starting from
Makefile.config.model
).
Also, the Make rules for some example.ml
file shows how to compile
a program with the interface.
Module
Hash
: User hashtables
module Hash:sig
..end
Cache
: Local cachesmodule Cache:sig
..end
Memo
: Memoization policymodule Memo:sig
..end
Man
: CUDD Managermodule Man:sig
..end
Bdd
: Binary Decision Diagramsmodule Bdd:sig
..end
Vdd
: MTBDDs with OCaml values (INTERNAL)module Vdd:sig
..end
Custom
: Type of identifiersmodule Custom:sig
..end
Weakke
: Hash tables of weak pointers.module Weakke:sig
..end
PWeakke
: Hash tables of weak pointers, parametrized polymorphic version.module PWeakke:sig
..end
Mtbdd
: MTBDDs with OCaml valuesmodule Mtbdd:sig
..end
Mtbddc
: MTBDDs with finalized OCaml values.module Mtbddc:sig
..end
User
: Custom operations for MTBDDsmodule User:sig
..end
Mapleaf
: Lifting operation on leaves to operations on MTBDDsmodule Mapleaf:sig
..end
Add
: MTBDDs with floats (CUDD ADDs)module Add:sig
..end