(* * This file is a component of PropPlan - a model-based planner * Copyright (C) 2000-2007 Michael Paul Fourman * homepages.inf.ed.ac.uk/mfourman/tools/propplan * sourceforge.net/projects/propplan * michael.fourman (AT) gmail.com * * This program is free software: you can redistribute it and/or modify * it under the terms of version 3 of the GNU Affero General Public License * as published by the Free Software Foundation. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU Affero General Public License for more details. * * You should have received the file COPYING, a copy of the GNU Affero * Public License, along with this program. * If not, see . * $Id: BUDDY.ML,v 1.2 2007/12/31 19:56:32 michaelfourman Exp $ *) signature BUDDY = sig eqtype Var eqtype Bdd eqtype Vars type BddPair (* type bddStat type bddGbcStat *) type Method val DEFAULT_REORDERING : Method exception Error of string datatype 'a Option = None | Some of 'a val V : Var -> Bdd val I : Var -> int val Var : int -> Var val Vs : Var list -> Vars val TRUE : unit -> Bdd val FALSE : unit -> Bdd val bdd_addref : Bdd -> Bdd val bdd_and : Bdd -> Bdd -> Bdd val bdd_appall : Bdd -> Bdd -> int -> Bdd -> Bdd val bdd_appex : Bdd -> Bdd -> int -> Bdd -> Bdd val bdd_appuni : Bdd -> Bdd -> int -> Bdd -> Bdd val bdd_autoreorder : Method -> int val bdd_biimp : Bdd -> Bdd -> Bdd (* val bdd_cachestats : unit -> BddCacheStat *) val bdd_clear_error : unit -> unit val bdd_compose : Bdd -> Bdd -> Var -> Bdd val bdd_constrain : Bdd -> Bdd -> Bdd val bdd_default_errhandler : int -> unit (*val bdd_default_printstat : unit -> unit*) val bdd_delref : Bdd -> Bdd val bdd_disable_reorder : unit -> unit val bdd_done : unit -> unit val bdd_enable_reorder : unit -> unit val bdd_errstring : int -> string val bdd_exist : Bdd -> Vars -> Bdd val bdd_extvarnum : int -> int val bdd_false : unit -> Bdd val bdd_forall : Bdd -> Vars -> Bdd val bdd_freepair : BddPair -> unit val bdd_fullsatone : Bdd -> Bdd val bdd_gbc : unit -> unit val bdd_getallocnum : unit -> int val bdd_getnodenum : unit -> int val bdd_getreorder_method : unit -> int val bdd_getreorder_times : unit -> int val bdd_high : Bdd -> Bdd val bdd_imp : Bdd -> Bdd -> Bdd val bdd_init : {nodesize: int, cachesize: int} -> bool val bdd_isrunning : unit -> bool val bdd_ite : Bdd -> Bdd -> Bdd -> Bdd val bdd_ithvar : Var -> Bdd val bdd_level2var : int -> int val bdd_low : Bdd -> Bdd val bdd_newpair : unit -> BddPair val bdd_nithvar : Var -> Bdd val bdd_nodecount : Bdd -> int val bdd_not : Bdd -> Bdd val bdd_or : Bdd -> Bdd -> Bdd val bdd_pathcount : Bdd -> real val bdd_printdot : Bdd -> unit val bdd_printset : Bdd -> unit val bdd_printstat : unit -> unit val bdd_printtable : Bdd -> unit val bdd_reorder : Method -> unit val bdd_reorder_gain : unit -> int val bdd_reorder_verbose : int -> int val bdd_replace : Bdd -> BddPair -> Bdd val bdd_resetpair : BddPair -> unit val bdd_restrict : Bdd -> Bdd -> Bdd val bdd_relprod : Bdd -> Bdd -> Vars -> Bdd val bdd_satcount : Bdd -> real val bdd_satcountln : Bdd -> real val bdd_satcountlnset : Bdd -> Bdd -> real val bdd_satcountset : Bdd -> Bdd -> real val bdd_satone : Bdd -> Bdd val bdd_satoneset : Bdd -> Bdd -> Bdd -> Bdd val bdd_setbddpair : BddPair -> Var -> Bdd -> bool val bdd_setbddpairs : (Var * Bdd) list -> BddPair val bdd_setcacheratio : int -> int val bdd_setmaxincrease : int -> int val bdd_setmaxnodenum : int -> int val bdd_setminfreenodes : int -> int val bdd_setpair : BddPair -> Var -> Var -> bool val bdd_setpairs : (Var * Var) list -> BddPair val bdd_setvarnum : int -> int val bdd_simplify : Bdd -> Bdd -> Bdd val bdd_start : unit -> unit (* val bdd_stats : unit ->BddStat *) val bdd_support : Bdd -> Bdd val bdd_true : unit -> Bdd val bdd_unique : Bdd -> Bdd -> Bdd val bdd_var : Bdd -> Var val bdd_var2level : int -> int val bdd_varlevel : int -> int val bdd_varnum : unit -> int val bdd_veccompose : Bdd -> BddPair -> Bdd val bdd_versionnum : unit -> int val bdd_versionstr : unit -> string val bdd_xor : Bdd -> Bdd -> Bdd (*val bdd_xnor bdd_nand *) end functor BUDDY():BUDDY = struct local open CInterface in datatype 'a Option = None | Some of 'a exception Error of string val bddlib = ref (None : dylib Option) fun bdd_start() = case !bddlib of None => bddlib := Some (CInterface.load_lib ("/usr/local/lib/libbdd.dylib")) | _ => (); fun get s = case !bddlib of Some lib => load_sym lib s | None => (bdd_start(); get s); datatype Var = Var of int datatype Bdd = Bdd of int datatype Vars = Vars of int datatype BddPair = BddPair of vol fun TRUE () = Bdd 1 fun FALSE () = Bdd 0 val (fromCbool,toCbool,_) = breakConversion BOOL fun notNULL v = fromCbool v val VARS = mkConversion (Vars o fromCint) (fn (Vars b) => toCint b) Cint; val VAR = mkConversion (Var o fromCint) (fn (Var b) => toCint b) Cint; val BDD = mkConversion (Bdd o fromCint) (fn (Bdd b) => toCint b) Cint; val PAIR = STRUCT4 (BDD, INT, INT, POINTER); (* val BDDM = mkConversion Bddm (fn (Bddm m) => m) (Cpointer Cvoid); val ASSOC = mkConversion (Assoc o fromCint) (fn (Assoc n) => toCint n) Cint val SUBST = mkConversion (Subst o fromCint) (fn (Subst n) => toCint n) Cint val PAIR = STRUCT2(VAR,BDD) *) val (fromCvar, toCvar, Cvar) = breakConversion VAR val (fromCbdd, toCbdd, Cbdd) = breakConversion BDD fun bdd_init {nodesize, cachesize} = call2 (get "bdd_init") (INT, INT) BOOL (nodesize, cachesize) fun bdd_done () = call0 (get "bdd_done") () VOID () fun bdd_setvarnum n = call1 (get "bdd_setvarnum") INT INT n fun bdd_extvarnum n = call1 (get "bdd_extvarnum") INT INT n fun bdd_isrunning () = call0 (get "bdd_isrunning") () BOOL () fun bdd_setmaxnodenum n = call1 (get "bdd_setmaxnodenum") INT INT n fun bdd_setmaxincrease n = call1 (get "bdd_setmaxincrease") INT INT n fun bdd_setminfreenodes n = call1 (get "bdd_setminfreenodes") INT INT n fun bdd_getnodenum () = call0 (get "bdd_getnodenum") () INT () fun bdd_getallocnum () = call0 (get "bdd_getallocnum") () INT () fun bdd_versionstr () = call0 (get "bdd_versionstr") () STRING () fun bdd_versionnum () = call0 (get "bdd_versionnum") () INT () (* extern void bdd_stats(bddStat* ); extern void bdd_cachestats(bddCacheStat* ); extern void bdd_fprintstat(FILE* ); extern void bdd_default_gbchandler(int, bddGbcStat* ); *) (*fun bdd_default_printstat () = call0 (get "bdd_default_printstat") () VOID ()*) fun bdd_default_errhandler n = call1 (get "bdd_default_errhandler") INT VOID n fun bdd_errstring n = call1 (get "bdd_errstring") INT STRING n fun bdd_clear_error () = call0 (get "bdd_clear_error") () VOID () fun bdd_true () = call0 (get "bdd_true") () BDD () fun bdd_false () = call0 (get "bdd_false") () BDD () fun bdd_varnum () = call0 (get "bdd_varnum") () INT () fun bdd_ithvar n = call1 (get"bdd_ithvar") VAR BDD n val V = bdd_ithvar fun I (Var v) = v fun bdd_nithvar n = call1 (get"bdd_nithvar") VAR BDD n fun bdd_var b = call1 (get"bdd_var") BDD VAR b fun bdd_low b = call1 (get "bdd_low") BDD BDD b fun bdd_high b = call1 (get "bdd_high") BDD BDD b fun bdd_varlevel n = call1 (get "bdd_varlevel") INT INT n fun bdd_addref b = call1 (get "bdd_addref") BDD BDD b fun bdd_delref b = call1 (get "bdd_delref") BDD BDD b fun bdd_gbc () = call0 (get "bdd_gbc") () VOID () (*Need to encapsulate this*) fun bdd_newpair () = BddPair (call0 (get "bdd_newpair") () POINTER ()) fun bdd_setpair (BddPair p) old new = call3 (get "bdd_setpair") (POINTER, VAR, VAR) BOOL (p, old, new) fun bdd_setbddpair (BddPair p) old new = call3 (get "bdd_setpair") (POINTER, VAR, BDD) BOOL (p, old, new) fun bdd_freepair (BddPair p) = call1 (get "bdd_freepair") POINTER VOID p fun bdd_resetpair (BddPair p) = call1 (get "bdd_resetpair") POINTER VOID p fun bdd_setpairs ps = let val pair = bdd_newpair() fun addPairs [] = pair | addPairs ((old,new)::t) = (bdd_setpair pair old new; addPairs t) in addPairs ps end fun bdd_setbddpairs ps = let val pair = bdd_newpair() fun addPairs [] = pair | addPairs ((old,new)::t) = (bdd_setbddpair pair old new; addPairs t) in addPairs ps end (* extern int bdd_scanset(BDD, int**, int* ); extern BDD bdd_makeset(int *, int); extern bddPair* bdd_newpair(void); extern int bdd_setpair(bddPair*, int, int); extern int bdd_setpairs(bddPair*, int*, int*, int); extern int bdd_setbddpair(bddPair*, int, BDD); extern int bdd_setbddpairs(bddPair*, int*, BDD*, int); extern void bdd_resetpair(bddPair* ); extern void bdd_freepair(bddPair* ); *) (* /* In bddop.c */ *) fun bdd_setcacheratio n = call1 (get "bdd_setcacheratio") INT INT n (* extern BDD bdd_buildcube(int, int, BDD* ); extern BDD bdd_ibuildcube(int, int, int* ); *) fun bdd_not b = call1 (get "bdd_not") BDD BDD b (*extern BDD bdd_apply(BDD, BDD, int);*) fun bdd_and l r = call2 (get "bdd_and") (BDD, BDD) BDD (l, r) fun bdd_or l r = call2 (get "bdd_or") (BDD, BDD) BDD (l, r) fun bdd_xor l r = call2 (get "bdd_xor") (BDD, BDD) BDD (l, r) fun bdd_imp l r = call2 (get "bdd_imp") (BDD, BDD) BDD (l, r) fun bdd_biimp l r = call2 (get "bdd_biimp") (BDD, BDD) BDD (l, r) fun bdd_ite f g h = call3 (get "bdd_ite") (BDD, BDD, BDD) BDD (f, g, h) fun Vs xs = (* This is the only way to make Vars *) let fun vs [] = TRUE() | vs (x :: t) = let val vst = vs t val vsxt = bdd_addref(bdd_and (V x) vst) in (bdd_delref vst; vsxt) end val (Bdd b) = vs xs in Vars b end fun bdd_relprod f g xs = call4 (get "bdd_appex") (BDD, BDD, INT, VARS) BDD (f, g, 0, xs) fun bdd_restrict l r = call2 (get "bdd_restrict") (BDD, BDD) BDD (l, r) fun bdd_constrain l r = call2 (get "bdd_constrain") (BDD, BDD) BDD (l, r) fun bdd_replace b (BddPair p) = call2 (get "bdd_replace") (BDD, POINTER) BDD (b, address p) fun bdd_compose f g h = call3 (get "bdd_compose") (BDD, BDD, VAR) BDD (f, g, h) fun bdd_veccompose b (BddPair p) = call2 (get "bdd_veccompose") (BDD, POINTER) BDD (b, address p) fun bdd_simplify l r = call2 (get "bdd_simplify") (BDD, BDD) BDD (l, r) fun bdd_exist l r = call2 (get "bdd_exist") (BDD, VARS) BDD (l, r) fun bdd_forall l r = call2 (get "bdd_forall") (BDD, VARS) BDD (l, r) fun bdd_unique l r = call2 (get "bdd_unique") (BDD, BDD) BDD (l, r) fun bdd_appex left right opn var = call4 (get "bdd_appex") (BDD, BDD, INT, BDD) BDD (left, right, opn, var) fun bdd_appall left right opn var = call4 (get "bdd_appall") (BDD, BDD, INT, BDD) BDD (left, right, opn, var) fun bdd_appuni left right opn var = call4 (get "bdd_appuni") (BDD, BDD, INT, BDD) BDD (left, right, opn, var) fun bdd_support b = call1 (get "bdd_support") BDD BDD b fun bdd_satone b = call1 (get "bdd_satone") BDD BDD b fun bdd_satoneset f g h = call3 (get "bdd_satoneset") (BDD, BDD, BDD) BDD (f, g, h) fun bdd_fullsatone b = call1 (get "bdd_fullsatone") BDD BDD b (* extern void bdd_allsat(BDD r, bddallsathandler handler); *) fun bdd_satcount b = call1 (get "bdd_satcount") BDD DOUBLE b fun bdd_satcountset b vars = call2 (get "bdd_satcountset") (BDD, BDD) DOUBLE (b, vars) fun bdd_satcountln b = call1 (get "bdd_satcountln") BDD DOUBLE b fun bdd_satcountlnset b vars = call2 (get "bdd_satcountlnset") (BDD, BDD) DOUBLE (b, vars) fun bdd_nodecount b = call1 (get "bdd_nodecount") BDD INT b (* extern int bdd_anodecount(BDD *, int); extern int* bdd_varprofile(BDD); *) fun bdd_pathcount b = call1 (get "bdd_pathcount") BDD DOUBLE b (* In file "bddio.c" *) fun bdd_printtable () = call0 (get"bdd_printtable") () VOID () (* extern void bdd_printall(void); extern void bdd_fprintall(FILE* ); extern void bdd_fprinttable(FILE *, BDD); *) fun bdd_printtable b = call1 (get"bdd_printtable") BDD VOID b (* extern void bdd_fprintset(FILE *, BDD); *) fun bdd_printset b = call1 (get"bdd_printset") BDD VOID b (* extern int bdd_fnprintdot(char *, BDD); extern void bdd_fprintdot(FILE *, BDD); *) fun bdd_printdot b = call1 (get"bdd_printdot") BDD VOID b fun bdd_printstat () = call0 (get"bdd_printstat") () VOID () (* fun bdd_fnsave fname b* = call2ret1 (get"bdd_fnsave") STRING BDD (fname, bptr) extern int bdd_fnsave(char *, BDD); extern int bdd_save(FILE *, BDD); extern int bdd_fnload(char *, BDD* ); extern int bdd_load(FILE *ifile, BDD* ); *) (* In file reorder.c *) datatype Method = BDD_REORDER_NONE | BDD_REORDER_WIN2 | BDD_REORDER_WIN2ITE | BDD_REORDER_SIFT | BDD_REORDER_SIFTITE | BDD_REORDER_WIN3 | BDD_REORDER_WIN3ITE | BDD_REORDER_RANDOM val DEFAULT_REORDERING = BDD_REORDER_WIN2ITE fun method BDD_REORDER_NONE = 0 | method BDD_REORDER_WIN2 = 1 | method BDD_REORDER_WIN2ITE = 2 | method BDD_REORDER_SIFT = 3 | method BDD_REORDER_SIFTITE = 4 | method BDD_REORDER_WIN3 = 5 | method BDD_REORDER_WIN3ITE = 6 | method BDD_REORDER_RANDOM = 7 (* #define BDD_REORDER_NONE 0 #define BDD_REORDER_WIN2 1 #define BDD_REORDER_WIN2ITE 2 #define BDD_REORDER_SIFT 3 #define BDD_REORDER_SIFTITE 4 #define BDD_REORDER_WIN3 5 #define BDD_REORDER_WIN3ITE 6 #define BDD_REORDER_RANDOM 7 #define BDD_REORDER_FREE 0 #define BDD_REORDER_FIXED 1 *) (* 00052 #define bddop_and 0 00053 #define bddop_xor 1 00054 #define bddop_or 2 00055 #define bddop_nand 3 00056 #define bddop_nor 4 00057 #define bddop_imp 5 00058 #define bddop_biimp 6 00059 #define bddop_diff 7 00060 #define bddop_less 8 00061 #define bddop_invimp 9 *) (* Error Codes #define BDD_MEMORY (-1) /* Out of memory */ #define BDD_VAR (-2) /* Unknown variable */ #define BDD_RANGE (-3) /* Variable value out of range (not in domain) */ #define BDD_DEREF (-4) /* Removing external reference to unknown node */ #define BDD_RUNNING (-5) /* Called bdd_init() twice whithout bdd_done() */ #define BDD_FILE (-6) /* Some file operation failed */ #define BDD_FORMAT (-7) /* Incorrect file format */ #define BDD_ORDER (-8) /* Vars. not in order for vector based functions */ #define BDD_BREAK (-9) /* User called break */ #define BDD_VARNUM (-10) /* Different number of vars. for vector pair */ #define BDD_NODES (-11) /* Tried to set max. number of nodes to be fewer */ /* than there already has been allocated */ #define BDD_OP (-12) /* Unknown operator */ #define BDD_VARSET (-13) /* Illegal variable set */ #define BDD_VARBLK (-14) /* Bad variable block operation */ #define BDD_DECVNUM (-15) /* Trying to decrease the number of variables */ #define BDD_REPLACE (-16) /* Replacing to already existing variables */ #define BDD_NODENUM (-17) /* Number of nodes reached user defined maximum */ #define BDD_ILLBDD (-18) /* Illegal bdd argument */ #define BDD_SIZE (-19) /* Illegal size argument */ #define BVEC_SIZE (-20) /* Mismatch in bitvector size */ #define BVEC_SHIFT (-21) /* Illegal shift-left/right parameter */ #define BVEC_DIVZERO (-22) /* Division by zero */ #define BDD_ERRNUM 24 *) (* extern int bdd_swapvar(int v1, int v2); *) fun bdd_reorder m = call1 (get "bdd_reorder") INT VOID (method m) fun bdd_reorder_gain () = call0 (get "bdd_reorder_gain") () INT () (* extern bddsizehandler bdd_reorder_probe(bddsizehandler); extern void bdd_clrvarblocks(void); extern int bdd_addvarblock(BDD, int); extern int bdd_intaddvarblock(int, int, int); extern void bdd_varblockall(void); extern bddfilehandler bdd_blockfile_hook(bddfilehandler); *) fun bdd_autoreorder m = call1 (get "bdd_autoreorder") INT INT (method m) fun bdd_var2level n = call1 (get "bdd_var2level") INT INT n fun bdd_level2var n = call1 (get "bdd_level2var") INT INT n fun bdd_getreorder_times () = call0 (get "bdd_getreorder_times") () INT () fun bdd_getreorder_method () = call0 (get "bdd_getreorder_method") () INT () fun bdd_enable_reorder () = call0 (get "bdd_enable_reorder") () VOID () fun bdd_disable_reorder () = call0 (get "bdd_disable_reorder") () VOID () fun bdd_reorder_verbose n = call1 (get "bdd_reorder_verbose") INT INT n (* extern void bdd_setvarorder(int* ); extern void bdd_printorder(void); extern void bdd_fprintorder(FILE* ); *) (**************************************************************************************) (* assoc in C is created from an array of pointers to variables *) (* we deal with lists of variables *) fun fill CONV = let val (fromCtype, toCtype, Ctype) = breakConversion CONV fun f p [] = (assign Ctype p (toCbool false)) | f p (x :: xs) = (assign Ctype p (toCtype x); f (offset 1 Ctype p) xs ) in f end fun extract CONV = let val (fromCtype, toCtype, Ctype) = breakConversion CONV fun e p = if notNULL p then fromCtype p :: e (offset 1 Ctype p) else [] in e end fun block CONV n = let val (fromCtype, toCtype, Ctype) = breakConversion CONV in alloc (n+1) Ctype end; fun LIST CONV = let fun length [] = 0 | length (_:: xs) = 1 + length xs; val (_,_, Ctype) = breakConversion CONV fun fromClist v = extract CONV v fun toClist xs = let val p = block CONV (length xs) in fill CONV p xs; p end in mkConversion (fromClist o deref) (address o toClist) (Cpointer Ctype) end; (* fun bdd_new_assoc m a = call3 (get "bdd_new_assoc") (BDDM, LIST VAR, INT) ASSOC (m,a,0) fun bdd_free_assoc m a = call2 (get "bdd_free_assoc") (BDDM,ASSOC) VOID (m,a) fun bdd_assoc m a = call2 (get "bdd_assoc") (BDDM,ASSOC) VOID (m,a) fun length [] = 0 | length (_ :: t) = 1 + length t; fun bdd_new_subst m a = call3 (get "bdd_new_assoc") (BDDM, LIST PAIR, INT) SUBST (m,a,length a) fun bdd_free_subst m a = call2 (get "bdd_free_assoc") (BDDM,SUBST) VOID (m,a) fun bdd_subst m a = call2 (get "bdd_assoc") (BDDM,SUBST) VOID (m,a) fun bdd_exists m f = call2 (get "bdd_exists") (VARS,BDD) BDD (m,f) fun bdd_forall m f = call2 (get "bdd_forall") (BDDM,BDD) BDD (m,f) fun bdd_rel_prod m f g = call3 (get "bdd_rel_prod") (BDDM,BDD,VARS) BDD (m,f,g) fun bdd_compose m f g h = call4 (get "bdd_compose") (BDDM,BDD,VAR,BDD) BDD (m,f,g,h) fun bdd_substitute m f = call2 (get "bdd_substitute") (BDDM,BDD) BDD (m,f) fun bdd_reduce m f g = call3 (get "bdd_reduce") (BDDM,BDD,BDD) BDD (m,f,g) fun bdd_cofactor m f g = call3 (get "bdd_cofactor") (BDDM,BDD,BDD) BDD (m,f,g) fun bdd_depends_on m f v = call3 (get "bdd_depends_on") (BDDM,BDD,VAR) BOOL (m,f,v) fun bdd_support m f = let val table = block VAR (bdd_vars m + 1) in call3 (get "bdd_support") (BDDM, BDD, POINTER) VOID (m, f, address table); extract VAR table end fun bdd_satisfy m f = call2 (get "bdd_satisfy") (BDDM, BDD) BDD (m,f) fun bdd_satisfy_support m f = call2 (get "bdd_satisfy_support") (BDDM, BDD) BDD (m,f) fun bdd_satisfying_fraction m f =call2 (get "bdd_satisfying_fraction") (BDDM,BDD) DOUBLE (m,f) fun bdd_total_size m = call1 (get "bdd_total_size") (BDDM) LONG (m) ; fun bdd_size m f b = call3 (get "bdd_size") (BDDM,BDD,BOOL) LONG (m,f,b) ; fun bdd_size_multiple m fs b = call3 (get "bdd_size_multiple") (BDDM,LIST BDD,BOOL) LONG (m,fs,b) ; fun bdd_free m f = call2 (get "bdd_free") (BDDM, BDD) VOID (m,f) fun bdd_stats m = call1 (get "bdd_stats") (BDDM) VOID m local fun method SIFT = volOfSym (get "bdd_reorder_sift") | method STABLE_WINDOW = volOfSym (get "bdd_reorder_stable_window3") | method NONE = toCbool false (*volOfSym (get "bdd_reorder_none")*) in fun bdd_dynamic_reordering m r = call2 (get "bdd_dynamic_reordering") (BDDM, POINTER) VOID (m, method r) end fun bdd_gc m = call1 (get "bdd_gc") (BDDM) VOID m fun bdd_reorder m = call1 (get "bdd_reorder") (BDDM) VOID m fun bdd_var_with_index m i = call2 (get "bdd_var_with_index") (BDDM, LONG) VAR (m,i) fun bdd_cache_ratio m i = call2 (get "bdd_cache_ratio") (BDDM, INT) INT (m,i) *) end end;