src/HOL/Tools/SMT2/smt2_real.ML
author blanchet
Thu Mar 13 13:18:13 2014 +0100 (2014-03-13)
changeset 56078 624faeda77b5
child 56090 34bd10a9a2ad
permissions -rw-r--r--
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet@56078
     1
(*  Title:      HOL/Tools/SMT2/smt2_real.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
SMT setup for reals.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@56078
     7
structure SMT2_Real: sig end =
blanchet@56078
     8
struct
blanchet@56078
     9
blanchet@56078
    10
blanchet@56078
    11
(* SMT-LIB logic *)
blanchet@56078
    12
blanchet@56078
    13
fun smtlib_logic ts =
blanchet@56078
    14
  if exists (Term.exists_type (Term.exists_subtype (equal @{typ real}))) ts
blanchet@56078
    15
  then SOME "AUFLIRA"
blanchet@56078
    16
  else NONE
blanchet@56078
    17
blanchet@56078
    18
blanchet@56078
    19
(* SMT-LIB and Z3 built-ins *)
blanchet@56078
    20
blanchet@56078
    21
local
blanchet@56078
    22
  fun real_num _ i = SOME (string_of_int i ^ ".0")
blanchet@56078
    23
blanchet@56078
    24
  fun is_linear [t] = SMT2_Utils.is_number t
blanchet@56078
    25
    | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u
blanchet@56078
    26
    | is_linear _ = false
blanchet@56078
    27
blanchet@56078
    28
  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
blanchet@56078
    29
blanchet@56078
    30
  fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
blanchet@56078
    31
in
blanchet@56078
    32
blanchet@56078
    33
val setup_builtins =
blanchet@56078
    34
  SMT2_Builtin.add_builtin_typ SMTLIB2_Interface.smtlib2C
blanchet@56078
    35
    (@{typ real}, K (SOME "Real"), real_num) #>
blanchet@56078
    36
  fold (SMT2_Builtin.add_builtin_fun' SMTLIB2_Interface.smtlib2C) [
blanchet@56078
    37
    (@{const less (real)}, "<"),
blanchet@56078
    38
    (@{const less_eq (real)}, "<="),
blanchet@56078
    39
    (@{const uminus (real)}, "~"),
blanchet@56078
    40
    (@{const plus (real)}, "+"),
blanchet@56078
    41
    (@{const minus (real)}, "-") ] #>
blanchet@56078
    42
  SMT2_Builtin.add_builtin_fun SMTLIB2_Interface.smtlib2C
blanchet@56078
    43
    (Term.dest_Const @{const times (real)}, times) #>
blanchet@56078
    44
  SMT2_Builtin.add_builtin_fun' Z3_New_Interface.smtlib2_z3C
blanchet@56078
    45
    (@{const times (real)}, "*") #>
blanchet@56078
    46
  SMT2_Builtin.add_builtin_fun' Z3_New_Interface.smtlib2_z3C
blanchet@56078
    47
    (@{const divide (real)}, "/")
blanchet@56078
    48
blanchet@56078
    49
end
blanchet@56078
    50
blanchet@56078
    51
blanchet@56078
    52
(* Z3 constructors *)
blanchet@56078
    53
blanchet@56078
    54
local
blanchet@56078
    55
  fun z3_mk_builtin_typ (Z3_New_Interface.Sym ("Real", _)) = SOME @{typ real}
blanchet@56078
    56
    | z3_mk_builtin_typ (Z3_New_Interface.Sym ("real", _)) = SOME @{typ real}
blanchet@56078
    57
        (*FIXME: delete*)
blanchet@56078
    58
    | z3_mk_builtin_typ _ = NONE
blanchet@56078
    59
blanchet@56078
    60
  fun z3_mk_builtin_num _ i T =
blanchet@56078
    61
    if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
blanchet@56078
    62
    else NONE
blanchet@56078
    63
blanchet@56078
    64
  fun mk_nary _ cu [] = cu
blanchet@56078
    65
    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
blanchet@56078
    66
blanchet@56078
    67
  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
blanchet@56078
    68
  val add = Thm.cterm_of @{theory} @{const plus (real)}
blanchet@56078
    69
  val real0 = Numeral.mk_cnumber @{ctyp real} 0
blanchet@56078
    70
  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
blanchet@56078
    71
  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
blanchet@56078
    72
  val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
blanchet@56078
    73
  val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
blanchet@56078
    74
  val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
blanchet@56078
    75
blanchet@56078
    76
  fun z3_mk_builtin_fun (Z3_New_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
blanchet@56078
    77
    | z3_mk_builtin_fun (Z3_New_Interface.Sym ("+", _)) cts =
blanchet@56078
    78
        SOME (mk_nary add real0 cts)
blanchet@56078
    79
    | z3_mk_builtin_fun (Z3_New_Interface.Sym ("-", _)) [ct, cu] =
blanchet@56078
    80
        SOME (mk_sub ct cu)
blanchet@56078
    81
    | z3_mk_builtin_fun (Z3_New_Interface.Sym ("*", _)) [ct, cu] =
blanchet@56078
    82
        SOME (mk_mul ct cu)
blanchet@56078
    83
    | z3_mk_builtin_fun (Z3_New_Interface.Sym ("/", _)) [ct, cu] =
blanchet@56078
    84
        SOME (mk_div ct cu)
blanchet@56078
    85
    | z3_mk_builtin_fun (Z3_New_Interface.Sym ("<", _)) [ct, cu] =
blanchet@56078
    86
        SOME (mk_lt ct cu)
blanchet@56078
    87
    | z3_mk_builtin_fun (Z3_New_Interface.Sym ("<=", _)) [ct, cu] =
blanchet@56078
    88
        SOME (mk_le ct cu)
blanchet@56078
    89
    | z3_mk_builtin_fun (Z3_New_Interface.Sym (">", _)) [ct, cu] =
blanchet@56078
    90
        SOME (mk_lt cu ct)
blanchet@56078
    91
    | z3_mk_builtin_fun (Z3_New_Interface.Sym (">=", _)) [ct, cu] =
blanchet@56078
    92
        SOME (mk_le cu ct)
blanchet@56078
    93
    | z3_mk_builtin_fun _ _ = NONE
blanchet@56078
    94
in
blanchet@56078
    95
blanchet@56078
    96
val z3_mk_builtins = {
blanchet@56078
    97
  mk_builtin_typ = z3_mk_builtin_typ,
blanchet@56078
    98
  mk_builtin_num = z3_mk_builtin_num,
blanchet@56078
    99
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
blanchet@56078
   100
    (case try (#T o Thm.rep_cterm o hd) cts of
blanchet@56078
   101
      SOME @{typ real} => z3_mk_builtin_fun sym cts
blanchet@56078
   102
    | _ => NONE)) }
blanchet@56078
   103
blanchet@56078
   104
end
blanchet@56078
   105
blanchet@56078
   106
blanchet@56078
   107
(* Z3 proof replay *)
blanchet@56078
   108
blanchet@56078
   109
val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
blanchet@56078
   110
  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc
blanchet@56078
   111
blanchet@56078
   112
blanchet@56078
   113
(* setup *)
blanchet@56078
   114
blanchet@56078
   115
val _ = Theory.setup (Context.theory_map (
blanchet@56078
   116
  SMTLIB2_Interface.add_logic (10, smtlib_logic) #>
blanchet@56078
   117
  setup_builtins #>
blanchet@56078
   118
  Z3_New_Interface.add_mk_builtins z3_mk_builtins #>
blanchet@56078
   119
  Z3_New_Proof_Tools.add_simproc real_linarith_proc))
blanchet@56078
   120
blanchet@56078
   121
end