src/HOL/Tools/SMT/smt_real.ML
author boehmes
Wed Dec 08 08:33:02 2010 +0100 (2010-12-08)
changeset 41072 9f9bc1bdacef
parent 41059 d2b1fc1b8e19
child 41280 a7de9d36f4f2
permissions -rw-r--r--
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
     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 B = SMT_Builtin
    16 
    17 
    18 (* SMT-LIB logic *)
    19 
    20 fun smtlib_logic ts =
    21   if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
    22   then SOME "AUFLIRA"
    23   else NONE
    24 
    25 
    26 (* SMT-LIB and Z3 built-ins *)
    27 
    28 local
    29   val smtlibC = SMTLIB_Interface.smtlibC
    30 
    31   fun real_num _ i = SOME (string_of_int i ^ ".0")
    32 in
    33 
    34 val setup_builtins =
    35   B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
    36   fold (B.add_builtin_fun' smtlibC) [
    37     (@{const uminus (real)}, "~"),
    38     (@{const plus (real)}, "+"),
    39     (@{const minus (real)}, "-"),
    40     (@{const times (real)}, "*"),
    41     (@{const less (real)}, "<"),
    42     (@{const less_eq (real)}, "<=") ] #>
    43   B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
    44 
    45 end
    46 
    47 
    48 (* Z3 constructors *)
    49 
    50 local
    51   structure I = Z3_Interface
    52 
    53   fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
    54     | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
    55     | z3_mk_builtin_typ _ = NONE
    56 
    57   fun z3_mk_builtin_num _ i T =
    58     if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
    59     else NONE
    60 
    61   val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
    62   val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
    63   val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
    64   val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    65   val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
    66   val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
    67   val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    68 
    69   fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    70     | z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
    71     | z3_mk_builtin_fun (I.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
    72     | z3_mk_builtin_fun (I.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
    73     | z3_mk_builtin_fun (I.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
    74     | z3_mk_builtin_fun (I.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
    75     | z3_mk_builtin_fun (I.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
    76     | z3_mk_builtin_fun (I.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
    77     | z3_mk_builtin_fun (I.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
    78     | z3_mk_builtin_fun _ _ = NONE
    79 in
    80 
    81 val z3_mk_builtins = {
    82   mk_builtin_typ = z3_mk_builtin_typ,
    83   mk_builtin_num = z3_mk_builtin_num,
    84   mk_builtin_fun = (fn _ => fn sym => fn cts =>
    85     (case try (#T o Thm.rep_cterm o hd) cts of
    86       SOME @{typ real} => z3_mk_builtin_fun sym cts
    87     | _ => NONE)) }
    88 
    89 end
    90 
    91 
    92 (* Z3 proof reconstruction *)
    93 
    94 val real_rules = @{lemma
    95   "0 + (x::real) = x"
    96   "x + 0 = x"
    97   "0 * x = 0"
    98   "1 * x = x"
    99   "x + y = y + x"
   100   by auto}
   101 
   102 val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
   103   "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
   104 
   105 
   106 (* setup *)
   107 
   108 val setup =
   109   Context.theory_map (
   110     SMTLIB_Interface.add_logic (10, smtlib_logic) #>
   111     setup_builtins #>
   112     Z3_Interface.add_mk_builtins z3_mk_builtins #>
   113     fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
   114     Z3_Proof_Tools.add_simproc real_linarith_proc)
   115 
   116 end