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