added crafted list of SMT built-in constants
authorboehmes
Fri Oct 29 18:17:08 2010 +0200 (2010-10-29)
changeset 402774e3a3461c1a6
parent 40276 6efa052b9213
child 40278 0fc78bb54f18
added crafted list of SMT built-in constants
src/HOL/IsaMakefile
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_builtin.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Oct 29 18:17:06 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 29 18:17:08 2010 +0200
     1.3 @@ -337,6 +337,7 @@
     1.4    Tools/Sledgehammer/sledgehammer_atp_translate.ML \
     1.5    Tools/Sledgehammer/sledgehammer_util.ML \
     1.6    Tools/SMT/smtlib_interface.ML \
     1.7 +  Tools/SMT/smt_builtin.ML \
     1.8    Tools/SMT/smt_monomorph.ML \
     1.9    Tools/SMT/smt_normalize.ML \
    1.10    Tools/SMT/smt_setup_solvers.ML \
     2.1 --- a/src/HOL/SMT.thy	Fri Oct 29 18:17:06 2010 +0200
     2.2 +++ b/src/HOL/SMT.thy	Fri Oct 29 18:17:08 2010 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4  uses
     2.5    "Tools/Datatype/datatype_selectors.ML"
     2.6    ("Tools/SMT/smt_monomorph.ML")
     2.7 +  ("Tools/SMT/smt_builtin.ML")
     2.8    ("Tools/SMT/smt_normalize.ML")
     2.9    ("Tools/SMT/smt_translate.ML")
    2.10    ("Tools/SMT/smt_solver.ML")
    2.11 @@ -126,6 +127,7 @@
    2.12  subsection {* Setup *}
    2.13  
    2.14  use "Tools/SMT/smt_monomorph.ML"
    2.15 +use "Tools/SMT/smt_builtin.ML"
    2.16  use "Tools/SMT/smt_normalize.ML"
    2.17  use "Tools/SMT/smt_translate.ML"
    2.18  use "Tools/SMT/smt_solver.ML"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Fri Oct 29 18:17:08 2010 +0200
     3.3 @@ -0,0 +1,110 @@
     3.4 +(*  Title:      HOL/Tools/SMT/smt_builtin.ML
     3.5 +    Author:     Sascha Boehme, TU Muenchen
     3.6 +
     3.7 +Crafted collection of SMT built-in symbols.
     3.8 +
     3.9 +FIXME: This list is currently not automatically kept synchronized with the
    3.10 +remaining implementation.
    3.11 +*)
    3.12 +
    3.13 +signature SMT_BUILTIN =
    3.14 +sig
    3.15 +  val is_partially_builtin: Proof.context -> string * typ -> bool
    3.16 +  val is_builtin: Proof.context -> string * typ -> bool
    3.17 +end
    3.18 +
    3.19 +structure SMT_Builtin: SMT_BUILTIN =
    3.20 +struct
    3.21 +
    3.22 +fun is_arithT (Type (@{type_name fun}, [T, _])) =
    3.23 +      (case T of
    3.24 +        @{typ int} => true
    3.25 +      | @{typ nat} => true
    3.26 +      | Type ("RealDef.real", []) => true
    3.27 +      | _ => false)
    3.28 +  | is_arithT _ = false
    3.29 +
    3.30 +val builtins = Symtab.make [
    3.31 +
    3.32 +  (* Pure constants *)
    3.33 +  (@{const_name all}, K true),
    3.34 +  (@{const_name "=="}, K true),
    3.35 +  (@{const_name "==>"}, K true),
    3.36 +  (@{const_name Trueprop}, K true),
    3.37 +
    3.38 +  (* logical constants *)
    3.39 +  (@{const_name All}, K true),
    3.40 +  (@{const_name Ex}, K true),
    3.41 +  (@{const_name Ball}, K true),
    3.42 +  (@{const_name Bex}, K true),
    3.43 +  (@{const_name Ex1}, K true),
    3.44 +  (@{const_name True}, K true),
    3.45 +  (@{const_name False}, K true),
    3.46 +  (@{const_name Not}, K true),
    3.47 +  (@{const_name HOL.conj}, K true),
    3.48 +  (@{const_name HOL.disj}, K true),
    3.49 +  (@{const_name HOL.implies}, K true),
    3.50 +
    3.51 +  (* term abbreviations *)
    3.52 +  (@{const_name If}, K true),
    3.53 +  (@{const_name bool.bool_case}, K true),
    3.54 +  (@{const_name Let}, K true),
    3.55 +  (@{const_name SMT.distinct}, K true),
    3.56 +
    3.57 +  (* technicalities *)
    3.58 +  (@{const_name SMT.pat}, K true),
    3.59 +  (@{const_name SMT.nopat}, K true),
    3.60 +  (@{const_name SMT.trigger}, K true),
    3.61 +  (@{const_name SMT.fun_app}, K true),
    3.62 +  (@{const_name SMT.z3div}, K true),
    3.63 +  (@{const_name SMT.z3mod}, K true),
    3.64 +
    3.65 +  (* equality *)
    3.66 +  (@{const_name HOL.eq}, K true),
    3.67 +
    3.68 +  (* numerals *)
    3.69 +  (@{const_name zero_class.zero}, K true),
    3.70 +  (@{const_name one_class.one}, K true),
    3.71 +  (@{const_name Int.Pls}, K true),
    3.72 +  (@{const_name Int.Min}, K true),
    3.73 +  (@{const_name Int.Bit0}, K true),
    3.74 +  (@{const_name Int.Bit1}, K true),
    3.75 +  (@{const_name number_of}, K true),
    3.76 +
    3.77 +  (* arithmetic *)
    3.78 +  (@{const_name nat}, K true),
    3.79 +  (@{const_name of_nat}, K true),
    3.80 +  (@{const_name Suc}, K true),
    3.81 +  (@{const_name plus}, is_arithT),
    3.82 +  (@{const_name uminus}, is_arithT),
    3.83 +  (@{const_name minus}, is_arithT),
    3.84 +  (@{const_name abs}, is_arithT),
    3.85 +  (@{const_name min}, is_arithT),
    3.86 +  (@{const_name max}, is_arithT),
    3.87 +  (@{const_name less}, is_arithT),
    3.88 +  (@{const_name less_eq}, is_arithT),
    3.89 +  
    3.90 +  (* pairs *)
    3.91 +  (@{const_name fst}, K true),
    3.92 +  (@{const_name snd}, K true),
    3.93 +  (@{const_name Pair}, K true)
    3.94 +
    3.95 +  ]
    3.96 +
    3.97 +val all_builtins =
    3.98 +  builtins
    3.99 +  |> Symtab.update (@{const_name times}, is_arithT)
   3.100 +  |> Symtab.update (@{const_name div_class.div}, is_arithT)
   3.101 +  |> Symtab.update (@{const_name div_class.mod}, is_arithT)
   3.102 +  |> Symtab.update ("Rings.inverse_class.divide", is_arithT)
   3.103 +
   3.104 +fun lookup_builtin bs (name, T) =
   3.105 +  (case Symtab.lookup bs name of
   3.106 +    SOME proper_type => proper_type T
   3.107 +  | NONE => false)
   3.108 +
   3.109 +fun is_partially_builtin _ = lookup_builtin builtins
   3.110 +
   3.111 +fun is_builtin _ = lookup_builtin all_builtins
   3.112 +
   3.113 +end