Module Cudd


module Cudd: sig .. end
Interface to CUDD library


Introduction

User modules:

Internal modules: This library provides an OCAML interface to the CUDD BDD library, as well as additional C functions to CUDD (in cuddauxXXX files). The reader is supposed to have looked at the user's manual of this library.

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

Module Cache: Local caches


module Cache: sig .. end

Module Memo: Memoization policy


module Memo: sig .. end

Module Man: CUDD Manager


module Man: sig .. end

Module Bdd: Binary Decision Diagrams


module Bdd: sig .. end

Module Vdd: MTBDDs with OCaml values (INTERNAL)


module Vdd: sig .. end

Module Custom: Type of identifiers


module Custom: sig .. end

Module Weakke: Hash tables of weak pointers.


module Weakke: sig .. end

Module PWeakke: Hash tables of weak pointers, parametrized polymorphic version.


module PWeakke: sig .. end

Module Mtbdd: MTBDDs with OCaml values


module Mtbdd: sig .. end

Module Mtbddc: MTBDDs with finalized OCaml values.


module Mtbddc: sig .. end

Module User: Custom operations for MTBDDs


module User: sig .. end

Module Mapleaf: Lifting operation on leaves to operations on MTBDDs


module Mapleaf: sig .. end

Module Add: MTBDDs with floats (CUDD ADDs)


module Add: sig .. end