src/HOL/Tools/SMT/smt_real.ML
changeset 41059 d2b1fc1b8e19
parent 40579 98ebd2300823
child 41072 9f9bc1bdacef
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Mon Dec 06 16:54:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Tue Dec 07 14:53:12 2010 +0100
     1.3 @@ -12,6 +12,8 @@
     1.4  structure SMT_Real: SMT_REAL =
     1.5  struct
     1.6  
     1.7 +structure B = SMT_Builtin
     1.8 +
     1.9  
    1.10  (* SMT-LIB logic *)
    1.11  
    1.12 @@ -21,58 +23,28 @@
    1.13    else NONE
    1.14  
    1.15  
    1.16 -
    1.17 -(* SMT-LIB builtins *)
    1.18 +(* SMT-LIB and Z3 built-ins *)
    1.19  
    1.20  local
    1.21 -  fun smtlib_builtin_typ @{typ real} = SOME "Real"
    1.22 -    | smtlib_builtin_typ _ = NONE
    1.23 -
    1.24 -  fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
    1.25 -    | smtlib_builtin_num _ _ = NONE
    1.26 +  val smtlibC = SMTLIB_Interface.smtlibC
    1.27  
    1.28 -  fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
    1.29 -    | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
    1.30 -    | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
    1.31 -    | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
    1.32 -    | smtlib_builtin_func _ _ = NONE
    1.33 -
    1.34 -  fun smtlib_builtin_pred @{const_name less} = SOME "<"
    1.35 -    | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
    1.36 -    | smtlib_builtin_pred _ = NONE
    1.37 -
    1.38 -  fun real_fun T y f x = 
    1.39 -    (case try Term.domain_type T of
    1.40 -      SOME @{typ real} => f x
    1.41 -    | _ => y)
    1.42 +  fun real_num _ i = SOME (string_of_int i ^ ".0")
    1.43  in
    1.44  
    1.45 -val smtlib_builtins = {
    1.46 -  builtin_typ = smtlib_builtin_typ,
    1.47 -  builtin_num = smtlib_builtin_num,
    1.48 -  builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
    1.49 -  builtin_pred = (fn (n, T) => fn ts =>
    1.50 -    real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
    1.51 -  is_builtin_pred = (fn n => fn T =>
    1.52 -    real_fun T false (is_some o smtlib_builtin_pred) n) }
    1.53 +val setup_builtins =
    1.54 +  B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    1.55 +  fold (B.add_builtin_fun' smtlibC) [
    1.56 +    (@{const uminus (real)}, "~"),
    1.57 +    (@{const plus (real)}, "+"),
    1.58 +    (@{const minus (real)}, "-"),
    1.59 +    (@{const times (real)}, "*"),
    1.60 +    (@{const less (real)}, "<"),
    1.61 +    (@{const less_eq (real)}, "<=") ] #>
    1.62 +  B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    1.63  
    1.64  end
    1.65  
    1.66  
    1.67 -
    1.68 -(* Z3 builtins *)
    1.69 -
    1.70 -local
    1.71 -  fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
    1.72 -    | z3_builtin_fun _ _ = NONE
    1.73 -in
    1.74 -
    1.75 -val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
    1.76 -
    1.77 -end
    1.78 -
    1.79 -
    1.80 -
    1.81  (* Z3 constructors *)
    1.82  
    1.83  local
    1.84 @@ -117,7 +89,6 @@
    1.85  end
    1.86  
    1.87  
    1.88 -
    1.89  (* Z3 proof reconstruction *)
    1.90  
    1.91  val real_rules = @{lemma
    1.92 @@ -132,14 +103,12 @@
    1.93    "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
    1.94  
    1.95  
    1.96 -
    1.97  (* setup *)
    1.98  
    1.99  val setup =
   1.100 +  setup_builtins #>
   1.101    Context.theory_map (
   1.102 -    SMTLIB_Interface.add_logic smtlib_logic #>
   1.103 -    SMTLIB_Interface.add_builtins smtlib_builtins #>
   1.104 -    Z3_Interface.add_builtin_funs z3_builtins #>
   1.105 +    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
   1.106      Z3_Interface.add_mk_builtins z3_mk_builtins #>
   1.107      fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
   1.108      Z3_Proof_Tools.add_simproc real_linarith_proc)