1.1 --- a/src/HOL/SMT.thy Mon Dec 06 16:54:22 2010 +0100
1.2 +++ b/src/HOL/SMT.thy Tue Dec 07 14:53:12 2010 +0100
1.3 @@ -105,16 +105,18 @@
1.4 subsection {* First-order logic *}
1.5
1.6 text {*
1.7 -Some SMT solvers require a strict separation between formulas and
1.8 -terms. When translating higher-order into first-order problems,
1.9 -all uninterpreted constants (those not builtin in the target solver)
1.10 +Some SMT solvers only accept problems in first-order logic, i.e.,
1.11 +where formulas and terms are syntactically separated. When
1.12 +translating higher-order into first-order problems, all
1.13 +uninterpreted constants (those not built-in in the target solver)
1.14 are treated as function symbols in the first-order sense. Their
1.15 -occurrences as head symbols in atoms (i.e., as predicate symbols) is
1.16 -turned into terms by equating such atoms with @{term True} using the
1.17 -following term-level equation symbol.
1.18 +occurrences as head symbols in atoms (i.e., as predicate symbols) are
1.19 +turned into terms by equating such atoms with @{term True}.
1.20 +Whenever the boolean type occurs in first-order terms, it is replaced
1.21 +by the following type.
1.22 *}
1.23
1.24 -definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
1.25 +typedecl term_bool
1.26
1.27
1.28
1.29 @@ -159,7 +161,10 @@
1.30
1.31 setup {*
1.32 SMT_Config.setup #>
1.33 + SMT_Normalize.setup #>
1.34 SMT_Solver.setup #>
1.35 + SMTLIB_Interface.setup #>
1.36 + Z3_Interface.setup #>
1.37 Z3_Proof_Reconstruction.setup #>
1.38 SMT_Setup_Solvers.setup
1.39 *}
1.40 @@ -354,9 +359,10 @@
1.41
1.42
1.43
1.44 +hide_type term_bool
1.45 hide_type (open) pattern
1.46 -hide_const Pattern term_eq
1.47 -hide_const (open) trigger pat nopat weight fun_app z3div z3mod
1.48 +hide_const Pattern fun_app
1.49 +hide_const (open) trigger pat nopat weight z3div z3mod
1.50
1.51
1.52
2.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML Mon Dec 06 16:54:22 2010 +0100
2.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 07 14:53:12 2010 +0100
2.3 @@ -1,116 +1,226 @@
2.4 (* Title: HOL/Tools/SMT/smt_builtin.ML
2.5 Author: Sascha Boehme, TU Muenchen
2.6
2.7 -Crafted collection of SMT built-in symbols.
2.8 -
2.9 -FIXME: This list is currently not automatically kept synchronized with the
2.10 -remaining implementation.
2.11 +Tables of types and terms directly supported by SMT solvers.
2.12 *)
2.13
2.14 signature SMT_BUILTIN =
2.15 sig
2.16 - val is_builtin: Proof.context -> string * typ -> bool
2.17 - val is_partially_builtin: Proof.context -> string * typ -> bool
2.18 + (*built-in types*)
2.19 + val add_builtin_typ: SMT_Config.class ->
2.20 + typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
2.21 + theory
2.22 + val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
2.23 + val builtin_typ: Proof.context -> typ -> string option
2.24 + val is_builtin_typ: Proof.context -> typ -> bool
2.25 + val is_builtin_typ_ext: Proof.context -> typ -> bool
2.26 +
2.27 + (*built-in numbers*)
2.28 + val builtin_num: Proof.context -> term -> string option
2.29 + val is_builtin_num: Proof.context -> term -> bool
2.30 + val is_builtin_num_ext: Proof.context -> term -> bool
2.31 +
2.32 + (*built-in functions*)
2.33 + type 'a bfun = Proof.context -> typ -> term list -> 'a
2.34 + val add_builtin_fun: SMT_Config.class ->
2.35 + (string * typ) * (string * term list) option bfun -> theory -> theory
2.36 + val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
2.37 + val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
2.38 + val add_builtin_fun_ext': string * typ -> theory -> theory
2.39 + val add_builtin_fun_ext'': string -> theory -> theory
2.40 + val builtin_fun: Proof.context -> string * typ -> term list ->
2.41 + (string * term list) option
2.42 + val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
2.43 + val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
2.44 + val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
2.45 + val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
2.46 end
2.47
2.48 structure SMT_Builtin: SMT_BUILTIN =
2.49 struct
2.50
2.51 -fun is_arithT T =
2.52 - (case T of
2.53 - @{typ int} => true
2.54 - | @{typ nat} => true
2.55 - | Type ("RealDef.real", []) => true
2.56 - | _ => false)
2.57 +structure C = SMT_Config
2.58
2.59 -fun is_arithT_dom (Type (@{type_name fun}, [T, _])) = is_arithT T
2.60 - | is_arithT_dom _ = false
2.61 -fun is_arithT_ran (Type (@{type_name fun}, [_, T])) = is_arithT T
2.62 - | is_arithT_ran _ = false
2.63
2.64 -val builtins = Symtab.make [
2.65 +(* built-in tables *)
2.66
2.67 - (* Pure constants *)
2.68 - (@{const_name all}, K true),
2.69 - (@{const_name "=="}, K true),
2.70 - (@{const_name "==>"}, K true),
2.71 - (@{const_name Trueprop}, K true),
2.72 +datatype ('a, 'b) kind = Ext of 'a | Int of 'b
2.73
2.74 - (* logical constants *)
2.75 - (@{const_name All}, K true),
2.76 - (@{const_name Ex}, K true),
2.77 - (@{const_name Ball}, K true),
2.78 - (@{const_name Bex}, K true),
2.79 - (@{const_name Ex1}, K true),
2.80 - (@{const_name True}, K true),
2.81 - (@{const_name False}, K true),
2.82 - (@{const_name Not}, K true),
2.83 - (@{const_name HOL.conj}, K true),
2.84 - (@{const_name HOL.disj}, K true),
2.85 - (@{const_name HOL.implies}, K true),
2.86 +type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list
2.87
2.88 - (* term abbreviations *)
2.89 - (@{const_name If}, K true),
2.90 - (@{const_name bool.bool_case}, K true),
2.91 - (@{const_name Let}, K true),
2.92 - (* (@{const_name distinct}, K true), -- not a real builtin, only when
2.93 - applied to an explicit list *)
2.94 +fun empty_ttab () = []
2.95
2.96 - (* technicalities *)
2.97 - (@{const_name SMT.pat}, K true),
2.98 - (@{const_name SMT.nopat}, K true),
2.99 - (@{const_name SMT.trigger}, K true),
2.100 - (@{const_name SMT.weight}, K true),
2.101 - (@{const_name SMT.fun_app}, K true),
2.102 - (@{const_name SMT.z3div}, K true),
2.103 - (@{const_name SMT.z3mod}, K true),
2.104 +fun typ_ord ((T, _), (U, _)) =
2.105 + let
2.106 + fun tord (TVar _, Type _) = GREATER
2.107 + | tord (Type _, TVar _) = LESS
2.108 + | tord (Type (n, Ts), Type (m, Us)) =
2.109 + if n = m then list_ord tord (Ts, Us)
2.110 + else Term_Ord.typ_ord (T, U)
2.111 + | tord TU = Term_Ord.typ_ord TU
2.112 + in tord (T, U) end
2.113
2.114 - (* equality *)
2.115 - (@{const_name HOL.eq}, K true),
2.116 +fun insert_ttab cs T f =
2.117 + AList.map_default (op =) (cs, [])
2.118 + (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
2.119
2.120 - (* numerals *)
2.121 - (@{const_name zero_class.zero}, is_arithT),
2.122 - (@{const_name one_class.one}, is_arithT),
2.123 - (@{const_name Int.Pls}, K true),
2.124 - (@{const_name Int.Min}, K true),
2.125 - (@{const_name Int.Bit0}, K true),
2.126 - (@{const_name Int.Bit1}, K true),
2.127 - (@{const_name number_of}, is_arithT_ran),
2.128 +fun merge_ttab ttabp =
2.129 + AList.join (op =) (K (uncurry (Ord_List.union typ_ord) o swap)) ttabp
2.130
2.131 - (* arithmetic *)
2.132 - (@{const_name nat}, K true),
2.133 - (@{const_name of_nat}, K true),
2.134 - (@{const_name Suc}, K true),
2.135 - (@{const_name plus}, is_arithT_dom),
2.136 - (@{const_name uminus}, is_arithT_dom),
2.137 - (@{const_name minus}, is_arithT_dom),
2.138 - (@{const_name abs}, is_arithT_dom),
2.139 - (@{const_name min}, is_arithT_dom),
2.140 - (@{const_name max}, is_arithT_dom),
2.141 - (@{const_name less}, is_arithT_dom),
2.142 - (@{const_name less_eq}, is_arithT_dom),
2.143 -
2.144 - (* pairs *)
2.145 - (@{const_name fst}, K true),
2.146 - (@{const_name snd}, K true),
2.147 - (@{const_name Pair}, K true)
2.148 +fun lookup_ttab ctxt ttab T =
2.149 + let
2.150 + val cs = C.solver_class_of ctxt
2.151 + fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
2.152
2.153 - ]
2.154 + fun matching (cs', Txs) =
2.155 + if is_prefix (op =) cs' cs then find_first match Txs
2.156 + else NONE
2.157 + in get_first matching ttab end
2.158
2.159 -val all_builtins =
2.160 - builtins
2.161 - |> Symtab.update (@{const_name times}, is_arithT_dom)
2.162 - |> Symtab.update (@{const_name div_class.div}, is_arithT_dom)
2.163 - |> Symtab.update (@{const_name div_class.mod}, is_arithT_dom)
2.164 - |> Symtab.update ("Rings.inverse_class.divide", is_arithT_dom)
2.165 +type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
2.166
2.167 -fun lookup_builtin bs (name, T) =
2.168 - (case Symtab.lookup bs name of
2.169 - SOME proper_type => proper_type T
2.170 +fun empty_btab () = Symtab.empty
2.171 +
2.172 +fun insert_btab cs n T f =
2.173 + Symtab.map_default (n, []) (insert_ttab cs T f)
2.174 +
2.175 +fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
2.176 +
2.177 +fun lookup_btab ctxt btab (n, T) =
2.178 + (case Symtab.lookup btab n of
2.179 + NONE => NONE
2.180 + | SOME ttab => lookup_ttab ctxt ttab T)
2.181 +
2.182 +
2.183 +(* built-in types *)
2.184 +
2.185 +structure Builtin_Types = Theory_Data
2.186 +(
2.187 + type T =
2.188 + (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
2.189 + val empty = empty_ttab ()
2.190 + val extend = I
2.191 + val merge = merge_ttab
2.192 +)
2.193 +
2.194 +fun add_builtin_typ cs (T, f, g) =
2.195 + Builtin_Types.map (insert_ttab cs T (Int (f, g)))
2.196 +
2.197 +fun add_builtin_typ_ext (T, f) =
2.198 + Builtin_Types.map (insert_ttab C.basicC T (Ext f))
2.199 +
2.200 +fun lookup_builtin_typ ctxt =
2.201 + lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
2.202 +
2.203 +fun builtin_typ ctxt T =
2.204 + (case lookup_builtin_typ ctxt T of
2.205 + SOME (_, Int (f, _)) => f T
2.206 + | _ => NONE)
2.207 +
2.208 +fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
2.209 +
2.210 +fun is_builtin_typ_ext ctxt T =
2.211 + (case lookup_builtin_typ ctxt T of
2.212 + SOME (_, Int (f, _)) => is_some (f T)
2.213 + | SOME (_, Ext f) => f T
2.214 | NONE => false)
2.215
2.216 -fun is_builtin _ = lookup_builtin builtins
2.217
2.218 -fun is_partially_builtin _ = lookup_builtin all_builtins
2.219 +(* built-in numbers *)
2.220 +
2.221 +fun builtin_num ctxt t =
2.222 + (case try HOLogic.dest_number t of
2.223 + NONE => NONE
2.224 + | SOME (T, i) =>
2.225 + (case lookup_builtin_typ ctxt T of
2.226 + SOME (_, Int (_, g)) => g T i
2.227 + | _ => NONE))
2.228 +
2.229 +val is_builtin_num = is_some oo builtin_num
2.230 +
2.231 +fun is_builtin_num_ext ctxt t =
2.232 + (case try HOLogic.dest_number t of
2.233 + NONE => false
2.234 + | SOME (T, _) => is_builtin_typ_ext ctxt T)
2.235 +
2.236 +
2.237 +(* built-in functions *)
2.238 +
2.239 +type 'a bfun = Proof.context -> typ -> term list -> 'a
2.240 +
2.241 +fun true3 _ _ _ = true
2.242 +
2.243 +fun raw_add_builtin_fun_ext thy cs n =
2.244 + insert_btab cs n (Sign.the_const_type thy n) (Ext true3)
2.245 +
2.246 +val basic_builtin_fun_names = [
2.247 + @{const_name SMT.pat}, @{const_name SMT.nopat},
2.248 + @{const_name SMT.trigger}, @{const_name SMT.weight}]
2.249 +
2.250 +fun basic_builtin_funcs () =
2.251 + empty_btab ()
2.252 + |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
2.253 + (* FIXME: SMT_Normalize should check that they are properly used *)
2.254 +
2.255 +structure Builtin_Funcs = Theory_Data
2.256 +(
2.257 + type T = (bool bfun, (string * term list) option bfun) btab
2.258 + val empty = basic_builtin_funcs ()
2.259 + val extend = I
2.260 + val merge = merge_btab
2.261 +)
2.262 +
2.263 +fun add_builtin_fun cs ((n, T), f) =
2.264 + Builtin_Funcs.map (insert_btab cs n T (Int f))
2.265 +
2.266 +fun add_builtin_fun' cs (t, n) =
2.267 + add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
2.268 +
2.269 +fun add_builtin_fun_ext ((n, T), f) =
2.270 + Builtin_Funcs.map (insert_btab C.basicC n T (Ext f))
2.271 +
2.272 +fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
2.273 +
2.274 +fun add_builtin_fun_ext'' n thy =
2.275 + add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
2.276 +
2.277 +fun lookup_builtin_fun ctxt =
2.278 + lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
2.279 +
2.280 +fun builtin_fun ctxt (c as (_, T)) ts =
2.281 + (case lookup_builtin_fun ctxt c of
2.282 + SOME (_, Int f) => f ctxt T ts
2.283 + | _ => NONE)
2.284 +
2.285 +fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
2.286 +
2.287 +fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
2.288 + (case lookup_builtin_fun ctxt c of
2.289 + SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
2.290 + | _ => false)
2.291 +
2.292 +fun is_pred_type T = Term.body_type T = @{typ bool}
2.293 +fun is_conn_type T =
2.294 + forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
2.295 +
2.296 +fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
2.297 +fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
2.298 +
2.299 +fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
2.300 + (case lookup_builtin_fun ctxt c of
2.301 + SOME (_, Int f) => is_some (f ctxt T ts)
2.302 + | SOME (_, Ext f) => f ctxt T ts
2.303 + | NONE => false)
2.304 +
2.305 +(* FIXME: move this information to the interfaces *)
2.306 +val only_partially_supported = [
2.307 + @{const_name times},
2.308 + @{const_name div_class.div},
2.309 + @{const_name div_class.mod},
2.310 + @{const_name inverse_class.divide} ]
2.311 +
2.312 +fun is_builtin_ext ctxt (c as (n, _)) ts =
2.313 + if member (op =) only_partially_supported n then false
2.314 + else is_builtin_fun_ext ctxt c ts
2.315
2.316 end
3.1 --- a/src/HOL/Tools/SMT/smt_config.ML Mon Dec 06 16:54:22 2010 +0100
3.2 +++ b/src/HOL/Tools/SMT/smt_config.ML Tue Dec 07 14:53:12 2010 +0100
3.3 @@ -6,11 +6,16 @@
3.4
3.5 signature SMT_CONFIG =
3.6 sig
3.7 + (*class*)
3.8 + type class = string list
3.9 + val basicC: class
3.10 +
3.11 (*solver*)
3.12 - val add_solver: string -> Context.generic -> Context.generic
3.13 + val add_solver: string * class -> Context.generic -> Context.generic
3.14 val set_solver_options: string * string -> Context.generic -> Context.generic
3.15 val select_solver: string -> Context.generic -> Context.generic
3.16 val solver_of: Proof.context -> string
3.17 + val solver_class_of: Proof.context -> class
3.18 val solver_options_of: Proof.context -> string list
3.19
3.20 (*options*)
3.21 @@ -46,11 +51,18 @@
3.22 structure SMT_Config: SMT_CONFIG =
3.23 struct
3.24
3.25 +(* class *)
3.26 +
3.27 +type class = string list
3.28 +
3.29 +val basicC = []
3.30 +
3.31 +
3.32 (* solver *)
3.33
3.34 structure Solvers = Generic_Data
3.35 (
3.36 - type T = string list Symtab.table * string option
3.37 + type T = (class * string list) Symtab.table * string option
3.38 val empty = (Symtab.empty, NONE)
3.39 val extend = I
3.40 fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
3.41 @@ -58,14 +70,14 @@
3.42
3.43 fun set_solver_options (name, options) =
3.44 let val opts = String.tokens (Symbol.is_ascii_blank o str) options
3.45 - in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
3.46 + in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
3.47
3.48 -fun add_solver name context =
3.49 +fun add_solver (name, class) context =
3.50 if Symtab.defined (fst (Solvers.get context)) name then
3.51 error ("Solver already registered: " ^ quote name)
3.52 else
3.53 context
3.54 - |> Solvers.map (apfst (Symtab.update (name, [])))
3.55 + |> Solvers.map (apfst (Symtab.update (name, (class, []))))
3.56 |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
3.57 (Scan.lift (Parse.$$$ "=" |-- Args.name) >>
3.58 (Thm.declaration_attribute o K o set_solver_options o pair name))
3.59 @@ -76,18 +88,23 @@
3.60 Solvers.map (apsnd (K (SOME name))) context
3.61 else error ("Trying to select unknown solver: " ^ quote name)
3.62
3.63 -val lookup_solver = snd o Solvers.get o Context.Proof
3.64 +fun no_solver_err () = error "No SMT solver selected"
3.65
3.66 fun solver_of ctxt =
3.67 - (case lookup_solver ctxt of
3.68 - SOME name => name
3.69 - | NONE => error "No SMT solver selected")
3.70 + (case Solvers.get (Context.Proof ctxt) of
3.71 + (_, SOME name) => name
3.72 + | (_, NONE) => no_solver_err ())
3.73 +
3.74 +fun solver_class_of ctxt =
3.75 + (case Solvers.get (Context.Proof ctxt) of
3.76 + (solvers, SOME name) => fst (the (Symtab.lookup solvers name))
3.77 + | (_, NONE) => no_solver_err())
3.78
3.79 fun solver_options_of ctxt =
3.80 - (case lookup_solver ctxt of
3.81 - NONE => []
3.82 - | SOME name =>
3.83 - Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
3.84 + (case Solvers.get (Context.Proof ctxt) of
3.85 + (solvers, SOME name) =>
3.86 + (case Symtab.lookup solvers name of SOME (_, opts) => opts | NONE => [])
3.87 + | (_, NONE) => [])
3.88
3.89 val setup_solver =
3.90 Attrib.setup @{binding smt_solver}
4.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Dec 06 16:54:22 2010 +0100
4.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Dec 07 14:53:12 2010 +0100
4.3 @@ -23,12 +23,14 @@
4.4 (int * thm) list * Proof.context
4.5 val atomize_conv: Proof.context -> conv
4.6 val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
4.7 + val setup: theory -> theory
4.8 end
4.9
4.10 structure SMT_Normalize: SMT_NORMALIZE =
4.11 struct
4.12
4.13 structure U = SMT_Utils
4.14 +structure B = SMT_Builtin
4.15
4.16 infix 2 ??
4.17 fun (test ?? f) x = if test x then f x else x
4.18 @@ -95,6 +97,9 @@
4.19 fun rewrite_bool_cases ctxt =
4.20 map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
4.21 Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
4.22 +
4.23 +val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
4.24 +
4.25 end
4.26
4.27
4.28 @@ -203,10 +208,20 @@
4.29 val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
4.30 val uses_nat_int = Term.exists_subterm (member (op aconv)
4.31 [@{const of_nat (int)}, @{const nat}])
4.32 +
4.33 + val nat_ops = [
4.34 + @{const less (nat)}, @{const less_eq (nat)},
4.35 + @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
4.36 + @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
4.37 + val nat_ops' = @{const of_nat (int)} :: @{const nat} :: nat_ops
4.38 in
4.39 fun nat_as_int ctxt =
4.40 map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
4.41 exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
4.42 +
4.43 +val setup_nat_as_int =
4.44 + B.add_builtin_typ_ext (@{typ nat}, K true) #>
4.45 + fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
4.46 end
4.47
4.48
4.49 @@ -263,7 +278,7 @@
4.50 | _ =>
4.51 (case Term.strip_comb (Thm.term_of ct) of
4.52 (Const (c as (_, T)), ts) =>
4.53 - if SMT_Builtin.is_partially_builtin ctxt c
4.54 + if SMT_Builtin.is_builtin_fun ctxt c ts
4.55 then eta_args_conv norm_conv
4.56 (length (Term.binder_types T) - length ts)
4.57 else args_conv o norm_conv
4.58 @@ -294,7 +309,7 @@
4.59 | _ =>
4.60 (case Term.strip_comb t of
4.61 (Const (c as (_, T)), ts) =>
4.62 - if SMT_Builtin.is_builtin ctxt c
4.63 + if SMT_Builtin.is_builtin_fun ctxt c ts
4.64 then length (Term.binder_types T) = length ts andalso
4.65 forall (is_normed ctxt) ts
4.66 else forall (is_normed ctxt) ts
4.67 @@ -302,6 +317,11 @@
4.68 in
4.69 fun norm_binder_conv ctxt =
4.70 U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
4.71 +
4.72 +val setup_unfolded_quants =
4.73 + fold B.add_builtin_fun_ext'' [@{const_name Ball}, @{const_name Bex},
4.74 + @{const_name Ex1}]
4.75 +
4.76 end
4.77
4.78 fun norm_def ctxt thm =
4.79 @@ -325,6 +345,10 @@
4.80 Conv.rewr_conv @{thm atomize_all}
4.81 | _ => Conv.all_conv) ct
4.82
4.83 +val setup_atomize =
4.84 + fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
4.85 + @{const_name all}, @{const_name Trueprop}]
4.86 +
4.87 fun normalize_rule ctxt =
4.88 Conv.fconv_rule (
4.89 (* reduce lambda abstractions, except at known binders: *)
4.90 @@ -554,4 +578,14 @@
4.91 |-> (if with_datatypes then datatype_selectors else pair)
4.92 end
4.93
4.94 +
4.95 +
4.96 +(* setup *)
4.97 +
4.98 +val setup =
4.99 + setup_bool_case #>
4.100 + setup_nat_as_int #>
4.101 + setup_unfolded_quants #>
4.102 + setup_atomize
4.103 +
4.104 end
5.1 --- a/src/HOL/Tools/SMT/smt_real.ML Mon Dec 06 16:54:22 2010 +0100
5.2 +++ b/src/HOL/Tools/SMT/smt_real.ML Tue Dec 07 14:53:12 2010 +0100
5.3 @@ -12,6 +12,8 @@
5.4 structure SMT_Real: SMT_REAL =
5.5 struct
5.6
5.7 +structure B = SMT_Builtin
5.8 +
5.9
5.10 (* SMT-LIB logic *)
5.11
5.12 @@ -21,58 +23,28 @@
5.13 else NONE
5.14
5.15
5.16 -
5.17 -(* SMT-LIB builtins *)
5.18 +(* SMT-LIB and Z3 built-ins *)
5.19
5.20 local
5.21 - fun smtlib_builtin_typ @{typ real} = SOME "Real"
5.22 - | smtlib_builtin_typ _ = NONE
5.23 + val smtlibC = SMTLIB_Interface.smtlibC
5.24
5.25 - fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
5.26 - | smtlib_builtin_num _ _ = NONE
5.27 -
5.28 - fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
5.29 - | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
5.30 - | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
5.31 - | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
5.32 - | smtlib_builtin_func _ _ = NONE
5.33 -
5.34 - fun smtlib_builtin_pred @{const_name less} = SOME "<"
5.35 - | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
5.36 - | smtlib_builtin_pred _ = NONE
5.37 -
5.38 - fun real_fun T y f x =
5.39 - (case try Term.domain_type T of
5.40 - SOME @{typ real} => f x
5.41 - | _ => y)
5.42 + fun real_num _ i = SOME (string_of_int i ^ ".0")
5.43 in
5.44
5.45 -val smtlib_builtins = {
5.46 - builtin_typ = smtlib_builtin_typ,
5.47 - builtin_num = smtlib_builtin_num,
5.48 - builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
5.49 - builtin_pred = (fn (n, T) => fn ts =>
5.50 - real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
5.51 - is_builtin_pred = (fn n => fn T =>
5.52 - real_fun T false (is_some o smtlib_builtin_pred) n) }
5.53 +val setup_builtins =
5.54 + B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
5.55 + fold (B.add_builtin_fun' smtlibC) [
5.56 + (@{const uminus (real)}, "~"),
5.57 + (@{const plus (real)}, "+"),
5.58 + (@{const minus (real)}, "-"),
5.59 + (@{const times (real)}, "*"),
5.60 + (@{const less (real)}, "<"),
5.61 + (@{const less_eq (real)}, "<=") ] #>
5.62 + B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
5.63
5.64 end
5.65
5.66
5.67 -
5.68 -(* Z3 builtins *)
5.69 -
5.70 -local
5.71 - fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
5.72 - | z3_builtin_fun _ _ = NONE
5.73 -in
5.74 -
5.75 -val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
5.76 -
5.77 -end
5.78 -
5.79 -
5.80 -
5.81 (* Z3 constructors *)
5.82
5.83 local
5.84 @@ -117,7 +89,6 @@
5.85 end
5.86
5.87
5.88 -
5.89 (* Z3 proof reconstruction *)
5.90
5.91 val real_rules = @{lemma
5.92 @@ -132,14 +103,12 @@
5.93 "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
5.94
5.95
5.96 -
5.97 (* setup *)
5.98
5.99 val setup =
5.100 + setup_builtins #>
5.101 Context.theory_map (
5.102 - SMTLIB_Interface.add_logic smtlib_logic #>
5.103 - SMTLIB_Interface.add_builtins smtlib_builtins #>
5.104 - Z3_Interface.add_builtin_funs z3_builtins #>
5.105 + SMTLIB_Interface.add_logic (10, smtlib_logic) #>
5.106 Z3_Interface.add_mk_builtins z3_mk_builtins #>
5.107 fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
5.108 Z3_Proof_Tools.add_simproc real_linarith_proc)
6.1 --- a/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 06 16:54:22 2010 +0100
6.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 14:53:12 2010 +0100
6.3 @@ -8,6 +8,7 @@
6.4 sig
6.5 (*configuration*)
6.6 type interface = {
6.7 + class: SMT_Config.class,
6.8 extra_norm: SMT_Normalize.extra_norm,
6.9 translate: SMT_Translate.config }
6.10 datatype outcome = Unsat | Sat | Unknown
6.11 @@ -57,6 +58,7 @@
6.12 (* configuration *)
6.13
6.14 type interface = {
6.15 + class: SMT_Config.class,
6.16 extra_norm: SMT_Normalize.extra_norm,
6.17 translate: SMT_Translate.config }
6.18
6.19 @@ -195,13 +197,10 @@
6.20
6.21 fun set_has_datatypes with_datatypes translate =
6.22 let
6.23 - val {prefixes, header, strict, builtins, serialize} = translate
6.24 - val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
6.25 + val {prefixes, header, is_fol, has_datatypes, serialize} = translate
6.26 val with_datatypes' = has_datatypes andalso with_datatypes
6.27 - val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
6.28 - builtin_fun=builtin_fun, has_datatypes=with_datatypes}
6.29 - val translate' = {prefixes=prefixes, header=header, strict=strict,
6.30 - builtins=builtins', serialize=serialize}
6.31 + val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
6.32 + has_datatypes=with_datatypes', serialize=serialize}
6.33 in (with_datatypes', translate') end
6.34
6.35 fun trace_assumptions ctxt irules idxs =
6.36 @@ -219,7 +218,7 @@
6.37 fun gen_solver name info rm ctxt irules =
6.38 let
6.39 val {env_var, is_remote, options, interface, reconstruct, ...} = info
6.40 - val {extra_norm, translate} = interface
6.41 + val {extra_norm, translate, ...} = interface
6.42 val (with_datatypes, translate') =
6.43 set_has_datatypes (Config.get ctxt C.datatypes) translate
6.44 val cmd = (rm, env_var, is_remote, name)
6.45 @@ -284,6 +283,7 @@
6.46 let
6.47 val {name, env_var, is_remote, options, interface, outcome, cex_parser,
6.48 reconstruct, default_max_relevant} = cfg
6.49 + val {class, ...} = interface
6.50
6.51 fun core_oracle () = cfalse
6.52
6.53 @@ -294,7 +294,7 @@
6.54 in
6.55 Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
6.56 Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
6.57 - Context.theory_map (C.add_solver name)
6.58 + Context.theory_map (C.add_solver (name, class))
6.59 end
6.60
6.61 end
7.1 --- a/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 06 16:54:22 2010 +0100
7.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Dec 07 14:53:12 2010 +0100
7.3 @@ -17,17 +17,6 @@
7.4
7.5 (* configuration options *)
7.6 type prefixes = {sort_prefix: string, func_prefix: string}
7.7 - type header = Proof.context -> term list -> string list
7.8 - type strict = {
7.9 - is_builtin_conn: string * typ -> bool,
7.10 - is_builtin_pred: Proof.context -> string * typ -> bool,
7.11 - is_builtin_distinct: bool}
7.12 - type builtins = {
7.13 - builtin_typ: Proof.context -> typ -> string option,
7.14 - builtin_num: Proof.context -> typ -> int -> string option,
7.15 - builtin_fun: Proof.context -> string * typ -> term list ->
7.16 - (string * term list) option,
7.17 - has_datatypes: bool }
7.18 type sign = {
7.19 header: string list,
7.20 sorts: string list,
7.21 @@ -35,9 +24,9 @@
7.22 funcs: (string * (string list * string)) list }
7.23 type config = {
7.24 prefixes: prefixes,
7.25 - header: header,
7.26 - strict: strict option,
7.27 - builtins: builtins,
7.28 + header: Proof.context -> term list -> string list,
7.29 + is_fol: bool,
7.30 + has_datatypes: bool,
7.31 serialize: string list -> sign -> sterm list -> string }
7.32 type recon = {
7.33 typs: typ Symtab.table,
7.34 @@ -53,6 +42,7 @@
7.35 struct
7.36
7.37 structure U = SMT_Utils
7.38 +structure B = SMT_Builtin
7.39
7.40
7.41 (* intermediate term structure *)
7.42 @@ -73,20 +63,6 @@
7.43
7.44 type prefixes = {sort_prefix: string, func_prefix: string}
7.45
7.46 -type header = Proof.context -> term list -> string list
7.47 -
7.48 -type strict = {
7.49 - is_builtin_conn: string * typ -> bool,
7.50 - is_builtin_pred: Proof.context -> string * typ -> bool,
7.51 - is_builtin_distinct: bool}
7.52 -
7.53 -type builtins = {
7.54 - builtin_typ: Proof.context -> typ -> string option,
7.55 - builtin_num: Proof.context -> typ -> int -> string option,
7.56 - builtin_fun: Proof.context -> string * typ -> term list ->
7.57 - (string * term list) option,
7.58 - has_datatypes: bool }
7.59 -
7.60 type sign = {
7.61 header: string list,
7.62 sorts: string list,
7.63 @@ -95,9 +71,9 @@
7.64
7.65 type config = {
7.66 prefixes: prefixes,
7.67 - header: header,
7.68 - strict: strict option,
7.69 - builtins: builtins,
7.70 + header: Proof.context -> term list -> string list,
7.71 + is_fol: bool,
7.72 + has_datatypes: bool,
7.73 serialize: string list -> sign -> sterm list -> string }
7.74
7.75 type recon = {
7.76 @@ -152,13 +128,20 @@
7.77
7.78
7.79
7.80 -(* enforce a strict separation between formulas and terms *)
7.81 +(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *)
7.82
7.83 -val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
7.84 +val tboolT = @{typ SMT.term_bool}
7.85 +val term_true = Const (@{const_name True}, tboolT)
7.86 +val term_false = Const (@{const_name False}, tboolT)
7.87
7.88 -val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
7.89 -val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
7.90 -
7.91 +val term_bool = @{lemma "True ~= False" by simp}
7.92 +val term_bool_prop =
7.93 + let
7.94 + fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
7.95 + | replace @{const True} = term_true
7.96 + | replace @{const False} = term_false
7.97 + | replace t = t
7.98 + in Term.map_aterms replace (prop_of term_bool) end
7.99
7.100 val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
7.101 Const (@{const_name Let}, _) => true
7.102 @@ -171,63 +154,57 @@
7.103 @{lemma "P = True == P" by (rule eq_reflection) simp},
7.104 @{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
7.105
7.106 -fun rewrite ctxt = Simplifier.full_rewrite
7.107 - (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
7.108 +fun rewrite ctxt ct =
7.109 + Conv.top_sweep_conv (fn ctxt' =>
7.110 + Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct
7.111
7.112 fun normalize ctxt thm =
7.113 if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
7.114
7.115 -val unfold_rules = term_eq_rewr :: rewrite_rules
7.116 +fun revert_typ @{typ SMT.term_bool} = @{typ bool}
7.117 + | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
7.118 + | revert_typ T = T
7.119
7.120 +val revert_types = Term.map_types revert_typ
7.121
7.122 -val revert_types =
7.123 +fun folify ctxt =
7.124 let
7.125 - fun revert @{typ prop} = @{typ bool}
7.126 - | revert (Type (n, Ts)) = Type (n, map revert Ts)
7.127 - | revert T = T
7.128 - in Term.map_types revert end
7.129 + fun is_builtin_conn (@{const_name True}, _) _ = false
7.130 + | is_builtin_conn (@{const_name False}, _) _ = false
7.131 + | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts
7.132
7.133 + fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
7.134
7.135 -fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
7.136 - let
7.137 - fun is_builtin_conn' (@{const_name True}, _) = false
7.138 - | is_builtin_conn' (@{const_name False}, _) = false
7.139 - | is_builtin_conn' c = is_builtin_conn c
7.140 + fun as_tbool @{typ bool} = tboolT
7.141 + | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
7.142 + | as_tbool T = T
7.143 + fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
7.144 + fun predT T = mapTs as_tbool I T
7.145 + fun funcT T = mapTs as_tbool as_tbool T
7.146 + fun func (n, T) = Const (n, funcT T)
7.147
7.148 - fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
7.149 - is_builtin_distinct andalso can HOLogic.dest_list t
7.150 - | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
7.151 -
7.152 - val propT = @{typ prop} and boolT = @{typ bool}
7.153 - val as_propT = (fn @{typ bool} => propT | T => T)
7.154 - fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
7.155 - fun conn (n, T) = (n, mapTs as_propT as_propT T)
7.156 - fun pred (n, T) = (n, mapTs I as_propT T)
7.157 -
7.158 - val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
7.159 - fun as_term t = Const term_eq $ t $ @{const True}
7.160 -
7.161 - val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
7.162 - fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
7.163 + fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->)
7.164 + val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
7.165 + fun wrap_in_if t = if_term $ t $ term_true $ term_false
7.166
7.167 fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
7.168
7.169 fun in_term t =
7.170 (case Term.strip_comb t of
7.171 - (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
7.172 - c $ in_form t1 $ in_term t2 $ in_term t3
7.173 - | (h as Const c, ts) =>
7.174 - if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
7.175 + (Const (c as @{const_name If}, T), [t1, t2, t3]) =>
7.176 + Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
7.177 + | (Const c, ts) =>
7.178 + if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts
7.179 then wrap_in_if (in_form t)
7.180 - else Term.list_comb (h, map in_term ts)
7.181 - | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
7.182 + else Term.list_comb (func c, map in_term ts)
7.183 + | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts)
7.184 | _ => t)
7.185
7.186 and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
7.187 | in_weight t = in_form t
7.188
7.189 - and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
7.190 - | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
7.191 + and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t
7.192 + | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t
7.193 | in_pat t = raise TERM ("in_pat", [t])
7.194
7.195 and in_pats ps =
7.196 @@ -239,23 +216,23 @@
7.197 and in_form t =
7.198 (case Term.strip_comb t of
7.199 (q as Const (qn, _), [Abs (n, T, t')]) =>
7.200 - if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
7.201 + if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t')
7.202 else as_term (in_term t)
7.203 - | (Const (c as (@{const_name distinct}, T)), [t']) =>
7.204 - if is_builtin_distinct andalso can HOLogic.dest_list t' then
7.205 - Const (pred c) $ in_list T in_term t'
7.206 + | (Const (c as (n as @{const_name distinct}, T)), [t']) =>
7.207 + if B.is_builtin_fun ctxt c [t'] then
7.208 + Const (n, predT T) $ in_list T in_term t'
7.209 else as_term (in_term t)
7.210 - | (Const c, ts) =>
7.211 - if is_builtin_conn (conn c)
7.212 - then Term.list_comb (Const (conn c), map in_form ts)
7.213 - else if is_builtin_pred ctxt (pred c)
7.214 - then Term.list_comb (Const (pred c), map in_term ts)
7.215 + | (Const (c as (n, T)), ts) =>
7.216 + if B.is_builtin_conn ctxt c ts
7.217 + then Term.list_comb (Const c, map in_form ts)
7.218 + else if B.is_builtin_pred ctxt c ts
7.219 + then Term.list_comb (Const (n, predT T), map in_term ts)
7.220 else as_term (in_term t)
7.221 | _ => as_term (in_term t))
7.222 in
7.223 map (apsnd (normalize ctxt)) #> (fn irules =>
7.224 - ((unfold_rules, (~1, term_bool') :: irules),
7.225 - map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
7.226 + ((rewrite_rules, (~1, term_bool) :: irules),
7.227 + term_bool_prop :: map (in_form o prop_of o snd) irules))
7.228 end
7.229
7.230
7.231 @@ -280,10 +257,12 @@
7.232 fun string_of_index pre i = pre ^ string_of_int i
7.233
7.234 fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
7.235 - let val s = string_of_index sort_prefix Tidx
7.236 - in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
7.237 + let
7.238 + val s = string_of_index sort_prefix Tidx
7.239 + val U = revert_typ T
7.240 + in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end
7.241
7.242 -fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
7.243 +fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ
7.244
7.245 fun fresh_typ T f cx =
7.246 (case lookup_typ cx T of
7.247 @@ -297,7 +276,7 @@
7.248 in (f, (Tidx, typs, dtyps, idx+1, terms')) end
7.249
7.250 fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
7.251 - (case Termtab.lookup terms t of
7.252 + (case Termtab.lookup terms (revert_types t) of
7.253 SOME (f, _) => (f, cx)
7.254 | NONE => new_fun func_prefix t ss cx)
7.255
7.256 @@ -335,15 +314,15 @@
7.257 in ((make_sign (header ts) context, us), make_recon ths context) end
7.258
7.259
7.260 -fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
7.261 +fun translate config ctxt comments =
7.262 let
7.263 + val {prefixes, is_fol, header, has_datatypes, serialize} = config
7.264 val {sort_prefix, func_prefix} = prefixes
7.265 - val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
7.266
7.267 fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
7.268 | transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
7.269 | transT (T as Type (n, Ts)) =
7.270 - (case builtin_typ ctxt T of
7.271 + (case B.builtin_typ ctxt T of
7.272 SOME n => pair n
7.273 | NONE => fresh_typ T (fn _ => fn cx =>
7.274 if not has_datatypes then new_typ sort_prefix true T cx
7.275 @@ -387,17 +366,14 @@
7.276 transT T ##>> trans t1 ##>> trans t2 #>>
7.277 (fn ((U, u1), u2) => SLet (U, u1, u2))
7.278 | (h as Const (c as (@{const_name distinct}, T)), ts) =>
7.279 - (case builtin_fun ctxt c ts of
7.280 + (case B.builtin_fun ctxt c ts of
7.281 SOME (n, ts) => fold_map trans ts #>> app n
7.282 | NONE => transs h T ts)
7.283 | (h as Const (c as (_, T)), ts) =>
7.284 - (case try HOLogic.dest_number t of
7.285 - SOME (T, i) =>
7.286 - (case builtin_num ctxt T i of
7.287 - SOME n => pair (SApp (n, []))
7.288 - | NONE => transs t T [])
7.289 + (case B.builtin_num ctxt t of
7.290 + SOME n => pair (SApp (n, []))
7.291 | NONE =>
7.292 - (case builtin_fun ctxt c ts of
7.293 + (case B.builtin_fun ctxt c ts of
7.294 SOME (n, ts') => fold_map trans ts' #>> app n
7.295 | NONE => transs h T ts))
7.296 | (h as Free (_, T), ts) => transs h T ts
7.297 @@ -414,7 +390,7 @@
7.298 fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
7.299 end
7.300 in
7.301 - (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
7.302 + (if is_fol then folify ctxt else relaxed) #>
7.303 with_context (header ctxt) trans #>> uncurry (serialize comments)
7.304 end
7.305
8.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 06 16:54:22 2010 +0100
8.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Dec 07 14:53:12 2010 +0100
8.3 @@ -6,34 +6,31 @@
8.4
8.5 signature SMTLIB_INTERFACE =
8.6 sig
8.7 - type builtins = {
8.8 - builtin_typ: typ -> string option,
8.9 - builtin_num: typ -> int -> string option,
8.10 - builtin_func: string * typ -> term list -> (string * term list) option,
8.11 - builtin_pred: string * typ -> term list -> (string * term list) option,
8.12 - is_builtin_pred: string -> typ -> bool }
8.13 - val add_builtins: builtins -> Context.generic -> Context.generic
8.14 - val add_logic: (term list -> string option) -> Context.generic ->
8.15 + val smtlibC: SMT_Config.class
8.16 + val add_logic: int * (term list -> string option) -> Context.generic ->
8.17 Context.generic
8.18 - val extra_norm: SMT_Normalize.extra_norm
8.19 + val setup: theory -> theory
8.20 val interface: SMT_Solver.interface
8.21 end
8.22
8.23 structure SMTLIB_Interface: SMTLIB_INTERFACE =
8.24 struct
8.25
8.26 +structure B = SMT_Builtin
8.27 structure N = SMT_Normalize
8.28 structure T = SMT_Translate
8.29
8.30 +val smtlibC = ["smtlib"]
8.31
8.32
8.33 -(** facts about uninterpreted constants **)
8.34 +
8.35 +(* facts about uninterpreted constants *)
8.36
8.37 infix 2 ??
8.38 fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
8.39
8.40
8.41 -(* pairs *)
8.42 +(** pairs **)
8.43
8.44 val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
8.45
8.46 @@ -43,7 +40,7 @@
8.47 val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
8.48
8.49
8.50 -(* function update *)
8.51 +(** function update **)
8.52
8.53 val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
8.54
8.55 @@ -53,7 +50,7 @@
8.56 val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
8.57
8.58
8.59 -(* abs/min/max *)
8.60 +(** abs/min/max **)
8.61
8.62 val exists_abs_min_max = Term.exists_subterm (fn
8.63 Const (@{const_name abs}, _) => true
8.64 @@ -86,7 +83,7 @@
8.65 else thm
8.66
8.67
8.68 -(* include additional facts *)
8.69 +(** include additional facts **)
8.70
8.71 fun extra_norm has_datatypes irules ctxt =
8.72 irules
8.73 @@ -97,121 +94,49 @@
8.74
8.75
8.76
8.77 -(** builtins **)
8.78 +(* builtins *)
8.79
8.80 -(* additional builtins *)
8.81 +local
8.82 + fun int_num _ i = SOME (string_of_int i)
8.83
8.84 -type builtins = {
8.85 - builtin_typ: typ -> string option,
8.86 - builtin_num: typ -> int -> string option,
8.87 - builtin_func: string * typ -> term list -> (string * term list) option,
8.88 - builtin_pred: string * typ -> term list -> (string * term list) option,
8.89 - is_builtin_pred: string -> typ -> bool }
8.90 + fun distinct _ _ [t] =
8.91 + (case try HOLogic.dest_list t of
8.92 + SOME (ts as _ :: _) => SOME ("distinct", ts)
8.93 + | _ => NONE)
8.94 + | distinct _ _ _ = NONE
8.95 +in
8.96
8.97 -fun chained _ [] = NONE
8.98 - | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
8.99 +val setup =
8.100 + B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
8.101 + fold (B.add_builtin_fun' smtlibC) [
8.102 + (@{const True}, "true"),
8.103 + (@{const False}, "false"),
8.104 + (* FIXME: we do not test if these constants are fully applied! *)
8.105 + (@{const Not}, "not"),
8.106 + (@{const HOL.conj}, "and"),
8.107 + (@{const HOL.disj}, "or"),
8.108 + (@{const HOL.implies}, "implies"),
8.109 + (@{const HOL.eq (bool)}, "iff"),
8.110 + (@{const HOL.eq ('a)}, "="),
8.111 + (@{const If (bool)}, "if_then_else"),
8.112 + (@{const If ('a)}, "ite"),
8.113 + (@{const less (int)}, "<"),
8.114 + (@{const less_eq (int)}, "<="),
8.115 + (@{const uminus (int)}, "~"),
8.116 + (@{const plus (int)}, "+"),
8.117 + (@{const minus (int)}, "-"),
8.118 + (@{const times (int)}, "*") ] #>
8.119 + B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
8.120
8.121 -fun chained' _ [] = false
8.122 - | chained' f (b :: bs) = f b orelse chained' f bs
8.123 +end
8.124
8.125 -fun chained_builtin_typ bs T =
8.126 - chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs
8.127
8.128 -fun chained_builtin_num bs T i =
8.129 - chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs
8.130
8.131 -fun chained_builtin_func bs c ts =
8.132 - chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs
8.133 +(* serialization *)
8.134
8.135 -fun chained_builtin_pred bs c ts =
8.136 - chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs
8.137 +(** header **)
8.138
8.139 -fun chained_is_builtin_pred bs n T =
8.140 - chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs
8.141 -
8.142 -fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
8.143 -
8.144 -structure Builtins = Generic_Data
8.145 -(
8.146 - type T = (int * builtins) list
8.147 - val empty = []
8.148 - val extend = I
8.149 - fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
8.150 -)
8.151 -
8.152 -fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
8.153 -
8.154 -fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
8.155 -
8.156 -
8.157 -(* basic builtins combined with additional builtins *)
8.158 -
8.159 -fun builtin_typ _ @{typ int} = SOME "Int"
8.160 - | builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T
8.161 -
8.162 -fun builtin_num _ @{typ int} i = SOME (string_of_int i)
8.163 - | builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i
8.164 -
8.165 -fun if_int_type T n =
8.166 - (case try Term.domain_type T of
8.167 - SOME @{typ int} => SOME n
8.168 - | _ => NONE)
8.169 -
8.170 -fun conn @{const_name True} = SOME "true"
8.171 - | conn @{const_name False} = SOME "false"
8.172 - | conn @{const_name Not} = SOME "not"
8.173 - | conn @{const_name HOL.conj} = SOME "and"
8.174 - | conn @{const_name HOL.disj} = SOME "or"
8.175 - | conn @{const_name HOL.implies} = SOME "implies"
8.176 - | conn @{const_name HOL.eq} = SOME "iff"
8.177 - | conn @{const_name If} = SOME "if_then_else"
8.178 - | conn _ = NONE
8.179 -
8.180 -fun distinct_pred (@{const_name distinct}, _) [t] =
8.181 - try HOLogic.dest_list t |> Option.map (pair "distinct")
8.182 - | distinct_pred _ _ = NONE
8.183 -
8.184 -fun pred @{const_name HOL.eq} _ = SOME "="
8.185 - | pred @{const_name term_eq} _ = SOME "="
8.186 - | pred @{const_name less} T = if_int_type T "<"
8.187 - | pred @{const_name less_eq} T = if_int_type T "<="
8.188 - | pred _ _ = NONE
8.189 -
8.190 -fun func @{const_name If} _ = SOME "ite"
8.191 - | func @{const_name uminus} T = if_int_type T "~"
8.192 - | func @{const_name plus} T = if_int_type T "+"
8.193 - | func @{const_name minus} T = if_int_type T "-"
8.194 - | func @{const_name times} T = if_int_type T "*"
8.195 - | func _ _ = NONE
8.196 -
8.197 -val is_propT = (fn @{typ prop} => true | _ => false)
8.198 -fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
8.199 -fun is_predT T = is_propT (Term.body_type T)
8.200 -
8.201 -fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
8.202 -fun is_builtin_pred ctxt (n, T) = is_predT T andalso
8.203 - (is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T)
8.204 -
8.205 -fun builtin_fun ctxt (c as (n, T)) ts =
8.206 - let
8.207 - val builtin_func' = chained_builtin_func (get_builtins ctxt)
8.208 - fun builtin_pred' c ts =
8.209 - (case distinct_pred c ts of
8.210 - SOME b => SOME b
8.211 - | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
8.212 - in
8.213 - if is_connT T then conn n |> Option.map (rpair ts)
8.214 - else if is_predT T then
8.215 - (case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts)
8.216 - else
8.217 - (case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts)
8.218 - end
8.219 -
8.220 -
8.221 -
8.222 -(** serialization **)
8.223 -
8.224 -(* header *)
8.225 +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
8.226
8.227 structure Logics = Generic_Data
8.228 (
8.229 @@ -221,13 +146,13 @@
8.230 fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
8.231 )
8.232
8.233 -fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
8.234 +fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
8.235
8.236 fun choose_logic ctxt ts =
8.237 let
8.238 fun choose [] = "AUFLIA"
8.239 - | choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls)
8.240 - in [":logic " ^ choose (rev (Logics.get (Context.Proof ctxt)))] end
8.241 + | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
8.242 + in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
8.243
8.244
8.245 (* serialization *)
8.246 @@ -294,21 +219,15 @@
8.247 (** interfaces **)
8.248
8.249 val interface = {
8.250 + class = smtlibC,
8.251 extra_norm = extra_norm,
8.252 translate = {
8.253 prefixes = {
8.254 sort_prefix = "S",
8.255 func_prefix = "f"},
8.256 header = choose_logic,
8.257 - strict = SOME {
8.258 - is_builtin_conn = is_builtin_conn,
8.259 - is_builtin_pred = is_builtin_pred,
8.260 - is_builtin_distinct = true},
8.261 - builtins = {
8.262 - builtin_typ = builtin_typ,
8.263 - builtin_num = builtin_num,
8.264 - builtin_fun = builtin_fun,
8.265 - has_datatypes = false},
8.266 + is_fol = true,
8.267 + has_datatypes = false,
8.268 serialize = serialize}}
8.269
8.270 end
9.1 --- a/src/HOL/Tools/SMT/z3_interface.ML Mon Dec 06 16:54:22 2010 +0100
9.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Dec 07 14:53:12 2010 +0100
9.3 @@ -6,8 +6,8 @@
9.4
9.5 signature Z3_INTERFACE =
9.6 sig
9.7 - type builtin_fun = string * typ -> term list -> (string * term list) option
9.8 - val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
9.9 + val smtlib_z3C: SMT_Config.class
9.10 + val setup: theory -> theory
9.11 val interface: SMT_Solver.interface
9.12
9.13 datatype sym = Sym of string * sym list
9.14 @@ -27,45 +27,17 @@
9.15 struct
9.16
9.17 structure U = SMT_Utils
9.18 +structure B = SMT_Builtin
9.19
9.20 +val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
9.21
9.22 -(** Z3-specific builtins **)
9.23
9.24 -type builtin_fun = string * typ -> term list -> (string * term list) option
9.25
9.26 -fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
9.27 -
9.28 -structure Builtins = Generic_Data
9.29 -(
9.30 - type T = (int * builtin_fun) list
9.31 - val empty = []
9.32 - val extend = I
9.33 - fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
9.34 -)
9.35 -
9.36 -fun add_builtin_funs b =
9.37 - Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
9.38 -
9.39 -fun get_builtin_funs ctxt c ts =
9.40 - let
9.41 - fun chained [] = NONE
9.42 - | chained (b :: bs) = (case b c ts of SOME x => SOME x | _ => chained bs)
9.43 - in chained (map snd (Builtins.get (Context.Proof ctxt))) end
9.44 -
9.45 -fun z3_builtin_fun builtin_fun ctxt c ts =
9.46 - (case builtin_fun ctxt c ts of
9.47 - SOME x => SOME x
9.48 - | _ => get_builtin_funs ctxt c ts)
9.49 -
9.50 -
9.51 -
9.52 -(** interface **)
9.53 +(* interface *)
9.54
9.55 local
9.56 - val {translate, ...} = SMTLIB_Interface.interface
9.57 - val {prefixes, strict, header, builtins, serialize} = translate
9.58 - val {is_builtin_pred, ...}= the strict
9.59 - val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
9.60 + val {translate, extra_norm, ...} = SMTLIB_Interface.interface
9.61 + val {prefixes, is_fol, header, serialize, ...} = translate
9.62
9.63 fun is_int_div_mod @{const div (int)} = true
9.64 | is_int_div_mod @{const mod (int)} = true
9.65 @@ -76,45 +48,33 @@
9.66 then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules
9.67 else irules
9.68
9.69 - fun extra_norm' has_datatypes =
9.70 - SMTLIB_Interface.extra_norm has_datatypes o add_div_mod
9.71 -
9.72 - fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
9.73 - | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
9.74 - | z3_builtin_fun' ctxt c ts = z3_builtin_fun builtin_fun ctxt c ts
9.75 -
9.76 - val as_propT = (fn @{typ bool} => @{typ prop} | T => T)
9.77 + fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod
9.78 in
9.79
9.80 -fun is_builtin_num ctxt (T, i) = is_some (builtin_num ctxt T i)
9.81 -
9.82 -fun is_builtin_fun ctxt (c as (n, T)) ts =
9.83 - is_some (z3_builtin_fun' ctxt c ts) orelse
9.84 - is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
9.85 +val setup =
9.86 + B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
9.87 + B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
9.88
9.89 val interface = {
9.90 + class = smtlib_z3C,
9.91 extra_norm = extra_norm',
9.92 translate = {
9.93 prefixes = prefixes,
9.94 - strict = strict,
9.95 + is_fol = is_fol,
9.96 header = header,
9.97 - builtins = {
9.98 - builtin_typ = builtin_typ,
9.99 - builtin_num = builtin_num,
9.100 - builtin_fun = z3_builtin_fun',
9.101 - has_datatypes = true},
9.102 + has_datatypes = true,
9.103 serialize = serialize}}
9.104
9.105 end
9.106
9.107
9.108
9.109 -(** constructors **)
9.110 +(* constructors *)
9.111
9.112 datatype sym = Sym of string * sym list
9.113
9.114
9.115 -(* additional constructors *)
9.116 +(** additional constructors **)
9.117
9.118 type mk_builtins = {
9.119 mk_builtin_typ: sym -> typ option,
9.120 @@ -135,6 +95,8 @@
9.121 let val thy = ProofContext.theory_of ctxt
9.122 in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
9.123
9.124 +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
9.125 +
9.126 structure Mk_Builtins = Generic_Data
9.127 (
9.128 type T = (int * mk_builtins) list
9.129 @@ -149,7 +111,7 @@
9.130 fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
9.131
9.132
9.133 -(* basic and additional constructors *)
9.134 +(** basic and additional constructors **)
9.135
9.136 fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
9.137 | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
9.138 @@ -241,14 +203,13 @@
9.139
9.140
9.141
9.142 -(** abstraction **)
9.143 +(* abstraction *)
9.144
9.145 fun is_builtin_theory_term ctxt t =
9.146 - (case try HOLogic.dest_number t of
9.147 - SOME n => is_builtin_num ctxt n
9.148 - | NONE =>
9.149 - (case Term.strip_comb t of
9.150 - (Const c, ts) => is_builtin_fun ctxt c ts
9.151 - | _ => false))
9.152 + if B.is_builtin_num ctxt t then true
9.153 + else
9.154 + (case Term.strip_comb t of
9.155 + (Const c, ts) => B.is_builtin_fun ctxt c ts
9.156 + | _ => false)
9.157
9.158 end
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 16:54:22 2010 +0100
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Dec 07 14:53:12 2010 +0100
10.3 @@ -135,7 +135,7 @@
10.4 @{const_name HOL.eq}]
10.5
10.6 fun is_built_in_const_for_prover ctxt name (s, T) =
10.7 - if is_smt_prover ctxt name then SMT_Builtin.is_builtin ctxt (s, T)
10.8 + if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) [] (*FIXME*)
10.9 else member (op =) atp_irrelevant_consts s
10.10
10.11 (* FUDGE *)