src/HOL/Tools/SMT/smt_real.ML
changeset 36899 bcd6fce5bf06
child 38715 6513ea67d95d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed May 12 23:54:04 2010 +0200
     1.3 @@ -0,0 +1,146 @@
     1.4 +(*  Title:      HOL/Tools/SMT/smt_real.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +SMT setup for reals.
     1.8 +*)
     1.9 +
    1.10 +signature SMT_REAL =
    1.11 +sig
    1.12 +  val setup: theory -> theory
    1.13 +end
    1.14 +
    1.15 +structure SMT_Real: SMT_REAL =
    1.16 +struct
    1.17 +
    1.18 +
    1.19 +(* SMT-LIB logic *)
    1.20 +
    1.21 +fun smtlib_logic ts =
    1.22 +  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
    1.23 +  then SOME "AUFLIRA"
    1.24 +  else NONE
    1.25 +
    1.26 +
    1.27 +
    1.28 +(* SMT-LIB builtins *)
    1.29 +
    1.30 +local
    1.31 +  fun smtlib_builtin_typ @{typ real} = SOME "Real"
    1.32 +    | smtlib_builtin_typ _ = NONE
    1.33 +
    1.34 +  fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
    1.35 +    | smtlib_builtin_num _ _ = NONE
    1.36 +
    1.37 +  fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
    1.38 +    | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
    1.39 +    | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
    1.40 +    | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
    1.41 +    | smtlib_builtin_func _ _ = NONE
    1.42 +
    1.43 +  fun smtlib_builtin_pred @{const_name less} = SOME "<"
    1.44 +    | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
    1.45 +    | smtlib_builtin_pred _ = NONE
    1.46 +
    1.47 +  fun real_fun T y f x = 
    1.48 +    (case try Term.domain_type T of
    1.49 +      SOME @{typ real} => f x
    1.50 +    | _ => y)
    1.51 +in
    1.52 +
    1.53 +val smtlib_builtins = {
    1.54 +  builtin_typ = smtlib_builtin_typ,
    1.55 +  builtin_num = smtlib_builtin_num,
    1.56 +  builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
    1.57 +  builtin_pred = (fn (n, T) => fn ts =>
    1.58 +    real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
    1.59 +  is_builtin_pred = (fn n => fn T =>
    1.60 +    real_fun T false (is_some o smtlib_builtin_pred) n) }
    1.61 +
    1.62 +end
    1.63 +
    1.64 +
    1.65 +
    1.66 +(* Z3 builtins *)
    1.67 +
    1.68 +local
    1.69 +  fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
    1.70 +    | z3_builtin_fun _ _ = NONE
    1.71 +in
    1.72 +
    1.73 +val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
    1.74 +
    1.75 +end
    1.76 +
    1.77 +
    1.78 +
    1.79 +(* Z3 constructors *)
    1.80 +
    1.81 +local
    1.82 +  structure I = Z3_Interface
    1.83 +
    1.84 +  fun z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real}
    1.85 +    | z3_mk_builtin_typ _ = NONE
    1.86 +
    1.87 +  fun z3_mk_builtin_num _ i T =
    1.88 +    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
    1.89 +    else NONE
    1.90 +
    1.91 +  val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
    1.92 +  val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
    1.93 +  val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
    1.94 +  val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
    1.95 +  val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
    1.96 +  val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
    1.97 +  val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
    1.98 +
    1.99 +  fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
   1.100 +    | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
   1.101 +    | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
   1.102 +    | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
   1.103 +    | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
   1.104 +    | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
   1.105 +    | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
   1.106 +    | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
   1.107 +    | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
   1.108 +    | z3_mk_builtin_fun _ _ = NONE
   1.109 +in
   1.110 +
   1.111 +val z3_mk_builtins = {
   1.112 +  mk_builtin_typ = z3_mk_builtin_typ,
   1.113 +  mk_builtin_num = z3_mk_builtin_num,
   1.114 +  mk_builtin_fun = (fn _ => fn sym => fn cts =>
   1.115 +    (case try (#T o Thm.rep_cterm o hd) cts of
   1.116 +      SOME @{typ real} => z3_mk_builtin_fun sym cts
   1.117 +    | _ => NONE)) }
   1.118 +
   1.119 +end
   1.120 +
   1.121 +
   1.122 +
   1.123 +(* Z3 proof reconstruction *)
   1.124 +
   1.125 +val real_rules = @{lemma
   1.126 +  "0 + (x::real) = x"
   1.127 +  "x + 0 = x"
   1.128 +  "0 * x = 0"
   1.129 +  "1 * x = x"
   1.130 +  "x + y = y + x"
   1.131 +  by auto}
   1.132 +
   1.133 +val real_linarith_proc = Simplifier.simproc @{theory} "fast_real_arith" [
   1.134 +  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
   1.135 +
   1.136 +
   1.137 +
   1.138 +(* setup *)
   1.139 +
   1.140 +val setup =
   1.141 +  Context.theory_map (
   1.142 +    SMTLIB_Interface.add_logic smtlib_logic #>
   1.143 +    SMTLIB_Interface.add_builtins smtlib_builtins #>
   1.144 +    Z3_Interface.add_builtin_funs z3_builtins #>
   1.145 +    Z3_Interface.add_mk_builtins z3_mk_builtins #>
   1.146 +    fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
   1.147 +    Z3_Proof_Tools.add_simproc real_linarith_proc)
   1.148 +
   1.149 +end