formal_lp/old/arith/arith_cache.hl

   1 (*****************************)
   2 (* Cached natural arithmetic *)
   3 (*****************************)
   4
   5 (* Dependencies *)
   6 needs "../formal_lp/arith/arith_options.hl";;
   7 needs ("../formal_lp/arith/"^(if Arith_options.binary then "arith_hash.hl" else "arith_hash2.hl"));;
   8
   9
  10 module Arith_cache = struct
  11
  12 (* Hash tables *)
  13 let cache_size = if Arith_options.cached then 10000 else 1;;
  14 let max_cache_size = cache_size * 2;;
  15
  16 let my_add h key v =
  17   if Hashtbl.length h >= max_cache_size then
  18     let _ = Hashtbl.clear h in
  19       print_string "Clearing a nat hash table"
  20   else
  21     ();
  22   Hashtbl.add h key v;;
  23
  24 let le_table = Hashtbl.create cache_size and
  25     add_table = Hashtbl.create cache_size and
  26     sub_table = Hashtbl.create cache_size and
  27     sub_le_table = Hashtbl.create cache_size and
  28     mul_table = Hashtbl.create cache_size and
  29     div_table = Hashtbl.create cache_size;;
  30
  31 (* Counters for collecting stats *)
  32 let suc_counter = ref 0 and
  33     eq0_counter = ref 0 and
  34     pre_counter = ref 0 and
  35     gt0_counter = ref 0 and
  36     lt_counter = ref 0 and
  37     le_counter = ref 0 and
  38     add_counter = ref 0 and
  39     sub_counter = ref 0 and
  40     sub_le_counter = ref 0 and
  41     mul_counter = ref 0 and
  42     div_counter = ref 0 and
  43     even_counter = ref 0 and
  44     odd_counter = ref 0;;
  45
  46
  47 (* Clears all cached results *)
  48 let reset_cache () =
  49   let clear = Hashtbl.clear in
  50     clear le_table;
  51     clear add_table;
  52     clear sub_table;
  53     clear sub_le_table;
  54     clear mul_table;
  55     clear div_table;;
  56
  57
  58 (* Resets all counters *)
  59 let reset_stat () =
  60   suc_counter := 0;
  61   eq0_counter := 0;
  62   pre_counter := 0;
  63   gt0_counter := 0;
  64   lt_counter := 0;
  65   le_counter := 0;
  66   add_counter := 0;
  67   sub_counter := 0;
  68   sub_le_counter := 0;
  69   mul_counter := 0;
  70   div_counter := 0;
  71   even_counter := 0;
  72   odd_counter := 0;;
  73
  74 (* Prints stats *)
  75 let print_stat () =
  76   let len = Hashtbl.length in
  77   let suc_pre_str = sprintf "suc = %d\npre = %d\n" !suc_counter !pre_counter in
  78   let cmp0_str = sprintf "eq0 = %d\ngt0 = %d\n" !eq0_counter !gt0_counter in
  79   let lt_str = sprintf "lt = %d\n" !lt_counter in
  80   let even_odd_str = sprintf "even = %d\nodd = %d\n" !even_counter !odd_counter in
  81   let le_str = sprintf "le = %d (le_hash = %d)\n" !le_counter (len le_table) in
  82   let add_str = sprintf "add = %d (add_hash = %d)\n" !add_counter (len add_table) in
  83   let sub_str = sprintf "sub = %d (sub_hash = %d)\n" !sub_counter (len sub_table) in
  84   let sub_le_str = sprintf "sub_le = %d (sub_le_hash = %d)\n" !sub_le_counter (len sub_le_table) in
  85   let mul_str = sprintf "mul = %d (mul_hash = %d)\n" !mul_counter (len mul_table) in
  86   let div_str = sprintf "div = %d (div_hash = %d)\n" !div_counter (len div_table) in
  87     print_string (suc_pre_str ^ cmp0_str ^ lt_str ^ even_odd_str ^
  88                     le_str ^ add_str ^ sub_str ^ sub_le_str ^ mul_str ^ div_str);;
  89
  90
  91 (* Note: the standard Hashtbl.hash function works very purely on terms *)
  92 let rec num_tm_hash tm =
  93   if is_comb tm then
  94     let b_tm, n_tm = dest_comb tm in
  95     let str = (fst o dest_const) b_tm in
  96       str ^ num_tm_hash n_tm
  97   else
  98     "";;
  99
 100 let op_tm_hash tm =
 101   let lhs, tm2 = dest_comb tm in
 102   let tm1 = rand lhs in
 103     num_tm_hash tm1 ^ "x" ^ num_tm_hash tm2;;
 104
 105
 106 let tm1_tm2_hash tm1 tm2 =
 107   num_tm_hash tm1 ^ "x" ^ num_tm_hash tm2;;
 108
 109
 110 (* SUC *)
 111 let raw_suc_conv_hash tm =
 112   let _ = suc_counter := !suc_counter + 1 in
 113 (*  let _ = suc_list := tm :: !suc_list in *)
 114     Arith_hash.raw_suc_conv_hash tm;;
 115
 116 (* x = 0 *)
 117 let raw_eq0_hash_conv tm =
 118   let _ = eq0_counter := !eq0_counter + 1 in
 119 (*  let _ = eq0_list := tm :: !eq0_list in *)
 120     Arith_hash.raw_eq0_hash_conv tm;;
 121
 122 (* PRE *)
 123 let raw_pre_hash_conv tm =
 124   let _ = pre_counter := !pre_counter + 1 in
 125     Arith_hash.raw_pre_hash_conv tm;;
 126
 127 (* x > 0 *)
 128 let raw_gt0_hash_conv tm =
 129   let _ = gt0_counter := !gt0_counter + 1 in
 130     Arith_hash.raw_gt0_hash_conv tm;;
 131
 132 (* x < y *)
 133 let raw_lt_hash_conv tm =
 134   let _ = lt_counter := !lt_counter + 1 in
 135     Arith_hash.raw_lt_hash_conv tm;;
 136
 137 (* x <= y *)
 138 let raw_le_hash_conv tm =
 139   let _ = le_counter := !le_counter + 1 in
 140   let hash = op_tm_hash tm in
 141     try
 142       Hashtbl.find le_table hash
 143     with Not_found ->
 144       let result = Arith_hash.raw_le_hash_conv tm in
 145       let _ = my_add le_table hash result in
 146         result;;
 147
 148 (* x + y *)
 149 let raw_add_conv_hash tm =
 150   let _ = add_counter := !add_counter + 1 in
 151   let hash = op_tm_hash tm in
 152     try
 153       Hashtbl.find add_table hash
 154     with Not_found ->
 155       let result = Arith_hash.raw_add_conv_hash tm in
 156       let _ = my_add add_table hash result in
 157         result;;
 158
 159 (* x - y *)
 160 let raw_sub_hash_conv tm =
 161   let _ = sub_counter := !sub_counter + 1 in
 162   let hash = op_tm_hash tm in
 163     try
 164       Hashtbl.find sub_table hash
 165     with Not_found ->
 166       let result = Arith_hash.raw_sub_hash_conv tm in
 167       let _ = my_add sub_table hash result in
 168         result;;
 169
 170 let raw_sub_and_le_hash_conv tm1 tm2 =
 171   let _ = sub_le_counter := !sub_le_counter + 1 in
 172   let hash = tm1_tm2_hash tm1 tm2 in
 173     try
 174       Hashtbl.find sub_le_table hash
 175     with Not_found ->
 176       let result = Arith_hash.raw_sub_and_le_hash_conv tm1 tm2 in
 177       let _ = my_add sub_le_table hash result in
 178         result;;
 179
 180 (* x * y *)
 181 let raw_mul_conv_hash tm =
 182   let _ = mul_counter := !mul_counter + 1 in
 183   let hash = op_tm_hash tm in
 184     try
 185       Hashtbl.find mul_table hash
 186     with Not_found ->
 187       let result = Arith_hash.raw_mul_conv_hash tm in
 188       let _ = my_add mul_table hash result in
 189         result;;
 190
 191 (* x / y *)
 192 let raw_div_hash_conv tm =
 193   let _ = div_counter := !div_counter + 1 in
 194   let hash = op_tm_hash tm in
 195     try
 196       Hashtbl.find div_table hash
 197     with Not_found ->
 198       let result = Arith_hash.raw_div_hash_conv tm in
 199       let _ = my_add div_table hash result in
 200         result;;
 201
 202 (* EVEN, ODD *)
 203 let raw_even_hash_conv tm =
 204   let _ = even_counter := !even_counter + 1 in
 205     Arith_hash.raw_even_hash_conv tm;;
 206
 207 let raw_odd_hash_conv tm =
 208   let _ = odd_counter := !odd_counter + 1 in
 209     Arith_hash.raw_odd_hash_conv tm;;
 210
 211 end;;