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