File ‹Tools/SMT/smt_real.ML›

(*  Title:      HOL/Tools/SMT/smt_real.ML
    Author:     Sascha Boehme, TU Muenchen

SMT setup for reals.
*)

structure SMT_Real: sig end =
struct


(* SMT-LIB logic *)

fun smtlib_logic _ ts _ =
    if exists (Term.exists_type (Term.exists_subtype (equal \<^typ>‹real›))) ts
    then SOME (SMT_Translate.SL {fixedSizeBitVectors=false,real=true,set=false,datatypes=false})
    else NONE


(* SMT-LIB and Z3 built-ins *)

local
  fun real_num _ i = SOME (string_of_int i ^ ".0")

  fun is_linear [t] = SMT_Util.is_number t
    | is_linear [t, u] = SMT_Util.is_number t orelse SMT_Util.is_number u
    | is_linear _ = false

  fun mk_times ts = Term.list_comb (\<^Const>‹times \<^Type>‹real››, ts)

  fun times _ _ ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
in

fun real_type_parser (SMTLIB.Sym "Real", []) = SOME \<^typ>‹Real.real›
  | real_type_parser _ = NONE

fun mk_divide t1 t2 = \<^Const>‹divide \<^Type>‹real› for t1 t2›
fun mk_real_num i = HOLogic.mk_number \<^Type>‹real› i

fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number \<^typ>‹Real.real› i)
  | real_term_parser (SMTLIB.Dec d, []) =
    let val (numerator, denominator) = SMTLIB.convert_dec_to_rat d in
      SOME (mk_divide (mk_real_num numerator) (mk_real_num denominator))
    end
  | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
      SOME (\<^term>‹Rings.divide :: real => _› $ t1 $ t2)
  | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (\<^term>‹Int.of_int :: int => Real.real› $ t)
  | real_term_parser (SMTLIB.Sym "to_int", [t]) = SOME (\<^term>‹floor :: Real.real ⇒ int› $ t)
  | real_term_parser _ = NONE

fun abstract abs t =
  (case t of
    (c as \<^term>‹Rings.divide :: real => _›) $ t1 $ t2 =>
      abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
  | (c as \<^term>‹Int.of_int :: int => _›) $ t =>
      abs t #>> (fn u => SOME (c $ u))
  | _ => pair NONE)

val _ = Theory.setup (Context.theory_map (
  SMTLIB_Proof.add_type_parser real_type_parser #>
  SMTLIB_Proof.add_term_parser real_term_parser #>
  SMT_Replay_Methods.add_arith_abstracter abstract))

val setup_builtins =
  SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
    (\<^typ>‹real›, K (SOME ("Real", [])), real_num) #>
  fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
    (\<^Const>‹less \<^Type>‹real››, "<"),
    (\<^Const>‹less_eq \<^Type>‹real››, "<="),
    (\<^Const>‹uminus \<^Type>‹real››, "-"),
    (\<^Const>‹plus \<^Type>‹real››, "+"),
    (\<^Const>‹minus \<^Type>‹real››, "-") ] #>
  SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
    (Term.dest_Const \<^Const>‹times \<^Type>‹real››, times)

end


(* Z3 constructors *)

local
  fun smt_mk_builtin_typ (Z3_Interface.Sym ("Real", _)) = SOME \<^typ>‹real›
    | smt_mk_builtin_typ (Z3_Interface.Sym ("real", _)) = SOME \<^typ>‹real›
        (*FIXME: delete*)
    | smt_mk_builtin_typ _ = NONE

  fun smt_mk_builtin_num _ i T =
    if T = \<^typ>‹real› then SOME (Numeral.mk_cnumber \<^ctyp>‹real› i)
    else NONE

  fun mk_nary _ cu [] = cu
    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)

  val mk_uminus = Thm.apply \<^cterm>‹uminus :: real ⇒ _›
  val add = \<^cterm>‹(+) :: real ⇒ _›
  val real0 = Numeral.mk_cnumber \<^ctyp>‹real› 0
  val mk_sub = Thm.mk_binop \<^cterm>‹(-) :: real ⇒ _›
  val mk_mul = Thm.mk_binop \<^cterm>‹(*) :: real ⇒ _›
  val mk_div = Thm.mk_binop \<^cterm>‹(/) :: real ⇒ _›
  val mk_lt = Thm.mk_binop \<^cterm>‹(<) :: real ⇒ _›
  val mk_le = Thm.mk_binop \<^cterm>‹(≤) :: real ⇒ _›

  fun smt_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    | smt_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts)
    | smt_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu)
    | smt_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu)
    | smt_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = SOME (mk_div ct cu)
    | smt_mk_builtin_fun (Z3_Interface.Sym ("<", _)) [ct, cu] = SOME (mk_lt ct cu)
    | smt_mk_builtin_fun (Z3_Interface.Sym ("<=", _)) [ct, cu] = SOME (mk_le ct cu)
    | smt_mk_builtin_fun (Z3_Interface.Sym (">", _)) [ct, cu] = SOME (mk_lt cu ct)
    | smt_mk_builtin_fun (Z3_Interface.Sym (">=", _)) [ct, cu] = SOME (mk_le cu ct)
    | smt_mk_builtin_fun _ _ = NONE
in

val smt_mk_builtins = {
  mk_builtin_typ = smt_mk_builtin_typ,
  mk_builtin_num = smt_mk_builtin_num,
  mk_builtin_fun = (fn _ => fn sym => fn cts =>
    (case try (Thm.typ_of_cterm o hd) cts of
      SOME \<^typ>‹real› => smt_mk_builtin_fun sym cts
    | _ => NONE)) }

end


(* Z3 proof replay *)

val real_linarith_simproc =
  \<^simproc_setup>‹passive fast_real_arith ("(m::real) < n" | "(m::real) ≤ n" | "(m::real) = n") =
    ‹K Lin_Arith.simproc››;


(* setup *)

val _ = Theory.setup (Context.theory_map (
  SMTLIB_Interface.add_logic (10, smtlib_logic) #>
  setup_builtins #>
  Z3_Interface.add_mk_builtins smt_mk_builtins #>
  SMT_Replay.add_simproc real_linarith_simproc))

end;