Module Cudd

module Cudd: sig .. end

Interface to CUDD library

Introduction

User modules:

Cudd.Man: CUDD managers;
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.

Internal modules:

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.

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

Module Cudd

Introduction

Memory management

This document

Organization of the code

Installation and Use

Module Hash: User hashtables

Module Cache: Local caches

Module Memo: Memoization policy

Module Man: CUDD Manager

Module Bdd: Binary Decision Diagrams

Module Vdd: MTBDDs with OCaml values (INTERNAL)

Module Custom: Type of identifiers

Module Weakke: Hash tables of weak pointers.

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

Module Mtbdd: MTBDDs with OCaml values

Module Mtbddc: MTBDDs with finalized OCaml values.

Module User: Custom operations for MTBDDs

Module Mapleaf: Lifting operation on leaves to operations on MTBDDs

Module Add: MTBDDs with floats (CUDD ADDs)