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