src/HOL/Tools/SMT/smt_real.ML
author boehmes
Wed May 12 23:54:04 2010 +0200 (2010-05-12)
changeset 36899 bcd6fce5bf06
child 38715 6513ea67d95d
permissions -rw-r--r--
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
     1 (*  Title:      HOL/Tools/SMT/smt_real.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 SMT setup for reals.
     5 *)
     6 
     7 signature SMT_REAL =
     8 sig
     9   val setup: theory -> theory
    10 end
    11 
    12 structure SMT_Real: SMT_REAL =
    13 struct
    14 
    15 
    16 (* SMT-LIB logic *)
    17 
    18 fun smtlib_logic ts =
    19   if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
    20   then SOME "AUFLIRA"
    21   else NONE
    22 
    23 
    24 
    25 (* SMT-LIB builtins *)
    26 
    27 local
    28   fun smtlib_builtin_typ @{typ real} = SOME "Real"
    29     | smtlib_builtin_typ _ = NONE
    30 
    31   fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
    32     | smtlib_builtin_num _ _ = NONE
    33 
    34   fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
    35     | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
    36     | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
    37     | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
    38     | smtlib_builtin_func _ _ = NONE
    39 
    40   fun smtlib_builtin_pred @{const_name less} = SOME "<"
    41     | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
    42     | smtlib_builtin_pred _ = NONE
    43 
    44   fun real_fun T y f x = 
    45     (case try Term.domain_type T of
    46       SOME @{typ real} => f x
    47     | _ => y)
    48 in
    49 
    50 val smtlib_builtins = {
    51   builtin_typ = smtlib_builtin_typ,
    52   builtin_num = smtlib_builtin_num,
    53   builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
    54   builtin_pred = (fn (n, T) => fn ts =>
    55     real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
    56   is_builtin_pred = (fn n => fn T =>
    57     real_fun T false (is_some o smtlib_builtin_pred) n) }
    58 
    59 end
    60 
    61 
    62 
    63 (* Z3 builtins *)
    64 
    65 local
    66   fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
    67     | z3_builtin_fun _ _ = NONE
    68 in
    69 
    70 val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
    71 
    72 end
    73 
    74 
    75 
    76 (* Z3 constructors *)
    77 
    78 local
    79   structure I = Z3_Interface
    80 
    81   fun z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real}
    82     | z3_mk_builtin_typ _ = NONE
    83 
    84   fun z3_mk_builtin_num _ i T =
    85     if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
    86     else NONE
    87 
    88   val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
    89   val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
    90   val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
    91   val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
    92   val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
    93   val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
    94   val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
    95 
    96   fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    97     | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
    98     | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
    99     | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
   100     | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
   101     | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
   102     | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
   103     | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
   104     | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
   105     | z3_mk_builtin_fun _ _ = NONE
   106 in
   107 
   108 val z3_mk_builtins = {
   109   mk_builtin_typ = z3_mk_builtin_typ,
   110   mk_builtin_num = z3_mk_builtin_num,
   111   mk_builtin_fun = (fn _ => fn sym => fn cts =>
   112     (case try (#T o Thm.rep_cterm o hd) cts of
   113       SOME @{typ real} => z3_mk_builtin_fun sym cts
   114     | _ => NONE)) }
   115 
   116 end
   117 
   118 
   119 
   120 (* Z3 proof reconstruction *)
   121 
   122 val real_rules = @{lemma
   123   "0 + (x::real) = x"
   124   "x + 0 = x"
   125   "0 * x = 0"
   126   "1 * x = x"
   127   "x + y = y + x"
   128   by auto}
   129 
   130 val real_linarith_proc = Simplifier.simproc @{theory} "fast_real_arith" [
   131   "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
   132 
   133 
   134 
   135 (* setup *)
   136 
   137 val setup =
   138   Context.theory_map (
   139     SMTLIB_Interface.add_logic smtlib_logic #>
   140     SMTLIB_Interface.add_builtins smtlib_builtins #>
   141     Z3_Interface.add_builtin_funs z3_builtins #>
   142     Z3_Interface.add_mk_builtins z3_mk_builtins #>
   143     fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
   144     Z3_Proof_Tools.add_simproc real_linarith_proc)
   145 
   146 end