Quelle smt_real.ML Sprache: SML

(*  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>\<open>real\<close>))) ts
  then SOME "AUFLIRA"
  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>\<open>times \<^Type>\<open>real\<close>\<close>, 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>\<open>Real.real\<close>
  | real_type_parser _ = NONE

fun real_term_parser (SMTLIB.Dec (i, 0), []) = SOME (HOLogic.mk_number \<^typ>\<open>Real.real\<close> i)
  | real_term_parser (SMTLIB.Sym "/", [t1, t2]) =
      SOME (\<^term>\<open>Rings.divide :: real => _\<close> $ t1 $ t2)
  | real_term_parser (SMTLIB.Sym "to_real", [t]) = SOME (\<^term>\<open>Int.of_int :: int => _\<close> $ t)
  | real_term_parser _ = NONE

fun abstract abs t =
  (case t of
    (c as \<^term>\<open>Rings.divide :: real => _\<close>) $ t1 $ t2 =>
      abs t1 ##>> abs t2 #>> (fn (u1, u2) => SOME (c $ u1 $ u2))
  | (c as \<^term>\<open>Int.of_int :: int => _\<close>) $ 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>\<open>real\<close>, K (SOME ("Real", [])), real_num) #>
  fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
    (\<^Const>\<open>less \<^Type>\<open>real\<close>\<close>, "<"),
    (\<^Const>\<open>less_eq \<^Type>\<open>real\<close>\<close>, "<="),
    (\<^Const>\<open>uminus \<^Type>\<open>real\<close>\<close>, "-"),
    (\<^Const>\<open>plus \<^Type>\<open>real\<close>\<close>, "+"),
    (\<^Const>\<open>minus \<^Type>\<open>real\<close>\<close>, "-") ] #>
  SMT_Builtin.add_builtin_fun SMTLIB_Interface.smtlibC
    (Term.dest_Const \<^Const>\<open>times \<^Type>\<open>real\<close>\<close>, times)

end

(* Z3 constructors *)

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

  fun smt_mk_builtin_num _ i T =
    if T = \<^typ>\<open>real\<close> then SOME (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 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>\<open>uminus :: real \<Rightarrow> _\<close>
  val add = \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close>
  val real0 = Numeral.mk_cnumber \<^ctyp>\<open>real\<close> 0
  val mk_sub = Thm.mk_binop \<^cterm>\<open>(-) :: real \<Rightarrow> _\<close>
  val mk_mul = Thm.mk_binop \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close>
  val mk_div = Thm.mk_binop \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
  val mk_lt = Thm.mk_binop \<^cterm>\<open>(<) :: real \<Rightarrow> _\<close>
  val mk_le = Thm.mk_binop \<^cterm>\<open>(\<le>) :: real \<Rightarrow> _\<close>

  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>\<open>real\<close> => smt_mk_builtin_fun sym cts
    | _ => NONE)) }

end

(* Z3 proof replay *)

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

(* 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;

quality100%

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.