formal_ineqs/arith/arith_cache.hl

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