1(* Copyright (C) 1997-2001 by Ken Friis Larsen and Jakob Lichtenberg. *)
2signature fdd =
3sig
4    type precision = int
5    type domain = int
6    type fddvar
7
8    val extDomain: domain list -> fddvar list
9    val clearAll: unit -> unit
10    val domainNum: unit -> int
11    val domainSize: fddvar -> domain
12    val varNum: fddvar -> precision
13    val vars: fddvar -> bdd.varnum list
14    val ithSet: fddvar -> bdd.varSet
15    val domain: fddvar -> bdd.bdd
16    val setPairs: (fddvar * fddvar) list -> bdd.pairSet
17end
18
19(* Structure fdd implements BuDDy's fdd functions.
20
21  Type [precision] is used to express the number of bits in an fdd.
22
23  Type [domain] is used to express a domain size.  A value n
24  represents a domain [0..(n-1)].
25
26  Type [fddvar] is the type of fdd variables.  An fdd variable
27  represents a set of bdd variables.
28
29  [extDomain [d1, ..., dn] ] returns a list of fddvars [v1, ... vn].
30  The domain di represents the domain of the i'th variable vi.  See
31  also [ordering].
32
33  [clearAll()], [domainNum() ], [domainSize v], [varNum v], [vars v],
34  [ithSet v], [domain v], [setPairs pairl]: see the Buddy
35  documentation.
36
37  The following table shows how ML types and values in this modules
38  relates to C types and function declarations in fdd.h:
39
40  MuDDy       BuDDy                   Comment
41  -----------------------------------------------------------------
42  Types:
43  precision   int
44  domain      int
45  fddvar      int
46
47  Values:
48  extDomain   fdd_extdomain
49  ?           fdd_overlapdomain
50  clearAll    fdd_clearall
51  domainNum   fdd_domainnum
52  domainSize  fdd_domainsize
53  varNum      fdd_varnum
54  vars        fdd_vars
55  ?           fdd_ithvar
56  ?           fdd_scanvar
57  ?           fdd_scanallvar
58  ithSet      fdd_ithset
59  domain      fdd_domain
60  ?           fdd_equals
61  ?           fdd_file_hook
62  ?           fdd_printset
63  ?           fdd_fprintset
64  ?           fdd_scanset
65  makeSet     fdd_makeset
66  ?           fdd_intaddvarblock
67  ?           fdd_setpair              (use setPair)
68  setPairs    fdd_setpairs
69*)
70