1(* Copyright (C) 1997-2001 by Ken Friis Larsen and Jakob Lichtenberg. *) 2structure bvec :> bvec = 3struct 4 5 open MuddyCore 6 7 open bdd fdd 8 9 prim_type bvec 10 type const = int 11 12 val bvectrue: precision -> bvec = app1 (symb "mlbvec_true") 13 val bvecfalse: precision -> bvec = app1 (symb "mlbvec_false") 14 val con: precision -> const -> bvec = app2 (symb "mlbvec_con") 15 16 val var: precision -> varnum -> int -> bvec = app3 (symb "mlbvec_var") 17 val varfdd: fddvar -> bvec = app1 (symb "mlbvec_varfdd") 18 19 val coerce: precision -> bvec -> bvec = app2 (symb "mlbvec_coerce") 20 21 val isConst: bvec -> bool = app1 (symb "mlbvec_isconst") 22 val getConst: bvec -> const = app1 (symb "mlbvec_getconst") 23 24 fun lookupConst bvec = 25 if isConst bvec then SOME(getConst bvec) else NONE 26 27 val add: bvec * bvec -> bvec = cur2 (symb "mlbvec_add") 28 val sub: bvec * bvec -> bvec = cur2 (symb "mlbvec_sub") 29 30 val mul : bvec * bvec -> bvec = cur2 (symb "mlbvec_mul") 31 val mulfixed: bvec * const -> bvec = cur2 (symb "mlbvec_mulfixed") 32 33 val op div : bvec * bvec -> bvec * bvec = cur2 (symb "mlbvec_div") 34 val divfixed: bvec * const -> bvec * bvec = cur2 (symb "mlbvec_divfixed") 35 val divi = #1 o op div 36 val divifixed = #1 o divfixed 37 val modu = #2 o op div 38 val modufixed = #2 o divfixed 39 40(* val divifixed: bvec * const -> bvec = cur2 (symb "mlbvec_divi") 41 val modufixed: bvec * const -> bvec = cur2 (symb "mlbvec_modu") 42*) 43 val shl : bvec -> bvec -> bdd -> bvec = app3 (symb "mlbvec_shl") 44 val shlfixed: bvec -> int -> bdd -> bvec = app3 (symb "mlbvec_shlfixed") 45 46 val shr : bvec -> bvec -> bdd -> bvec = app3 (symb "mlbvec_shr") 47 val shrfixed: bvec -> int -> bdd -> bvec = app3 (symb "mlbvec_shrfixed") 48 49 val lth: bvec * bvec -> bdd = cur2 (symb "mlbvec_lth") 50 val lte: bvec * bvec -> bdd = cur2 (symb "mlbvec_lte") 51 val gth: bvec * bvec -> bdd = cur2 (symb "mlbvec_gth") 52 val gte: bvec * bvec -> bdd = cur2 (symb "mlbvec_gte") 53 val equ: bvec * bvec -> bdd = cur2 (symb "mlbvec_equ") 54 val neq: bvec * bvec -> bdd = cur2 (symb "mlbvec_neq") 55end 56