src/HOL/Tools/SMT/smt_real.ML
author boehmes
Sun Dec 19 18:54:29 2010 +0100 (2010-12-19)
changeset 41281 679118e35378
parent 41280 a7de9d36f4f2
child 41302 0485186839a7
permissions -rw-r--r--
removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
removed odd retyping during folify (instead, keep all terms well-typed)
boehmes@36899
     1
(*  Title:      HOL/Tools/SMT/smt_real.ML
boehmes@36899
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36899
     3
boehmes@36899
     4
SMT setup for reals.
boehmes@36899
     5
*)
boehmes@36899
     6
boehmes@36899
     7
signature SMT_REAL =
boehmes@36899
     8
sig
boehmes@36899
     9
  val setup: theory -> theory
boehmes@36899
    10
end
boehmes@36899
    11
boehmes@36899
    12
structure SMT_Real: SMT_REAL =
boehmes@36899
    13
struct
boehmes@36899
    14
boehmes@41280
    15
structure U = SMT_Utils
boehmes@41059
    16
structure B = SMT_Builtin
boehmes@41059
    17
boehmes@36899
    18
boehmes@36899
    19
(* SMT-LIB logic *)
boehmes@36899
    20
boehmes@36899
    21
fun smtlib_logic ts =
boehmes@36899
    22
  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
boehmes@36899
    23
  then SOME "AUFLIRA"
boehmes@36899
    24
  else NONE
boehmes@36899
    25
boehmes@36899
    26
boehmes@41059
    27
(* SMT-LIB and Z3 built-ins *)
boehmes@36899
    28
boehmes@36899
    29
local
boehmes@41059
    30
  val smtlibC = SMTLIB_Interface.smtlibC
boehmes@36899
    31
boehmes@41059
    32
  fun real_num _ i = SOME (string_of_int i ^ ".0")
boehmes@41280
    33
boehmes@41280
    34
  fun is_linear [t] = U.is_number t
boehmes@41280
    35
    | is_linear [t, u] = U.is_number t orelse U.is_number u
boehmes@41280
    36
    | is_linear _ = false
boehmes@41280
    37
boehmes@41281
    38
  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
boehmes@41281
    39
boehmes@41281
    40
  fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
boehmes@41280
    41
    | times _ _ _  = NONE
boehmes@41280
    42
boehmes@41281
    43
  fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
boehmes@41281
    44
boehmes@41280
    45
  fun divide _ T (ts as [_, t]) =
boehmes@41281
    46
        if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
boehmes@41280
    47
    | divide _ _ _ = NONE
boehmes@36899
    48
in
boehmes@36899
    49
boehmes@41059
    50
val setup_builtins =
boehmes@41059
    51
  B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
boehmes@41059
    52
  fold (B.add_builtin_fun' smtlibC) [
boehmes@41280
    53
    (@{const less (real)}, "<"),
boehmes@41280
    54
    (@{const less_eq (real)}, "<="),
boehmes@41059
    55
    (@{const uminus (real)}, "~"),
boehmes@41059
    56
    (@{const plus (real)}, "+"),
boehmes@41280
    57
    (@{const minus (real)}, "-") ] #>
boehmes@41280
    58
  B.add_builtin_fun SMTLIB_Interface.smtlibC
boehmes@41280
    59
    (Term.dest_Const @{const times (real)}, times) #>
boehmes@41280
    60
  B.add_builtin_fun Z3_Interface.smtlib_z3C
boehmes@41280
    61
    (Term.dest_Const @{const divide (real)}, divide)
boehmes@36899
    62
boehmes@36899
    63
end
boehmes@36899
    64
boehmes@36899
    65
boehmes@36899
    66
(* Z3 constructors *)
boehmes@36899
    67
boehmes@36899
    68
local
boehmes@36899
    69
  structure I = Z3_Interface
boehmes@36899
    70
boehmes@40516
    71
  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
boehmes@40516
    72
    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
boehmes@36899
    73
    | z3_mk_builtin_typ _ = NONE
boehmes@36899
    74
boehmes@36899
    75
  fun z3_mk_builtin_num _ i T =
boehmes@36899
    76
    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
boehmes@36899
    77
    else NONE
boehmes@36899
    78
boehmes@40579
    79
  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
boehmes@40579
    80
  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
boehmes@40579
    81
  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
boehmes@40579
    82
  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
boehmes@40579
    83
  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
boehmes@40579
    84
  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
boehmes@40579
    85
  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
boehmes@36899
    86
boehmes@36899
    87
  fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
boehmes@36899
    88
    | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
boehmes@36899
    89
    | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
boehmes@36899
    90
    | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
boehmes@36899
    91
    | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
boehmes@36899
    92
    | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
boehmes@36899
    93
    | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
boehmes@36899
    94
    | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
boehmes@36899
    95
    | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
boehmes@36899
    96
    | z3_mk_builtin_fun _ _ = NONE
boehmes@36899
    97
in
boehmes@36899
    98
boehmes@36899
    99
val z3_mk_builtins = {
boehmes@36899
   100
  mk_builtin_typ = z3_mk_builtin_typ,
boehmes@36899
   101
  mk_builtin_num = z3_mk_builtin_num,
boehmes@36899
   102
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
boehmes@36899
   103
    (case try (#T o Thm.rep_cterm o hd) cts of
boehmes@36899
   104
      SOME @{typ real} => z3_mk_builtin_fun sym cts
boehmes@36899
   105
    | _ => NONE)) }
boehmes@36899
   106
boehmes@36899
   107
end
boehmes@36899
   108
boehmes@36899
   109
boehmes@36899
   110
(* Z3 proof reconstruction *)
boehmes@36899
   111
boehmes@36899
   112
val real_rules = @{lemma
boehmes@36899
   113
  "0 + (x::real) = x"
boehmes@36899
   114
  "x + 0 = x"
boehmes@36899
   115
  "0 * x = 0"
boehmes@36899
   116
  "1 * x = x"
boehmes@36899
   117
  "x + y = y + x"
boehmes@36899
   118
  by auto}
boehmes@36899
   119
wenzelm@38715
   120
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
boehmes@36899
   121
  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
boehmes@36899
   122
boehmes@36899
   123
boehmes@36899
   124
(* setup *)
boehmes@36899
   125
boehmes@36899
   126
val setup =
boehmes@36899
   127
  Context.theory_map (
boehmes@41059
   128
    SMTLIB_Interface.add_logic (10, smtlib_logic) #>
boehmes@41072
   129
    setup_builtins #>
boehmes@36899
   130
    Z3_Interface.add_mk_builtins z3_mk_builtins #>
boehmes@36899
   131
    fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
boehmes@36899
   132
    Z3_Proof_Tools.add_simproc real_linarith_proc)
boehmes@36899
   133
boehmes@36899
   134
end