centralized handling of built-in types and constants;
also store types and constants which are rewritten during preprocessing;
interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols);
removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
--- a/src/HOL/SMT.thy Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/SMT.thy Tue Dec 07 14:53:12 2010 +0100
@@ -105,16 +105,18 @@
subsection {* First-order logic *}
text {*
-Some SMT solvers require a strict separation between formulas and
-terms. When translating higher-order into first-order problems,
-all uninterpreted constants (those not builtin in the target solver)
+Some SMT solvers only accept problems in first-order logic, i.e.,
+where formulas and terms are syntactically separated. When
+translating higher-order into first-order problems, all
+uninterpreted constants (those not built-in in the target solver)
are treated as function symbols in the first-order sense. Their
-occurrences as head symbols in atoms (i.e., as predicate symbols) is
-turned into terms by equating such atoms with @{term True} using the
-following term-level equation symbol.
+occurrences as head symbols in atoms (i.e., as predicate symbols) are
+turned into terms by equating such atoms with @{term True}.
+Whenever the boolean type occurs in first-order terms, it is replaced
+by the following type.
*}
-definition term_eq :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "term_eq x y = (x = y)"
+typedecl term_bool
@@ -159,7 +161,10 @@
setup {*
SMT_Config.setup #>
+ SMT_Normalize.setup #>
SMT_Solver.setup #>
+ SMTLIB_Interface.setup #>
+ Z3_Interface.setup #>
Z3_Proof_Reconstruction.setup #>
SMT_Setup_Solvers.setup
*}
@@ -354,9 +359,10 @@
+hide_type term_bool
hide_type (open) pattern
-hide_const Pattern term_eq
-hide_const (open) trigger pat nopat weight fun_app z3div z3mod
+hide_const Pattern fun_app
+hide_const (open) trigger pat nopat weight z3div z3mod
--- a/src/HOL/Tools/SMT/smt_builtin.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML Tue Dec 07 14:53:12 2010 +0100
@@ -1,116 +1,226 @@
(* Title: HOL/Tools/SMT/smt_builtin.ML
Author: Sascha Boehme, TU Muenchen
-Crafted collection of SMT built-in symbols.
-
-FIXME: This list is currently not automatically kept synchronized with the
-remaining implementation.
+Tables of types and terms directly supported by SMT solvers.
*)
signature SMT_BUILTIN =
sig
- val is_builtin: Proof.context -> string * typ -> bool
- val is_partially_builtin: Proof.context -> string * typ -> bool
+ (*built-in types*)
+ val add_builtin_typ: SMT_Config.class ->
+ typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
+ theory
+ val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
+ val builtin_typ: Proof.context -> typ -> string option
+ val is_builtin_typ: Proof.context -> typ -> bool
+ val is_builtin_typ_ext: Proof.context -> typ -> bool
+
+ (*built-in numbers*)
+ val builtin_num: Proof.context -> term -> string option
+ val is_builtin_num: Proof.context -> term -> bool
+ val is_builtin_num_ext: Proof.context -> term -> bool
+
+ (*built-in functions*)
+ type 'a bfun = Proof.context -> typ -> term list -> 'a
+ val add_builtin_fun: SMT_Config.class ->
+ (string * typ) * (string * term list) option bfun -> theory -> theory
+ val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
+ val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
+ val add_builtin_fun_ext': string * typ -> theory -> theory
+ val add_builtin_fun_ext'': string -> theory -> theory
+ val builtin_fun: Proof.context -> string * typ -> term list ->
+ (string * term list) option
+ val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
+ val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
+ val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
+ val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
end
structure SMT_Builtin: SMT_BUILTIN =
struct
-fun is_arithT T =
- (case T of
- @{typ int} => true
- | @{typ nat} => true
- | Type ("RealDef.real", []) => true
- | _ => false)
+structure C = SMT_Config
+
+
+(* built-in tables *)
+
+datatype ('a, 'b) kind = Ext of 'a | Int of 'b
+
+type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list
-fun is_arithT_dom (Type (@{type_name fun}, [T, _])) = is_arithT T
- | is_arithT_dom _ = false
-fun is_arithT_ran (Type (@{type_name fun}, [_, T])) = is_arithT T
- | is_arithT_ran _ = false
+fun empty_ttab () = []
-val builtins = Symtab.make [
-
- (* Pure constants *)
- (@{const_name all}, K true),
- (@{const_name "=="}, K true),
- (@{const_name "==>"}, K true),
- (@{const_name Trueprop}, K true),
+fun typ_ord ((T, _), (U, _)) =
+ let
+ fun tord (TVar _, Type _) = GREATER
+ | tord (Type _, TVar _) = LESS
+ | tord (Type (n, Ts), Type (m, Us)) =
+ if n = m then list_ord tord (Ts, Us)
+ else Term_Ord.typ_ord (T, U)
+ | tord TU = Term_Ord.typ_ord TU
+ in tord (T, U) end
- (* logical constants *)
- (@{const_name All}, K true),
- (@{const_name Ex}, K true),
- (@{const_name Ball}, K true),
- (@{const_name Bex}, K true),
- (@{const_name Ex1}, K true),
- (@{const_name True}, K true),
- (@{const_name False}, K true),
- (@{const_name Not}, K true),
- (@{const_name HOL.conj}, K true),
- (@{const_name HOL.disj}, K true),
- (@{const_name HOL.implies}, K true),
+fun insert_ttab cs T f =
+ AList.map_default (op =) (cs, [])
+ (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
+
+fun merge_ttab ttabp =
+ AList.join (op =) (K (uncurry (Ord_List.union typ_ord) o swap)) ttabp
- (* term abbreviations *)
- (@{const_name If}, K true),
- (@{const_name bool.bool_case}, K true),
- (@{const_name Let}, K true),
- (* (@{const_name distinct}, K true), -- not a real builtin, only when
- applied to an explicit list *)
+fun lookup_ttab ctxt ttab T =
+ let
+ val cs = C.solver_class_of ctxt
+ fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
+
+ fun matching (cs', Txs) =
+ if is_prefix (op =) cs' cs then find_first match Txs
+ else NONE
+ in get_first matching ttab end
+
+type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
+
+fun empty_btab () = Symtab.empty
- (* technicalities *)
- (@{const_name SMT.pat}, K true),
- (@{const_name SMT.nopat}, K true),
- (@{const_name SMT.trigger}, K true),
- (@{const_name SMT.weight}, K true),
- (@{const_name SMT.fun_app}, K true),
- (@{const_name SMT.z3div}, K true),
- (@{const_name SMT.z3mod}, K true),
+fun insert_btab cs n T f =
+ Symtab.map_default (n, []) (insert_ttab cs T f)
+
+fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
- (* equality *)
- (@{const_name HOL.eq}, K true),
+fun lookup_btab ctxt btab (n, T) =
+ (case Symtab.lookup btab n of
+ NONE => NONE
+ | SOME ttab => lookup_ttab ctxt ttab T)
- (* numerals *)
- (@{const_name zero_class.zero}, is_arithT),
- (@{const_name one_class.one}, is_arithT),
- (@{const_name Int.Pls}, K true),
- (@{const_name Int.Min}, K true),
- (@{const_name Int.Bit0}, K true),
- (@{const_name Int.Bit1}, K true),
- (@{const_name number_of}, is_arithT_ran),
+
+(* built-in types *)
- (* arithmetic *)
- (@{const_name nat}, K true),
- (@{const_name of_nat}, K true),
- (@{const_name Suc}, K true),
- (@{const_name plus}, is_arithT_dom),
- (@{const_name uminus}, is_arithT_dom),
- (@{const_name minus}, is_arithT_dom),
- (@{const_name abs}, is_arithT_dom),
- (@{const_name min}, is_arithT_dom),
- (@{const_name max}, is_arithT_dom),
- (@{const_name less}, is_arithT_dom),
- (@{const_name less_eq}, is_arithT_dom),
-
- (* pairs *)
- (@{const_name fst}, K true),
- (@{const_name snd}, K true),
- (@{const_name Pair}, K true)
+structure Builtin_Types = Theory_Data
+(
+ type T =
+ (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
+ val empty = empty_ttab ()
+ val extend = I
+ val merge = merge_ttab
+)
+
+fun add_builtin_typ cs (T, f, g) =
+ Builtin_Types.map (insert_ttab cs T (Int (f, g)))
+
+fun add_builtin_typ_ext (T, f) =
+ Builtin_Types.map (insert_ttab C.basicC T (Ext f))
- ]
+fun lookup_builtin_typ ctxt =
+ lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
-val all_builtins =
- builtins
- |> Symtab.update (@{const_name times}, is_arithT_dom)
- |> Symtab.update (@{const_name div_class.div}, is_arithT_dom)
- |> Symtab.update (@{const_name div_class.mod}, is_arithT_dom)
- |> Symtab.update ("Rings.inverse_class.divide", is_arithT_dom)
+fun builtin_typ ctxt T =
+ (case lookup_builtin_typ ctxt T of
+ SOME (_, Int (f, _)) => f T
+ | _ => NONE)
-fun lookup_builtin bs (name, T) =
- (case Symtab.lookup bs name of
- SOME proper_type => proper_type T
+fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
+
+fun is_builtin_typ_ext ctxt T =
+ (case lookup_builtin_typ ctxt T of
+ SOME (_, Int (f, _)) => is_some (f T)
+ | SOME (_, Ext f) => f T
| NONE => false)
-fun is_builtin _ = lookup_builtin builtins
+
+(* built-in numbers *)
+
+fun builtin_num ctxt t =
+ (case try HOLogic.dest_number t of
+ NONE => NONE
+ | SOME (T, i) =>
+ (case lookup_builtin_typ ctxt T of
+ SOME (_, Int (_, g)) => g T i
+ | _ => NONE))
+
+val is_builtin_num = is_some oo builtin_num
+
+fun is_builtin_num_ext ctxt t =
+ (case try HOLogic.dest_number t of
+ NONE => false
+ | SOME (T, _) => is_builtin_typ_ext ctxt T)
+
+
+(* built-in functions *)
+
+type 'a bfun = Proof.context -> typ -> term list -> 'a
+
+fun true3 _ _ _ = true
+
+fun raw_add_builtin_fun_ext thy cs n =
+ insert_btab cs n (Sign.the_const_type thy n) (Ext true3)
+
+val basic_builtin_fun_names = [
+ @{const_name SMT.pat}, @{const_name SMT.nopat},
+ @{const_name SMT.trigger}, @{const_name SMT.weight}]
+
+fun basic_builtin_funcs () =
+ empty_btab ()
+ |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
+ (* FIXME: SMT_Normalize should check that they are properly used *)
+
+structure Builtin_Funcs = Theory_Data
+(
+ type T = (bool bfun, (string * term list) option bfun) btab
+ val empty = basic_builtin_funcs ()
+ val extend = I
+ val merge = merge_btab
+)
+
+fun add_builtin_fun cs ((n, T), f) =
+ Builtin_Funcs.map (insert_btab cs n T (Int f))
-fun is_partially_builtin _ = lookup_builtin all_builtins
+fun add_builtin_fun' cs (t, n) =
+ add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
+
+fun add_builtin_fun_ext ((n, T), f) =
+ Builtin_Funcs.map (insert_btab C.basicC n T (Ext f))
+
+fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
+
+fun add_builtin_fun_ext'' n thy =
+ add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
+
+fun lookup_builtin_fun ctxt =
+ lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
+
+fun builtin_fun ctxt (c as (_, T)) ts =
+ (case lookup_builtin_fun ctxt c of
+ SOME (_, Int f) => f ctxt T ts
+ | _ => NONE)
+
+fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
+
+fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
+ (case lookup_builtin_fun ctxt c of
+ SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
+ | _ => false)
+
+fun is_pred_type T = Term.body_type T = @{typ bool}
+fun is_conn_type T =
+ forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
+
+fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
+fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
+
+fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
+ (case lookup_builtin_fun ctxt c of
+ SOME (_, Int f) => is_some (f ctxt T ts)
+ | SOME (_, Ext f) => f ctxt T ts
+ | NONE => false)
+
+(* FIXME: move this information to the interfaces *)
+val only_partially_supported = [
+ @{const_name times},
+ @{const_name div_class.div},
+ @{const_name div_class.mod},
+ @{const_name inverse_class.divide} ]
+
+fun is_builtin_ext ctxt (c as (n, _)) ts =
+ if member (op =) only_partially_supported n then false
+ else is_builtin_fun_ext ctxt c ts
end
--- a/src/HOL/Tools/SMT/smt_config.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Dec 07 14:53:12 2010 +0100
@@ -6,11 +6,16 @@
signature SMT_CONFIG =
sig
+ (*class*)
+ type class = string list
+ val basicC: class
+
(*solver*)
- val add_solver: string -> Context.generic -> Context.generic
+ val add_solver: string * class -> Context.generic -> Context.generic
val set_solver_options: string * string -> Context.generic -> Context.generic
val select_solver: string -> Context.generic -> Context.generic
val solver_of: Proof.context -> string
+ val solver_class_of: Proof.context -> class
val solver_options_of: Proof.context -> string list
(*options*)
@@ -46,11 +51,18 @@
structure SMT_Config: SMT_CONFIG =
struct
+(* class *)
+
+type class = string list
+
+val basicC = []
+
+
(* solver *)
structure Solvers = Generic_Data
(
- type T = string list Symtab.table * string option
+ type T = (class * string list) Symtab.table * string option
val empty = (Symtab.empty, NONE)
val extend = I
fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
@@ -58,14 +70,14 @@
fun set_solver_options (name, options) =
let val opts = String.tokens (Symbol.is_ascii_blank o str) options
- in Solvers.map (apfst (Symtab.map_entry name (K opts))) end
+ in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
-fun add_solver name context =
+fun add_solver (name, class) context =
if Symtab.defined (fst (Solvers.get context)) name then
error ("Solver already registered: " ^ quote name)
else
context
- |> Solvers.map (apfst (Symtab.update (name, [])))
+ |> Solvers.map (apfst (Symtab.update (name, (class, []))))
|> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options"))
(Scan.lift (Parse.$$$ "=" |-- Args.name) >>
(Thm.declaration_attribute o K o set_solver_options o pair name))
@@ -76,18 +88,23 @@
Solvers.map (apsnd (K (SOME name))) context
else error ("Trying to select unknown solver: " ^ quote name)
-val lookup_solver = snd o Solvers.get o Context.Proof
+fun no_solver_err () = error "No SMT solver selected"
fun solver_of ctxt =
- (case lookup_solver ctxt of
- SOME name => name
- | NONE => error "No SMT solver selected")
+ (case Solvers.get (Context.Proof ctxt) of
+ (_, SOME name) => name
+ | (_, NONE) => no_solver_err ())
+
+fun solver_class_of ctxt =
+ (case Solvers.get (Context.Proof ctxt) of
+ (solvers, SOME name) => fst (the (Symtab.lookup solvers name))
+ | (_, NONE) => no_solver_err())
fun solver_options_of ctxt =
- (case lookup_solver ctxt of
- NONE => []
- | SOME name =>
- Symtab.lookup_list (fst (Solvers.get (Context.Proof ctxt))) name)
+ (case Solvers.get (Context.Proof ctxt) of
+ (solvers, SOME name) =>
+ (case Symtab.lookup solvers name of SOME (_, opts) => opts | NONE => [])
+ | (_, NONE) => [])
val setup_solver =
Attrib.setup @{binding smt_solver}
--- a/src/HOL/Tools/SMT/smt_normalize.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Tue Dec 07 14:53:12 2010 +0100
@@ -23,12 +23,14 @@
(int * thm) list * Proof.context
val atomize_conv: Proof.context -> conv
val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val setup: theory -> theory
end
structure SMT_Normalize: SMT_NORMALIZE =
struct
structure U = SMT_Utils
+structure B = SMT_Builtin
infix 2 ??
fun (test ?? f) x = if test x then f x else x
@@ -95,6 +97,9 @@
fun rewrite_bool_cases ctxt =
map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
+
+val setup_bool_case = B.add_builtin_fun_ext'' @{const_name "bool.bool_case"}
+
end
@@ -203,10 +208,20 @@
val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
val uses_nat_int = Term.exists_subterm (member (op aconv)
[@{const of_nat (int)}, @{const nat}])
+
+ val nat_ops = [
+ @{const less (nat)}, @{const less_eq (nat)},
+ @{const Suc}, @{const plus (nat)}, @{const minus (nat)},
+ @{const times (nat)}, @{const div (nat)}, @{const mod (nat)}]
+ val nat_ops' = @{const of_nat (int)} :: @{const nat} :: nat_ops
in
fun nat_as_int ctxt =
map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
+
+val setup_nat_as_int =
+ B.add_builtin_typ_ext (@{typ nat}, K true) #>
+ fold (B.add_builtin_fun_ext' o Term.dest_Const) nat_ops'
end
@@ -263,7 +278,7 @@
| _ =>
(case Term.strip_comb (Thm.term_of ct) of
(Const (c as (_, T)), ts) =>
- if SMT_Builtin.is_partially_builtin ctxt c
+ if SMT_Builtin.is_builtin_fun ctxt c ts
then eta_args_conv norm_conv
(length (Term.binder_types T) - length ts)
else args_conv o norm_conv
@@ -294,7 +309,7 @@
| _ =>
(case Term.strip_comb t of
(Const (c as (_, T)), ts) =>
- if SMT_Builtin.is_builtin ctxt c
+ if SMT_Builtin.is_builtin_fun ctxt c ts
then length (Term.binder_types T) = length ts andalso
forall (is_normed ctxt) ts
else forall (is_normed ctxt) ts
@@ -302,6 +317,11 @@
in
fun norm_binder_conv ctxt =
U.if_conv (is_normed ctxt) Conv.all_conv (norm_conv ctxt)
+
+val setup_unfolded_quants =
+ fold B.add_builtin_fun_ext'' [@{const_name Ball}, @{const_name Bex},
+ @{const_name Ex1}]
+
end
fun norm_def ctxt thm =
@@ -325,6 +345,10 @@
Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
+val setup_atomize =
+ fold B.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
+ @{const_name all}, @{const_name Trueprop}]
+
fun normalize_rule ctxt =
Conv.fconv_rule (
(* reduce lambda abstractions, except at known binders: *)
@@ -554,4 +578,14 @@
|-> (if with_datatypes then datatype_selectors else pair)
end
+
+
+(* setup *)
+
+val setup =
+ setup_bool_case #>
+ setup_nat_as_int #>
+ setup_unfolded_quants #>
+ setup_atomize
+
end
--- a/src/HOL/Tools/SMT/smt_real.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML Tue Dec 07 14:53:12 2010 +0100
@@ -12,6 +12,8 @@
structure SMT_Real: SMT_REAL =
struct
+structure B = SMT_Builtin
+
(* SMT-LIB logic *)
@@ -21,58 +23,28 @@
else NONE
-
-(* SMT-LIB builtins *)
+(* SMT-LIB and Z3 built-ins *)
local
- fun smtlib_builtin_typ @{typ real} = SOME "Real"
- | smtlib_builtin_typ _ = NONE
-
- fun smtlib_builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
- | smtlib_builtin_num _ _ = NONE
+ val smtlibC = SMTLIB_Interface.smtlibC
- fun smtlib_builtin_func @{const_name uminus} ts = SOME ("~", ts)
- | smtlib_builtin_func @{const_name plus} ts = SOME ("+", ts)
- | smtlib_builtin_func @{const_name minus} ts = SOME ("-", ts)
- | smtlib_builtin_func @{const_name times} ts = SOME ("*", ts)
- | smtlib_builtin_func _ _ = NONE
-
- fun smtlib_builtin_pred @{const_name less} = SOME "<"
- | smtlib_builtin_pred @{const_name less_eq} = SOME "<="
- | smtlib_builtin_pred _ = NONE
-
- fun real_fun T y f x =
- (case try Term.domain_type T of
- SOME @{typ real} => f x
- | _ => y)
+ fun real_num _ i = SOME (string_of_int i ^ ".0")
in
-val smtlib_builtins = {
- builtin_typ = smtlib_builtin_typ,
- builtin_num = smtlib_builtin_num,
- builtin_func = (fn (n, T) => real_fun T NONE (smtlib_builtin_func n)),
- builtin_pred = (fn (n, T) => fn ts =>
- real_fun T NONE smtlib_builtin_pred n |> Option.map (rpair ts)),
- is_builtin_pred = (fn n => fn T =>
- real_fun T false (is_some o smtlib_builtin_pred) n) }
+val setup_builtins =
+ B.add_builtin_typ smtlibC (@{typ real}, K (SOME "Real"), real_num) #>
+ fold (B.add_builtin_fun' smtlibC) [
+ (@{const uminus (real)}, "~"),
+ (@{const plus (real)}, "+"),
+ (@{const minus (real)}, "-"),
+ (@{const times (real)}, "*"),
+ (@{const less (real)}, "<"),
+ (@{const less_eq (real)}, "<=") ] #>
+ B.add_builtin_fun' Z3_Interface.smtlib_z3C (@{const divide (real)}, "/")
end
-
-(* Z3 builtins *)
-
-local
- fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
- | z3_builtin_fun _ _ = NONE
-in
-
-val z3_builtins = (fn c => fn ts => z3_builtin_fun (Const c) ts)
-
-end
-
-
-
(* Z3 constructors *)
local
@@ -117,7 +89,6 @@
end
-
(* Z3 proof reconstruction *)
val real_rules = @{lemma
@@ -132,14 +103,12 @@
"(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
-
(* setup *)
val setup =
+ setup_builtins #>
Context.theory_map (
- SMTLIB_Interface.add_logic smtlib_logic #>
- SMTLIB_Interface.add_builtins smtlib_builtins #>
- Z3_Interface.add_builtin_funs z3_builtins #>
+ SMTLIB_Interface.add_logic (10, smtlib_logic) #>
Z3_Interface.add_mk_builtins z3_mk_builtins #>
fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
Z3_Proof_Tools.add_simproc real_linarith_proc)
--- a/src/HOL/Tools/SMT/smt_solver.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Tue Dec 07 14:53:12 2010 +0100
@@ -8,6 +8,7 @@
sig
(*configuration*)
type interface = {
+ class: SMT_Config.class,
extra_norm: SMT_Normalize.extra_norm,
translate: SMT_Translate.config }
datatype outcome = Unsat | Sat | Unknown
@@ -57,6 +58,7 @@
(* configuration *)
type interface = {
+ class: SMT_Config.class,
extra_norm: SMT_Normalize.extra_norm,
translate: SMT_Translate.config }
@@ -195,13 +197,10 @@
fun set_has_datatypes with_datatypes translate =
let
- val {prefixes, header, strict, builtins, serialize} = translate
- val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
+ val {prefixes, header, is_fol, has_datatypes, serialize} = translate
val with_datatypes' = has_datatypes andalso with_datatypes
- val builtins' = {builtin_typ=builtin_typ, builtin_num=builtin_num,
- builtin_fun=builtin_fun, has_datatypes=with_datatypes}
- val translate' = {prefixes=prefixes, header=header, strict=strict,
- builtins=builtins', serialize=serialize}
+ val translate' = {prefixes=prefixes, header=header, is_fol=is_fol,
+ has_datatypes=with_datatypes', serialize=serialize}
in (with_datatypes', translate') end
fun trace_assumptions ctxt irules idxs =
@@ -219,7 +218,7 @@
fun gen_solver name info rm ctxt irules =
let
val {env_var, is_remote, options, interface, reconstruct, ...} = info
- val {extra_norm, translate} = interface
+ val {extra_norm, translate, ...} = interface
val (with_datatypes, translate') =
set_has_datatypes (Config.get ctxt C.datatypes) translate
val cmd = (rm, env_var, is_remote, name)
@@ -284,6 +283,7 @@
let
val {name, env_var, is_remote, options, interface, outcome, cex_parser,
reconstruct, default_max_relevant} = cfg
+ val {class, ...} = interface
fun core_oracle () = cfalse
@@ -294,7 +294,7 @@
in
Thm.add_oracle (Binding.name name, core_oracle) #-> (fn (_, ocl) =>
Context.theory_map (Solvers.map (Symtab.update_new (name, solver ocl)))) #>
- Context.theory_map (C.add_solver name)
+ Context.theory_map (C.add_solver (name, class))
end
end
--- a/src/HOL/Tools/SMT/smt_translate.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Dec 07 14:53:12 2010 +0100
@@ -17,17 +17,6 @@
(* configuration options *)
type prefixes = {sort_prefix: string, func_prefix: string}
- type header = Proof.context -> term list -> string list
- type strict = {
- is_builtin_conn: string * typ -> bool,
- is_builtin_pred: Proof.context -> string * typ -> bool,
- is_builtin_distinct: bool}
- type builtins = {
- builtin_typ: Proof.context -> typ -> string option,
- builtin_num: Proof.context -> typ -> int -> string option,
- builtin_fun: Proof.context -> string * typ -> term list ->
- (string * term list) option,
- has_datatypes: bool }
type sign = {
header: string list,
sorts: string list,
@@ -35,9 +24,9 @@
funcs: (string * (string list * string)) list }
type config = {
prefixes: prefixes,
- header: header,
- strict: strict option,
- builtins: builtins,
+ header: Proof.context -> term list -> string list,
+ is_fol: bool,
+ has_datatypes: bool,
serialize: string list -> sign -> sterm list -> string }
type recon = {
typs: typ Symtab.table,
@@ -53,6 +42,7 @@
struct
structure U = SMT_Utils
+structure B = SMT_Builtin
(* intermediate term structure *)
@@ -73,20 +63,6 @@
type prefixes = {sort_prefix: string, func_prefix: string}
-type header = Proof.context -> term list -> string list
-
-type strict = {
- is_builtin_conn: string * typ -> bool,
- is_builtin_pred: Proof.context -> string * typ -> bool,
- is_builtin_distinct: bool}
-
-type builtins = {
- builtin_typ: Proof.context -> typ -> string option,
- builtin_num: Proof.context -> typ -> int -> string option,
- builtin_fun: Proof.context -> string * typ -> term list ->
- (string * term list) option,
- has_datatypes: bool }
-
type sign = {
header: string list,
sorts: string list,
@@ -95,9 +71,9 @@
type config = {
prefixes: prefixes,
- header: header,
- strict: strict option,
- builtins: builtins,
+ header: Proof.context -> term list -> string list,
+ is_fol: bool,
+ has_datatypes: bool,
serialize: string list -> sign -> sterm list -> string }
type recon = {
@@ -152,13 +128,20 @@
-(* enforce a strict separation between formulas and terms *)
+(* map HOL formulas to FOL formulas (i.e., separate formulas froms terms) *)
-val term_eq_rewr = @{lemma "term_eq x y == x = y" by (simp add: term_eq_def)}
+val tboolT = @{typ SMT.term_bool}
+val term_true = Const (@{const_name True}, tboolT)
+val term_false = Const (@{const_name False}, tboolT)
-val term_bool = @{lemma "~(term_eq True False)" by (simp add: term_eq_def)}
-val term_bool' = Simplifier.rewrite_rule [term_eq_rewr] term_bool
-
+val term_bool = @{lemma "True ~= False" by simp}
+val term_bool_prop =
+ let
+ fun replace @{const HOL.eq (bool)} = @{const HOL.eq (SMT.term_bool)}
+ | replace @{const True} = term_true
+ | replace @{const False} = term_false
+ | replace t = t
+ in Term.map_aterms replace (prop_of term_bool) end
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
Const (@{const_name Let}, _) => true
@@ -171,63 +154,57 @@
@{lemma "P = True == P" by (rule eq_reflection) simp},
@{lemma "if P then True else False == P" by (rule eq_reflection) simp}]
-fun rewrite ctxt = Simplifier.full_rewrite
- (Simplifier.context ctxt empty_ss addsimps rewrite_rules)
+fun rewrite ctxt ct =
+ Conv.top_sweep_conv (fn ctxt' =>
+ Conv.rewrs_conv rewrite_rules then_conv rewrite ctxt') ctxt ct
fun normalize ctxt thm =
if needs_rewrite thm then Conv.fconv_rule (rewrite ctxt) thm else thm
-val unfold_rules = term_eq_rewr :: rewrite_rules
-
+fun revert_typ @{typ SMT.term_bool} = @{typ bool}
+ | revert_typ (Type (n, Ts)) = Type (n, map revert_typ Ts)
+ | revert_typ T = T
-val revert_types =
- let
- fun revert @{typ prop} = @{typ bool}
- | revert (Type (n, Ts)) = Type (n, map revert Ts)
- | revert T = T
- in Term.map_types revert end
+val revert_types = Term.map_types revert_typ
-
-fun strictify {is_builtin_conn, is_builtin_pred, is_builtin_distinct} ctxt =
+fun folify ctxt =
let
- fun is_builtin_conn' (@{const_name True}, _) = false
- | is_builtin_conn' (@{const_name False}, _) = false
- | is_builtin_conn' c = is_builtin_conn c
+ fun is_builtin_conn (@{const_name True}, _) _ = false
+ | is_builtin_conn (@{const_name False}, _) _ = false
+ | is_builtin_conn c ts = B.is_builtin_conn ctxt c ts
- fun is_builtin_pred' _ (@{const_name distinct}, _) [t] =
- is_builtin_distinct andalso can HOLogic.dest_list t
- | is_builtin_pred' ctxt c _ = is_builtin_pred ctxt c
+ fun as_term t = @{const HOL.eq (SMT.term_bool)} $ t $ term_true
- val propT = @{typ prop} and boolT = @{typ bool}
- val as_propT = (fn @{typ bool} => propT | T => T)
+ fun as_tbool @{typ bool} = tboolT
+ | as_tbool (Type (n, Ts)) = Type (n, map as_tbool Ts)
+ | as_tbool T = T
fun mapTs f g = Term.strip_type #> (fn (Ts, T) => map f Ts ---> g T)
- fun conn (n, T) = (n, mapTs as_propT as_propT T)
- fun pred (n, T) = (n, mapTs I as_propT T)
+ fun predT T = mapTs as_tbool I T
+ fun funcT T = mapTs as_tbool as_tbool T
+ fun func (n, T) = Const (n, funcT T)
- val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
- fun as_term t = Const term_eq $ t $ @{const True}
-
- val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
- fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
+ fun map_ifT T = T |> Term.dest_funT ||> funcT |> (op -->)
+ val if_term = @{const If (bool)} |> Term.dest_Const ||> map_ifT |> Const
+ fun wrap_in_if t = if_term $ t $ term_true $ term_false
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
fun in_term t =
(case Term.strip_comb t of
- (c as Const (@{const_name If}, _), [t1, t2, t3]) =>
- c $ in_form t1 $ in_term t2 $ in_term t3
- | (h as Const c, ts) =>
- if is_builtin_conn' (conn c) orelse is_builtin_pred' ctxt (pred c) ts
+ (Const (c as @{const_name If}, T), [t1, t2, t3]) =>
+ Const (c, map_ifT T) $ in_form t1 $ in_term t2 $ in_term t3
+ | (Const c, ts) =>
+ if is_builtin_conn c ts orelse B.is_builtin_pred ctxt c ts
then wrap_in_if (in_form t)
- else Term.list_comb (h, map in_term ts)
- | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
+ else Term.list_comb (func c, map in_term ts)
+ | (Free (n, T), ts) => Term.list_comb (Free (n, funcT T), map in_term ts)
| _ => t)
and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
| in_weight t = in_form t
- and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
- | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
+ and in_pat (Const (c as (@{const_name pat}, _)) $ t) = func c $ in_term t
+ | in_pat (Const (c as (@{const_name nopat}, _)) $ t) = func c $ in_term t
| in_pat t = raise TERM ("in_pat", [t])
and in_pats ps =
@@ -239,23 +216,23 @@
and in_form t =
(case Term.strip_comb t of
(q as Const (qn, _), [Abs (n, T, t')]) =>
- if is_some (quantifier qn) then q $ Abs (n, T, in_trig t')
+ if is_some (quantifier qn) then q $ Abs (n, as_tbool T, in_trig t')
else as_term (in_term t)
- | (Const (c as (@{const_name distinct}, T)), [t']) =>
- if is_builtin_distinct andalso can HOLogic.dest_list t' then
- Const (pred c) $ in_list T in_term t'
+ | (Const (c as (n as @{const_name distinct}, T)), [t']) =>
+ if B.is_builtin_fun ctxt c [t'] then
+ Const (n, predT T) $ in_list T in_term t'
else as_term (in_term t)
- | (Const c, ts) =>
- if is_builtin_conn (conn c)
- then Term.list_comb (Const (conn c), map in_form ts)
- else if is_builtin_pred ctxt (pred c)
- then Term.list_comb (Const (pred c), map in_term ts)
+ | (Const (c as (n, T)), ts) =>
+ if B.is_builtin_conn ctxt c ts
+ then Term.list_comb (Const c, map in_form ts)
+ else if B.is_builtin_pred ctxt c ts
+ then Term.list_comb (Const (n, predT T), map in_term ts)
else as_term (in_term t)
| _ => as_term (in_term t))
in
map (apsnd (normalize ctxt)) #> (fn irules =>
- ((unfold_rules, (~1, term_bool') :: irules),
- map (in_form o prop_of o snd) ((~1, term_bool) :: irules)))
+ ((rewrite_rules, (~1, term_bool) :: irules),
+ term_bool_prop :: map (in_form o prop_of o snd) irules))
end
@@ -280,10 +257,12 @@
fun string_of_index pre i = pre ^ string_of_int i
fun new_typ sort_prefix proper T (Tidx, typs, dtyps, idx, terms) =
- let val s = string_of_index sort_prefix Tidx
- in (s, (Tidx+1, Typtab.update (T, (s, proper)) typs, dtyps, idx, terms)) end
+ let
+ val s = string_of_index sort_prefix Tidx
+ val U = revert_typ T
+ in (s, (Tidx+1, Typtab.update (U, (s, proper)) typs, dtyps, idx, terms)) end
-fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs
+fun lookup_typ (_, typs, _, _, _) = Typtab.lookup typs o revert_typ
fun fresh_typ T f cx =
(case lookup_typ cx T of
@@ -297,7 +276,7 @@
in (f, (Tidx, typs, dtyps, idx+1, terms')) end
fun fresh_fun func_prefix t ss (cx as (_, _, _, _, terms)) =
- (case Termtab.lookup terms t of
+ (case Termtab.lookup terms (revert_types t) of
SOME (f, _) => (f, cx)
| NONE => new_fun func_prefix t ss cx)
@@ -335,15 +314,15 @@
in ((make_sign (header ts) context, us), make_recon ths context) end
-fun translate {prefixes, strict, header, builtins, serialize} ctxt comments =
+fun translate config ctxt comments =
let
+ val {prefixes, is_fol, header, has_datatypes, serialize} = config
val {sort_prefix, func_prefix} = prefixes
- val {builtin_typ, builtin_num, builtin_fun, has_datatypes} = builtins
fun transT (T as TFree _) = fresh_typ T (new_typ sort_prefix true)
| transT (T as TVar _) = (fn _ => raise TYPE ("smt_translate", [T], []))
| transT (T as Type (n, Ts)) =
- (case builtin_typ ctxt T of
+ (case B.builtin_typ ctxt T of
SOME n => pair n
| NONE => fresh_typ T (fn _ => fn cx =>
if not has_datatypes then new_typ sort_prefix true T cx
@@ -387,17 +366,14 @@
transT T ##>> trans t1 ##>> trans t2 #>>
(fn ((U, u1), u2) => SLet (U, u1, u2))
| (h as Const (c as (@{const_name distinct}, T)), ts) =>
- (case builtin_fun ctxt c ts of
+ (case B.builtin_fun ctxt c ts of
SOME (n, ts) => fold_map trans ts #>> app n
| NONE => transs h T ts)
| (h as Const (c as (_, T)), ts) =>
- (case try HOLogic.dest_number t of
- SOME (T, i) =>
- (case builtin_num ctxt T i of
- SOME n => pair (SApp (n, []))
- | NONE => transs t T [])
+ (case B.builtin_num ctxt t of
+ SOME n => pair (SApp (n, []))
| NONE =>
- (case builtin_fun ctxt c ts of
+ (case B.builtin_fun ctxt c ts of
SOME (n, ts') => fold_map trans ts' #>> app n
| NONE => transs h T ts))
| (h as Free (_, T), ts) => transs h T ts
@@ -414,7 +390,7 @@
fresh_fun func_prefix t (SOME Up) ##>> fold_map trans ts #>> SApp)
end
in
- (case strict of SOME strct => strictify strct ctxt | NONE => relaxed) #>
+ (if is_fol then folify ctxt else relaxed) #>
with_context (header ctxt) trans #>> uncurry (serialize comments)
end
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Dec 07 14:53:12 2010 +0100
@@ -6,34 +6,31 @@
signature SMTLIB_INTERFACE =
sig
- type builtins = {
- builtin_typ: typ -> string option,
- builtin_num: typ -> int -> string option,
- builtin_func: string * typ -> term list -> (string * term list) option,
- builtin_pred: string * typ -> term list -> (string * term list) option,
- is_builtin_pred: string -> typ -> bool }
- val add_builtins: builtins -> Context.generic -> Context.generic
- val add_logic: (term list -> string option) -> Context.generic ->
+ val smtlibC: SMT_Config.class
+ val add_logic: int * (term list -> string option) -> Context.generic ->
Context.generic
- val extra_norm: SMT_Normalize.extra_norm
+ val setup: theory -> theory
val interface: SMT_Solver.interface
end
structure SMTLIB_Interface: SMTLIB_INTERFACE =
struct
+structure B = SMT_Builtin
structure N = SMT_Normalize
structure T = SMT_Translate
+val smtlibC = ["smtlib"]
-(** facts about uninterpreted constants **)
+
+(* facts about uninterpreted constants *)
infix 2 ??
fun (ex ?? f) irules = irules |> exists (ex o Thm.prop_of o snd) irules ? f
-(* pairs *)
+(** pairs **)
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
@@ -43,7 +40,7 @@
val add_pair_rules = exists_pair_type ?? append (map (pair ~1) pair_rules)
-(* function update *)
+(** function update **)
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
@@ -53,7 +50,7 @@
val add_fun_upd_rules = exists_fun_upd ?? append (map (pair ~1) fun_upd_rules)
-(* abs/min/max *)
+(** abs/min/max **)
val exists_abs_min_max = Term.exists_subterm (fn
Const (@{const_name abs}, _) => true
@@ -86,7 +83,7 @@
else thm
-(* include additional facts *)
+(** include additional facts **)
fun extra_norm has_datatypes irules ctxt =
irules
@@ -97,121 +94,49 @@
-(** builtins **)
-
-(* additional builtins *)
-
-type builtins = {
- builtin_typ: typ -> string option,
- builtin_num: typ -> int -> string option,
- builtin_func: string * typ -> term list -> (string * term list) option,
- builtin_pred: string * typ -> term list -> (string * term list) option,
- is_builtin_pred: string -> typ -> bool }
+(* builtins *)
-fun chained _ [] = NONE
- | chained f (b :: bs) = (case f b of SOME y => SOME y | NONE => chained f bs)
-
-fun chained' _ [] = false
- | chained' f (b :: bs) = f b orelse chained' f bs
-
-fun chained_builtin_typ bs T =
- chained (fn {builtin_typ, ...} : builtins => builtin_typ T) bs
-
-fun chained_builtin_num bs T i =
- chained (fn {builtin_num, ...} : builtins => builtin_num T i) bs
-
-fun chained_builtin_func bs c ts =
- chained (fn {builtin_func, ...} : builtins => builtin_func c ts) bs
+local
+ fun int_num _ i = SOME (string_of_int i)
-fun chained_builtin_pred bs c ts =
- chained (fn {builtin_pred, ...} : builtins => builtin_pred c ts) bs
-
-fun chained_is_builtin_pred bs n T =
- chained' (fn {is_builtin_pred, ...} : builtins => is_builtin_pred n T) bs
-
-fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
-
-structure Builtins = Generic_Data
-(
- type T = (int * builtins) list
- val empty = []
- val extend = I
- fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
-)
-
-fun add_builtins bs = Builtins.map (Ord_List.insert fst_int_ord (serial (), bs))
-
-fun get_builtins ctxt = map snd (Builtins.get (Context.Proof ctxt))
-
-
-(* basic builtins combined with additional builtins *)
-
-fun builtin_typ _ @{typ int} = SOME "Int"
- | builtin_typ ctxt T = chained_builtin_typ (get_builtins ctxt) T
-
-fun builtin_num _ @{typ int} i = SOME (string_of_int i)
- | builtin_num ctxt T i = chained_builtin_num (get_builtins ctxt) T i
+ fun distinct _ _ [t] =
+ (case try HOLogic.dest_list t of
+ SOME (ts as _ :: _) => SOME ("distinct", ts)
+ | _ => NONE)
+ | distinct _ _ _ = NONE
+in
-fun if_int_type T n =
- (case try Term.domain_type T of
- SOME @{typ int} => SOME n
- | _ => NONE)
-
-fun conn @{const_name True} = SOME "true"
- | conn @{const_name False} = SOME "false"
- | conn @{const_name Not} = SOME "not"
- | conn @{const_name HOL.conj} = SOME "and"
- | conn @{const_name HOL.disj} = SOME "or"
- | conn @{const_name HOL.implies} = SOME "implies"
- | conn @{const_name HOL.eq} = SOME "iff"
- | conn @{const_name If} = SOME "if_then_else"
- | conn _ = NONE
-
-fun distinct_pred (@{const_name distinct}, _) [t] =
- try HOLogic.dest_list t |> Option.map (pair "distinct")
- | distinct_pred _ _ = NONE
-
-fun pred @{const_name HOL.eq} _ = SOME "="
- | pred @{const_name term_eq} _ = SOME "="
- | pred @{const_name less} T = if_int_type T "<"
- | pred @{const_name less_eq} T = if_int_type T "<="
- | pred _ _ = NONE
+val setup =
+ B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
+ fold (B.add_builtin_fun' smtlibC) [
+ (@{const True}, "true"),
+ (@{const False}, "false"),
+ (* FIXME: we do not test if these constants are fully applied! *)
+ (@{const Not}, "not"),
+ (@{const HOL.conj}, "and"),
+ (@{const HOL.disj}, "or"),
+ (@{const HOL.implies}, "implies"),
+ (@{const HOL.eq (bool)}, "iff"),
+ (@{const HOL.eq ('a)}, "="),
+ (@{const If (bool)}, "if_then_else"),
+ (@{const If ('a)}, "ite"),
+ (@{const less (int)}, "<"),
+ (@{const less_eq (int)}, "<="),
+ (@{const uminus (int)}, "~"),
+ (@{const plus (int)}, "+"),
+ (@{const minus (int)}, "-"),
+ (@{const times (int)}, "*") ] #>
+ B.add_builtin_fun smtlibC (Term.dest_Const @{const distinct ('a)}, distinct)
-fun func @{const_name If} _ = SOME "ite"
- | func @{const_name uminus} T = if_int_type T "~"
- | func @{const_name plus} T = if_int_type T "+"
- | func @{const_name minus} T = if_int_type T "-"
- | func @{const_name times} T = if_int_type T "*"
- | func _ _ = NONE
-
-val is_propT = (fn @{typ prop} => true | _ => false)
-fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
-fun is_predT T = is_propT (Term.body_type T)
-
-fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
-fun is_builtin_pred ctxt (n, T) = is_predT T andalso
- (is_some (pred n T) orelse chained_is_builtin_pred (get_builtins ctxt) n T)
-
-fun builtin_fun ctxt (c as (n, T)) ts =
- let
- val builtin_func' = chained_builtin_func (get_builtins ctxt)
- fun builtin_pred' c ts =
- (case distinct_pred c ts of
- SOME b => SOME b
- | NONE => chained_builtin_pred (get_builtins ctxt) c ts)
- in
- if is_connT T then conn n |> Option.map (rpair ts)
- else if is_predT T then
- (case pred n T of SOME c' => SOME (c', ts) | NONE => builtin_pred' c ts)
- else
- (case func n T of SOME c' => SOME (c', ts) | NONE => builtin_func' c ts)
- end
+end
-(** serialization **)
+(* serialization *)
-(* header *)
+(** header **)
+
+fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
structure Logics = Generic_Data
(
@@ -221,13 +146,13 @@
fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
)
-fun add_logic l = Logics.map (Ord_List.insert fst_int_ord (serial (), l))
+fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
fun choose_logic ctxt ts =
let
fun choose [] = "AUFLIA"
- | choose ((_, l) :: ls) = (case l ts of SOME s => s | NONE => choose ls)
- in [":logic " ^ choose (rev (Logics.get (Context.Proof ctxt)))] end
+ | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
+ in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
(* serialization *)
@@ -294,21 +219,15 @@
(** interfaces **)
val interface = {
+ class = smtlibC,
extra_norm = extra_norm,
translate = {
prefixes = {
sort_prefix = "S",
func_prefix = "f"},
header = choose_logic,
- strict = SOME {
- is_builtin_conn = is_builtin_conn,
- is_builtin_pred = is_builtin_pred,
- is_builtin_distinct = true},
- builtins = {
- builtin_typ = builtin_typ,
- builtin_num = builtin_num,
- builtin_fun = builtin_fun,
- has_datatypes = false},
+ is_fol = true,
+ has_datatypes = false,
serialize = serialize}}
end
--- a/src/HOL/Tools/SMT/z3_interface.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML Tue Dec 07 14:53:12 2010 +0100
@@ -6,8 +6,8 @@
signature Z3_INTERFACE =
sig
- type builtin_fun = string * typ -> term list -> (string * term list) option
- val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic
+ val smtlib_z3C: SMT_Config.class
+ val setup: theory -> theory
val interface: SMT_Solver.interface
datatype sym = Sym of string * sym list
@@ -27,45 +27,17 @@
struct
structure U = SMT_Utils
-
-
-(** Z3-specific builtins **)
-
-type builtin_fun = string * typ -> term list -> (string * term list) option
-
-fun fst_int_ord ((s1, _), (s2, _)) = int_ord (s1, s2)
+structure B = SMT_Builtin
-structure Builtins = Generic_Data
-(
- type T = (int * builtin_fun) list
- val empty = []
- val extend = I
- fun merge (bs1, bs2) = Ord_List.union fst_int_ord bs2 bs1
-)
-
-fun add_builtin_funs b =
- Builtins.map (Ord_List.insert fst_int_ord (serial (), b))
-
-fun get_builtin_funs ctxt c ts =
- let
- fun chained [] = NONE
- | chained (b :: bs) = (case b c ts of SOME x => SOME x | _ => chained bs)
- in chained (map snd (Builtins.get (Context.Proof ctxt))) end
-
-fun z3_builtin_fun builtin_fun ctxt c ts =
- (case builtin_fun ctxt c ts of
- SOME x => SOME x
- | _ => get_builtin_funs ctxt c ts)
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
-(** interface **)
+(* interface *)
local
- val {translate, ...} = SMTLIB_Interface.interface
- val {prefixes, strict, header, builtins, serialize} = translate
- val {is_builtin_pred, ...}= the strict
- val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
+ val {translate, extra_norm, ...} = SMTLIB_Interface.interface
+ val {prefixes, is_fol, header, serialize, ...} = translate
fun is_int_div_mod @{const div (int)} = true
| is_int_div_mod @{const mod (int)} = true
@@ -76,45 +48,33 @@
then [(~1, @{thm div_by_z3div}), (~1, @{thm mod_by_z3mod})] @ irules
else irules
- fun extra_norm' has_datatypes =
- SMTLIB_Interface.extra_norm has_datatypes o add_div_mod
-
- fun z3_builtin_fun' _ (@{const_name z3div}, _) ts = SOME ("div", ts)
- | z3_builtin_fun' _ (@{const_name z3mod}, _) ts = SOME ("mod", ts)
- | z3_builtin_fun' ctxt c ts = z3_builtin_fun builtin_fun ctxt c ts
-
- val as_propT = (fn @{typ bool} => @{typ prop} | T => T)
+ fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod
in
-fun is_builtin_num ctxt (T, i) = is_some (builtin_num ctxt T i)
-
-fun is_builtin_fun ctxt (c as (n, T)) ts =
- is_some (z3_builtin_fun' ctxt c ts) orelse
- is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->))
+val setup =
+ B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
+ B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
val interface = {
+ class = smtlib_z3C,
extra_norm = extra_norm',
translate = {
prefixes = prefixes,
- strict = strict,
+ is_fol = is_fol,
header = header,
- builtins = {
- builtin_typ = builtin_typ,
- builtin_num = builtin_num,
- builtin_fun = z3_builtin_fun',
- has_datatypes = true},
+ has_datatypes = true,
serialize = serialize}}
end
-(** constructors **)
+(* constructors *)
datatype sym = Sym of string * sym list
-(* additional constructors *)
+(** additional constructors **)
type mk_builtins = {
mk_builtin_typ: sym -> typ option,
@@ -135,6 +95,8 @@
let val thy = ProofContext.theory_of ctxt
in chained (fn {mk_builtin_fun=mk, ...} : mk_builtins => mk thy s cts) bs end
+fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
+
structure Mk_Builtins = Generic_Data
(
type T = (int * mk_builtins) list
@@ -149,7 +111,7 @@
fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
-(* basic and additional constructors *)
+(** basic and additional constructors **)
fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
| mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
@@ -241,14 +203,13 @@
-(** abstraction **)
+(* abstraction *)
fun is_builtin_theory_term ctxt t =
- (case try HOLogic.dest_number t of
- SOME n => is_builtin_num ctxt n
- | NONE =>
- (case Term.strip_comb t of
- (Const c, ts) => is_builtin_fun ctxt c ts
- | _ => false))
+ if B.is_builtin_num ctxt t then true
+ else
+ (case Term.strip_comb t of
+ (Const c, ts) => B.is_builtin_fun ctxt c ts
+ | _ => false)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Dec 06 16:54:22 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Dec 07 14:53:12 2010 +0100
@@ -135,7 +135,7 @@
@{const_name HOL.eq}]
fun is_built_in_const_for_prover ctxt name (s, T) =
- if is_smt_prover ctxt name then SMT_Builtin.is_builtin ctxt (s, T)
+ if is_smt_prover ctxt name then SMT_Builtin.is_builtin_ext ctxt (s, T) [] (*FIXME*)
else member (op =) atp_irrelevant_consts s
(* FUDGE *)