-
Notifications
You must be signed in to change notification settings - Fork 2
/
cudd.mlpacki
119 lines (95 loc) · 4.69 KB
/
cudd.mlpacki
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
{2 Introduction}
User modules:
- {!Man}: CUDD managers;
- {!Bdd}: CUDD BDDs;
- {!Add}: CUDD ADDs;
- {!Mtbdd}, {!Mtbddc}: MTBDDs on OCaml values;
- {!Mapleaf}, {!User}: maps user operations from leaves to
MTBDDs on such leaves.
- {!Memo}, relying on {!Hash} and {!Cache}: allows the control
of memoization techniques, for permutation and vector composition functions
on BDDs and MTBDDs, and user operations.
Internal modules:
- {!Vdd}: MTBDDs on unhashed OCaml values;
- {!Custom}: for user operations on ADDs and MTBDDs;
- {!Weakke} and {!PWeakke}: for polymorphic weak hashtables.
This library provides an OCAML interface to the
{{:http://vlsi.colorado.edu/software.html}CUDD BDD library}, as well as
additional C functions to CUDD (in cuddauxXXX files). The reader is supposed
to have looked at the {{:http://vlsi.colorado.edu/~fabio/CUDD/}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.
{3 Memory management}
The diagrams are implemented as abstract types, and more precisely
as OCAML {e 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 {e d}ouble values at leaves) , which has the type
[Man.d Man.t], and one dedicated to BDDs and so-called VDDs, with OCaml {e
v}alues at leaves., which has the type [Man.v Man.t], see {!Man.d}, {!Man.v}
and {!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 {!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.
{3 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.
{3 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.
{3 Installation and Use}
See the [README] file.
You need:
{ul
{- {{:http://www.gnu.org/software/make}GNU Make}}
{- {{:http://caml.inria.fr}OBJECTIVE CAML 3.0}}
{- {{:http://caml.inria.fr/camlidl}CAMLIDL 1.05}}
{- {{:http://projects.camlcity.org/projects/findlib.html}FINDLIB}}
{- M4 preprocessor, SED, GREP
{{:http://www.gnu.org/software}GNU versions}}
}
{{:http://vlsi.colorado.edu/software.html}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.