1(* Copyright (C) 1997-2001 by Ken Friis Larsen and Jakob Lichtenberg. *)
2structure bdd :> bdd =
3struct
4
5    prim_type bdd;
6    type varSet = bdd;
7    type assignment = bdd;
8    prim_type pairSet;
9    type composeSet = pairSet (* not the entire truth *)
10
11    type varnum = int
12
13    datatype bddop =
14        And | Xor | Or | Nand | Nor | Imp | Biimp | Diff | Lessth | Invimp
15
16
17    open MuddyCore
18
19    val constants_ : unit -> int * int * int * int
20                           * int * int * int * int
21                           * int * int
22                           * int * int * int * int * int * int * int * int
23                   = app1 (symb "mlbdd_constants")
24
25    val (bddop_and, bddop_xor, bddop_or, bddop_nand,
26         bddop_nor, bddop_imp, bddop_biimp, bddop_diff,
27         bddop_less, bddop_invimp,
28         FIXED, FREE, WIN2, WIN2ITE, SIFT, SIFTITE, RANDOM, REORDER_NONE)
29        = constants_ ()
30
31    val opr2i =
32        fn And    => bddop_and
33         | Xor    => bddop_xor
34         | Or     => bddop_or
35         | Nand   => bddop_nand
36         | Nor    => bddop_nor
37         | Imp    => bddop_imp
38         | Biimp  => bddop_biimp
39         | Diff   => bddop_diff
40         | Lessth => bddop_less
41         | Invimp => bddop_invimp
42
43    val apply_ : bdd -> bdd -> int -> bdd = app3 (symb "mlbdd_bdd_apply")
44    val exist_  : bdd -> varSet -> bdd    = app2 (symb "mlbdd_bdd_exist")
45    val forall_ : bdd -> varSet -> bdd    = app2 (symb "mlbdd_bdd_forall")
46    val appall_ : bdd -> bdd -> int -> varSet -> bdd
47                                          = app4 (symb "mlbdd_bdd_appall")
48    val appex_ : bdd -> bdd -> int -> varSet -> bdd
49                                          = app4 (symb "mlbdd_bdd_appex")
50
51    val mkset_ : varnum vector -> varSet  = app1 (symb "mlbdd_makeset")
52
53
54    val stats_ : unit -> int * int * int * int * int * int * int * int
55                                          = app1 (symb "mlbdd_bdd_stats")
56
57
58    val makepairset_ : varnum vector -> varnum vector -> pairSet
59                                          = app2 (symb "mlbdd_makepairset")
60
61    val makebddpairset_ : varnum vector -> bdd vector -> pairSet
62                                          = app2 (symb "mlbdd_makebddpairset")
63
64
65    val setVarnum : int -> unit = app1 (symb "mlbdd_bdd_setvarnum")
66    val getVarnum : unit -> int = app1 (symb "mlbdd_getvarnum")
67
68    val root : bdd -> int = app1 (symb "mlbdd_root")
69    val hash = root
70
71    val init : int -> int -> unit         = app2 (symb "mlbdd_bdd_init")
72    val done : unit -> unit               = app1 (symb "mlbdd_bdd_done")
73    val isRunning : unit -> bool          = app1 (symb "mlbdd_bdd_isrunning")
74
75    val ithvar : varnum -> bdd  = app1 (symb "mlbdd_bdd_ithvar")
76    val nithvar : varnum -> bdd = app1 (symb "mlbdd_bdd_nithvar")
77
78    val fromBool : bool -> bdd = app1 (symb "mlbdd_fromBool")
79    val toBool : bdd -> bool   = app1 (symb "mlbdd_toBool")
80
81    val var  : bdd -> varnum = app1 (symb "mlbdd_bdd_var")
82    val low  : bdd -> bdd    = app1 (symb "mlbdd_bdd_low")
83    val high : bdd -> bdd    = app1 (symb "mlbdd_bdd_high")
84
85    val TRUE = fromBool true
86    val FALSE = fromBool false
87
88    val equal : bdd -> bdd -> bool = app2 (symb "mlbdd_equal")
89
90    local fun C f x y = f y x in
91    val simplify : bdd -> bdd -> bdd = C (app2 (symb "mlbdd_bdd_simplify")) end
92
93    val printdot : bdd -> unit             = app1 (symb "mlbdd_bdd_printdot")
94    val fnprintdot : string -> bdd -> unit = app2 (symb "mlbdd_bdd_fnprintdot")
95
96    val printset : bdd -> unit             = app1 (symb "mlbdd_bdd_printset")
97    val fnprintset : string -> bdd -> unit = app2 (symb "mlbdd_bdd_fnprintset")
98
99    val bddSave : string -> bdd -> unit    = app2 (symb "mlbdd_bdd_fnsave")
100    val bddLoad : string -> bdd            = app1 (symb "mlbdd_bdd_fnload")
101
102
103    val satcount : bdd -> real = app1 (symb "mlbdd_bdd_satcount")
104
105    val nodecount : bdd -> int = app1 (symb "mlbdd_bdd_nodecount")
106
107    fun stats unit =
108        let val (p,nn,mn,fnum,minn,vn,cs,gn) = stats_ unit
109        in
110            {produced     = p,
111             nodenum      = nn,
112             maxnodenum   = mn,
113             freenodes    = fnum,
114             minfreenodes = minn,
115             varnum       = vn,
116             cachesize    = cs,
117             gbcnum       = gn}
118        end
119
120    fun makeset_ vector = if Vector.length vector = 0 then (*Obj.magic*) FALSE
121                          else mkset_ vector
122
123    fun nodup _ nil                   = nil
124      | nodup pre (h :: tail) = if pre = h then nodup pre tail
125                                        else h :: nodup h tail
126    fun makeset varlist =
127        let val positive = List.filter (fn i => i >= 0) varlist
128            val sorted = Listsort.sort Int.compare positive
129            val nodup  = case sorted of
130                             nil => nil
131                           | h :: tail => h :: nodup h tail
132        in
133            makeset_ (Vector.fromList(nodup))
134        end
135
136    val scanset : varSet -> varnum vector = app1 (symb "mlbdd_bdd_scanset")
137
138    val support : bdd -> varSet = app1 (symb "mlbdd_bdd_support")
139
140    val fromSet = fn x => x
141    val toSet_  = fn x => x
142
143    fun apply r1 r2 opr         = apply_ r1 r2 (opr2i opr)
144    fun exist vs r              = exist_ r vs
145    fun forall vs r             = forall_ r vs
146    fun appall r1 r2 opr varset = appall_ r1 r2 (opr2i opr) varset
147    fun appex r1 r2 opr varset  = appex_ r1 r2 (opr2i opr) varset
148
149
150    val NOT : bdd -> bdd  = app1 (symb "mlbdd_bdd_not")
151    val ITE : bdd -> bdd -> bdd -> bdd = app3(symb "mlbdd_bdd_ite")
152
153    fun AND (r1, r2)    = apply_ r1 r2 bddop_and
154    fun XOR (r1, r2)    = apply_ r1 r2 bddop_xor
155    fun OR (r1, r2)     = apply_ r1 r2 bddop_or
156    fun NAND (r1, r2)   = apply_ r1 r2 bddop_nand
157    fun NOR (r1, r2)    = apply_ r1 r2 bddop_nor
158    fun IMP (r1, r2)    = apply_ r1 r2 bddop_imp
159    fun BIIMP (r1, r2)  = apply_ r1 r2 bddop_biimp
160    fun DIFF (r1, r2)   = apply_ r1 r2 bddop_diff
161    fun LESSTH (r1, r2) = apply_ r1 r2 bddop_less
162    fun INVIMP (r1, r2) = apply_ r1 r2 bddop_invimp
163
164    val replace : bdd -> pairSet -> bdd = app2 (symb "mlbdd_bdd_replace")
165
166    fun makepairSet pl =
167        let val (old,new) = ListPair.unzip pl
168        in makepairset_ (vector old) (vector new) end
169
170    val compose_ : bdd -> bdd -> varnum -> bdd
171        = app3 (symb "mlbdd_bdd_compose")
172
173    fun compose (v,r2) r1 = compose_ r1 r2 v
174
175    val veccompose : pairSet -> bdd -> bdd = app2 (symb "mlbdd_bdd_veccompose")
176
177    fun composeSet pl =
178        let val (old, new) = ListPair.unzip pl
179        in  makebddpairset_ (vector old) (vector new) end
180
181
182    fun assign((v,b), res) = apply res (if b then ithvar v else nithvar v) And
183    val assignment = List.foldl assign TRUE
184    val fromAssignment = fn x => x
185    val toAssignment_ = fn x => x
186
187    fun isBool bdd = (toBool bdd; true) handle Domain => false
188
189    fun getAssignment bdd =
190        let fun loop bdd acc =
191                if isBool bdd then acc
192                else let val var = var bdd
193                         val low = low bdd
194                         val high = high bdd
195                     in  if equal low FALSE then loop high ((var,true) :: acc)
196                         else loop low ((var,false) :: acc)
197                     end
198        in  loop bdd [] end
199
200    val restrict : bdd -> bdd -> bdd = app2 (symb "mlbdd_bdd_restrict")
201
202    val satone_ : bdd -> assignment = app1 (symb "mlbdd_bdd_satone")
203    fun satone r = if equal r FALSE then raise Domain
204                   else satone_ r
205
206    val fullsatone_ : bdd -> assignment = app1 (symb "mlbdd_bdd_fullsatone")
207    fun fullsatone r = if equal r FALSE then raise Domain
208                   else fullsatone_ r
209
210    type nodetable = int * (varnum * int * int) Vector.vector
211
212
213    (* Three helper functions, used to normalize rootno *)
214    fun table size = (size, ref 0, Array.array(size,[]))
215    fun mem i []           = NONE
216      | mem i ((k,d) :: t) = if i = k then SOME d
217                             else mem i t
218    fun add (size,next,tab) r =
219        let val code = r mod size
220            val slot = Array.sub(tab,code)
221        in
222            case mem r slot of
223                NONE => let val n = !next
224                        in  next := n + 1;
225                            Array.update(tab, code, (r,n) :: slot);
226                            n
227                        end
228              | SOME n => n
229        end
230
231    fun nodetable r =
232        let val nc = nodecount r + 2
233            val rootno = add (table nc) o root
234            val tab = Array.array(nc,NONE)
235            fun peek i = Array.sub(tab, i)
236            fun update i d = Array.update(tab,i,SOME d)
237
238            fun node r =
239                let val root = rootno r
240                in
241                    case peek root of
242                        NONE   => let val low = low r
243                                      val high = high r
244                                  in  update root (var r,
245                                                   rootno low,
246                                                   rootno high);
247                                      node low;
248                                      node high
249                                  end
250                      | SOME _ => ()
251                end
252        in
253            update (rootno TRUE) (0,0,0);
254            update (rootno FALSE) (0,0,0);
255            node r;
256            (rootno r,
257             Vector.tabulate(nc, fn i => valOf(Array.sub(tab,i))))
258        end
259
260    (* BuDDy tuning stuff *)
261    val setMaxincrease : int -> int = app1 (symb "mlbdd_bdd_setmaxincrease")
262    val setCacheratio  : int -> int = app1 (symb "mlbdd_bdd_setcacheratio")
263
264    val setprintgc : bool -> string -> string -> unit =
265        app3 (symb "mlbdd_setprintgc")
266
267    fun verbosegc NONE           = setprintgc false "" ""
268      | verbosegc (SOME(s1, s2)) = setprintgc true s1 s2
269
270
271    (* Variable reordering stuff *)
272    type fixed = int
273    val addvarblock  : varnum -> varnum -> fixed -> unit
274        = app3 (symb "mlbdd_bdd_intaddvarblock")
275    val clrvarblocks  : unit -> unit = app1 (symb "mlbdd_bdd_clrvarblocks")
276
277
278    type method = int
279    val reorder     : method -> unit = app1 (symb "mlbdd_bdd_reorder")
280    val autoReorder : method -> method = app1 (symb "mlbdd_bdd_autoreorder")
281    val autoReorderTimes : method -> int -> method = app2 (symb "mlbdd_bdd_autoreorder_times")
282
283    val getMethod : unit -> method = app1 (symb "mlbdd_bdd_getreorder_method")
284    val getTimes  : unit -> int    = app1 (symb "mlbdd_bdd_getreorder_times")
285
286    val disableReorder : unit -> unit = app1 (symb "mlbdd_bdd_disable_reorder")
287    val enableReorder  : unit -> unit = app1 (symb "mlbdd_bdd_enable_reorder")
288
289    type level = int
290    val varToLevel : varnum -> level = app1 (symb "mlbdd_bdd_var2level")
291    val varAtLevel : level -> varnum = app1 (symb "mlbdd_bdd_level2var")
292
293end
294