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)
     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 structure U = SMT_Utils
    16 structure B = SMT_Builtin
    17 
    18 
    19 (* SMT-LIB logic *)
    20 
    21 fun smtlib_logic ts =
    22   if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
    23   then SOME "AUFLIRA"
    24   else NONE
    25 
    26 
    27 (* SMT-LIB and Z3 built-ins *)
    28 
    29 local
    30   val smtlibC = SMTLIB_Interface.smtlibC
    31 
    32   fun real_num _ i = SOME (string_of_int i ^ ".0")
    33 
    34   fun is_linear [t] = U.is_number t
    35     | is_linear [t, u] = U.is_number t orelse U.is_number u
    36     | is_linear _ = false
    37 
    38   fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
    39 
    40   fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
    41     | times _ _ _  = NONE
    42 
    43   fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
    44 
    45   fun divide _ T (ts as [_, t]) =
    46         if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
    47     | divide _ _ _ = NONE
    48 in
    49 
    50 val setup_builtins =
    51   B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    52   fold (B.add_builtin_fun' smtlibC) [
    53     (@{const less (real)}, "<"),
    54     (@{const less_eq (real)}, "<="),
    55     (@{const uminus (real)}, "~"),
    56     (@{const plus (real)}, "+"),
    57     (@{const minus (real)}, "-") ] #>
    58   B.add_builtin_fun SMTLIB_Interface.smtlibC
    59     (Term.dest_Const @{const times (real)}, times) #>
    60   B.add_builtin_fun Z3_Interface.smtlib_z3C
    61     (Term.dest_Const @{const divide (real)}, divide)
    62 
    63 end
    64 
    65 
    66 (* Z3 constructors *)
    67 
    68 local
    69   structure I = Z3_Interface
    70 
    71   fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
    72     | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
    73     | z3_mk_builtin_typ _ = NONE
    74 
    75   fun z3_mk_builtin_num _ i T =
    76     if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
    77     else NONE
    78 
    79   val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
    80   val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
    81   val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
    82   val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    83   val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
    84   val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
    85   val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    86 
    87   fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    88     | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
    89     | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
    90     | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
    91     | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
    92     | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
    93     | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
    94     | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
    95     | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
    96     | z3_mk_builtin_fun _ _ = NONE
    97 in
    98 
    99 val z3_mk_builtins = {
   100   mk_builtin_typ = z3_mk_builtin_typ,
   101   mk_builtin_num = z3_mk_builtin_num,
   102   mk_builtin_fun = (fn _ => fn sym => fn cts =>
   103     (case try (#T o Thm.rep_cterm o hd) cts of
   104       SOME @{typ real} => z3_mk_builtin_fun sym cts
   105     | _ => NONE)) }
   106 
   107 end
   108 
   109 
   110 (* Z3 proof reconstruction *)
   111 
   112 val real_rules = @{lemma
   113   "0 + (x::real) = x"
   114   "x + 0 = x"
   115   "0 * x = 0"
   116   "1 * x = x"
   117   "x + y = y + x"
   118   by auto}
   119 
   120 val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
   121   "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
   122 
   123 
   124 (* setup *)
   125 
   126 val setup =
   127   Context.theory_map (
   128     SMTLIB_Interface.add_logic (10, smtlib_logic) #>
   129     setup_builtins #>
   130     Z3_Interface.add_mk_builtins z3_mk_builtins #>
   131     fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
   132     Z3_Proof_Tools.add_simproc real_linarith_proc)
   133 
   134 end