formal_ineqs/arith_options.hl

   1 (* =========================================================== *)\r
   2 (* Options of the arithmetic library                           *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 module Arith_options = struct\r
   8 \r
   9 (* Base of arithmetic operations with natural numbers *)\r
  10 (* The base should be even in order to represent inv(2) exactly *)\r
  11 let base = ref 100;;\r
  12 (* If true then results of natural number operations are cached *)\r
  13 let cached = ref true;;\r
  14 (* Initial size of the cache *)\r
  15 let init_cache_size = ref 10000;;\r
  16 (* Maximal size of the cache *)\r
  17 let max_cache_size = ref 20000;;\r
  18 \r
  19 (* Minimal exponent value for floating point numbers *)\r
  20 (* (should be even for the square root operation) *)\r
  21 let min_exp = ref 50;;\r
  22 (* If true, then arithmetic operations with floating point numbers are cached *)\r
  23 let float_cached = ref true;;\r
  24 \r
  25 end;;\r