src/HOL/Tools/SMT/smt_real.ML
author boehmes
Wed Nov 17 08:14:56 2010 +0100 (2010-11-17)
changeset 40579 98ebd2300823
parent 40516 516a367eb38c
child 41059 d2b1fc1b8e19
permissions -rw-r--r--
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
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@36899
    15
boehmes@36899
    16
(* SMT-LIB logic *)
boehmes@36899
    17
boehmes@36899
    18
fun smtlib_logic ts =
boehmes@36899
    19
  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
boehmes@36899
    20
  then SOME "AUFLIRA"
boehmes@36899
    21
  else NONE
boehmes@36899
    22
boehmes@36899
    23
boehmes@36899
    24
boehmes@36899
    25
(* SMT-LIB builtins *)
boehmes@36899
    26
boehmes@36899
    27
local
boehmes@36899
    28
  fun smtlib_builtin_typ @{typ real} = SOME "Real"
boehmes@36899
    29
    | smtlib_builtin_typ _ = NONE
boehmes@36899
    30
boehmes@36899
    31
  fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
boehmes@36899
    32
    | smtlib_builtin_num _ _ = NONE
boehmes@36899
    33
boehmes@36899
    34
  fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
boehmes@36899
    35
    | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
boehmes@36899
    36
    | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
boehmes@36899
    37
    | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
boehmes@36899
    38
    | smtlib_builtin_func _ _ = NONE
boehmes@36899
    39
boehmes@36899
    40
  fun smtlib_builtin_pred @{const_name less} = SOME "<"
boehmes@36899
    41
    | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
boehmes@36899
    42
    | smtlib_builtin_pred _ = NONE
boehmes@36899
    43
boehmes@36899
    44
  fun real_fun T y f x = 
boehmes@36899
    45
    (case try Term.domain_type T of
boehmes@36899
    46
      SOME @{typ real} => f x
boehmes@36899
    47
    | _ => y)
boehmes@36899
    48
in
boehmes@36899
    49
boehmes@36899
    50
val smtlib_builtins = {
boehmes@36899
    51
  builtin_typ = smtlib_builtin_typ,
boehmes@36899
    52
  builtin_num = smtlib_builtin_num,
boehmes@36899
    53
  builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
boehmes@36899
    54
  builtin_pred = (fn (n, T) => fn ts =>
boehmes@36899
    55
    real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
boehmes@36899
    56
  is_builtin_pred = (fn n => fn T =>
boehmes@36899
    57
    real_fun T false (is_some o smtlib_builtin_pred) n) }
boehmes@36899
    58
boehmes@36899
    59
end
boehmes@36899
    60
boehmes@36899
    61
boehmes@36899
    62
boehmes@36899
    63
(* Z3 builtins *)
boehmes@36899
    64
boehmes@36899
    65
local
boehmes@40579
    66
  fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
boehmes@36899
    67
    | z3_builtin_fun _ _ = NONE
boehmes@36899
    68
in
boehmes@36899
    69
boehmes@36899
    70
val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
boehmes@36899
    71
boehmes@36899
    72
end
boehmes@36899
    73
boehmes@36899
    74
boehmes@36899
    75
boehmes@36899
    76
(* Z3 constructors *)
boehmes@36899
    77
boehmes@36899
    78
local
boehmes@36899
    79
  structure I = Z3_Interface
boehmes@36899
    80
boehmes@40516
    81
  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
boehmes@40516
    82
    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
boehmes@36899
    83
    | z3_mk_builtin_typ _ = NONE
boehmes@36899
    84
boehmes@36899
    85
  fun z3_mk_builtin_num _ i T =
boehmes@36899
    86
    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
boehmes@36899
    87
    else NONE
boehmes@36899
    88
boehmes@40579
    89
  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
boehmes@40579
    90
  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
boehmes@40579
    91
  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
boehmes@40579
    92
  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
boehmes@40579
    93
  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
boehmes@40579
    94
  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
boehmes@40579
    95
  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
boehmes@36899
    96
boehmes@36899
    97
  fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
boehmes@36899
    98
    | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
boehmes@36899
    99
    | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
boehmes@36899
   100
    | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
boehmes@36899
   101
    | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
boehmes@36899
   102
    | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
boehmes@36899
   103
    | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
boehmes@36899
   104
    | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
boehmes@36899
   105
    | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
boehmes@36899
   106
    | z3_mk_builtin_fun _ _ = NONE
boehmes@36899
   107
in
boehmes@36899
   108
boehmes@36899
   109
val z3_mk_builtins = {
boehmes@36899
   110
  mk_builtin_typ = z3_mk_builtin_typ,
boehmes@36899
   111
  mk_builtin_num = z3_mk_builtin_num,
boehmes@36899
   112
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
boehmes@36899
   113
    (case try (#T o Thm.rep_cterm o hd) cts of
boehmes@36899
   114
      SOME @{typ real} => z3_mk_builtin_fun sym cts
boehmes@36899
   115
    | _ => NONE)) }
boehmes@36899
   116
boehmes@36899
   117
end
boehmes@36899
   118
boehmes@36899
   119
boehmes@36899
   120
boehmes@36899
   121
(* Z3 proof reconstruction *)
boehmes@36899
   122
boehmes@36899
   123
val real_rules = @{lemma
boehmes@36899
   124
  "0 + (x::real) = x"
boehmes@36899
   125
  "x + 0 = x"
boehmes@36899
   126
  "0 * x = 0"
boehmes@36899
   127
  "1 * x = x"
boehmes@36899
   128
  "x + y = y + x"
boehmes@36899
   129
  by auto}
boehmes@36899
   130
wenzelm@38715
   131
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
boehmes@36899
   132
  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
boehmes@36899
   133
boehmes@36899
   134
boehmes@36899
   135
boehmes@36899
   136
(* setup *)
boehmes@36899
   137
boehmes@36899
   138
val setup =
boehmes@36899
   139
  Context.theory_map (
boehmes@36899
   140
    SMTLIB_Interface.add_logic smtlib_logic #>
boehmes@36899
   141
    SMTLIB_Interface.add_builtins smtlib_builtins #>
boehmes@36899
   142
    Z3_Interface.add_builtin_funs z3_builtins #>
boehmes@36899
   143
    Z3_Interface.add_mk_builtins z3_mk_builtins #>
boehmes@36899
   144
    fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
boehmes@36899
   145
    Z3_Proof_Tools.add_simproc real_linarith_proc)
boehmes@36899
   146
boehmes@36899
   147
end