--- a/src/HOL/SMT2.thy Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/SMT2.thy Thu Mar 13 13:18:14 2014 +0100
@@ -9,7 +9,7 @@
keywords "smt2_status" :: diag
begin
-ML_file "Tools/SMT2/smt2_utils.ML"
+ML_file "Tools/SMT2/smt2_util.ML"
ML_file "Tools/SMT2/smt2_failure.ML"
ML_file "Tools/SMT2/smt2_config.ML"
@@ -51,7 +51,7 @@
definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
text {*
-Weights must be non-negative. The value @{text 0} is equivalent to providing
+Weights must be nonnegative. The value @{text 0} is equivalent to providing
no weight at all.
Weights should only be used at quantifiers and only inside triggers (if the
@@ -105,14 +105,14 @@
ML_file "Tools/SMT2/z3_new_model.ML"
ML_file "Tools/SMT2/z3_new_proof.ML"
ML_file "Tools/SMT2/smt2_solver.ML"
+ML_file "Tools/SMT2/z3_new_isar.ML"
ML_file "Tools/SMT2/z3_new_interface.ML"
-ML_file "Tools/SMT2/z3_new_proof_tools.ML"
-ML_file "Tools/SMT2/z3_new_proof_literals.ML"
-ML_file "Tools/SMT2/z3_new_proof_rules.ML"
-ML_file "Tools/SMT2/z3_new_proof_methods.ML"
-ML_file "Tools/SMT2/z3_new_proof_replay.ML"
-ML_file "Tools/SMT2/z3_new_isar.ML"
-ML_file "Tools/SMT2/smt2_setup_solvers.ML"
+ML_file "Tools/SMT2/z3_new_replay_util.ML"
+ML_file "Tools/SMT2/z3_new_replay_literals.ML"
+ML_file "Tools/SMT2/z3_new_replay_rules.ML"
+ML_file "Tools/SMT2/z3_new_replay_methods.ML"
+ML_file "Tools/SMT2/z3_new_replay.ML"
+ML_file "Tools/SMT2/smt2_systems.ML"
method_setup smt2 = {*
Scan.optional Attrib.thms [] >>
--- a/src/HOL/Tools/SMT2/smt2_builtin.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_builtin.ML Thu Mar 13 13:18:14 2014 +0100
@@ -10,9 +10,9 @@
val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
(*built-in types*)
- val add_builtin_typ: SMT2_Utils.class ->
- typ * (typ -> string option) * (typ -> int -> string option) ->
- Context.generic -> Context.generic
+ val add_builtin_typ: SMT2_Util.class ->
+ typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+ Context.generic
val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
Context.generic
val dest_builtin_typ: Proof.context -> typ -> string option
@@ -26,10 +26,9 @@
(*built-in functions*)
type 'a bfun = Proof.context -> typ -> term list -> 'a
type bfunr = string * int * term list * (term list -> term)
- val add_builtin_fun: SMT2_Utils.class ->
- (string * typ) * bfunr option bfun -> Context.generic -> Context.generic
- val add_builtin_fun': SMT2_Utils.class -> term * string -> Context.generic ->
+ val add_builtin_fun: SMT2_Util.class -> (string * typ) * bfunr option bfun -> Context.generic ->
Context.generic
+ val add_builtin_fun': SMT2_Util.class -> term * string -> Context.generic -> Context.generic
val add_builtin_fun_ext: (string * typ) * term list bfun ->
Context.generic -> Context.generic
val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
@@ -56,7 +55,7 @@
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
-type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Utils.dict
+type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT2_Util.dict
fun typ_ord ((T, _), (U, _)) =
let
@@ -69,17 +68,15 @@
in tord (T, U) end
fun insert_ttab cs T f =
- SMT2_Utils.dict_map_default (cs, [])
+ SMT2_Util.dict_map_default (cs, [])
(Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
-fun merge_ttab ttabp =
- SMT2_Utils.dict_merge (Ord_List.merge typ_ord) ttabp
+fun merge_ttab ttabp = SMT2_Util.dict_merge (Ord_List.merge typ_ord) ttabp
fun lookup_ttab ctxt ttab T =
let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
in
- get_first (find_first match)
- (SMT2_Utils.dict_lookup ttab (SMT2_Config.solver_class_of ctxt))
+ get_first (find_first match) (SMT2_Util.dict_lookup ttab (SMT2_Config.solver_class_of ctxt))
end
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
@@ -120,8 +117,7 @@
fun add_builtin_typ cs (T, f, g) =
Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
-fun add_builtin_typ_ext (T, f) =
- Builtins.map (apfst (insert_ttab SMT2_Utils.basicC T (Ext f)))
+fun add_builtin_typ_ext (T, f) = Builtins.map (apfst (insert_ttab SMT2_Util.basicC T (Ext f)))
fun lookup_builtin_typ ctxt =
lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
@@ -170,7 +166,7 @@
in add_builtin_fun cs (c, bfun) end
fun add_builtin_fun_ext ((n, T), f) =
- Builtins.map (apsnd (insert_btab SMT2_Utils.basicC n T (Ext f)))
+ Builtins.map (apsnd (insert_btab SMT2_Util.basicC n T (Ext f)))
fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
--- a/src/HOL/Tools/SMT2/smt2_config.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_config.ML Thu Mar 13 13:18:14 2014 +0100
@@ -9,7 +9,7 @@
(*solver*)
type solver_info = {
name: string,
- class: Proof.context -> SMT2_Utils.class,
+ class: Proof.context -> SMT2_Util.class,
avail: unit -> bool,
options: Proof.context -> string list }
val add_solver: solver_info -> Context.generic -> Context.generic
@@ -18,7 +18,7 @@
val available_solvers_of: Proof.context -> string list
val select_solver: string -> Context.generic -> Context.generic
val solver_of: Proof.context -> string
- val solver_class_of: Proof.context -> SMT2_Utils.class
+ val solver_class_of: Proof.context -> SMT2_Util.class
val solver_options_of: Proof.context -> string list
(*options*)
@@ -57,9 +57,9 @@
type solver_info = {
name: string,
- class: Proof.context -> SMT2_Utils.class,
+ class: Proof.context -> SMT2_Util.class,
avail: unit -> bool,
- options: Proof.context -> string list }
+ options: Proof.context -> string list}
(* FIXME just one data slot (record) per program unit *)
structure Solvers = Generic_Data
--- a/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_normalize.ML Thu Mar 13 13:18:14 2014 +0100
@@ -9,8 +9,7 @@
val drop_fact_warning: Proof.context -> thm -> unit
val atomize_conv: Proof.context -> conv
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
- val add_extra_norm: SMT2_Utils.class * extra_norm -> Context.generic ->
- Context.generic
+ val add_extra_norm: SMT2_Util.class * extra_norm -> Context.generic -> Context.generic
val normalize: (int * (int option * thm)) list -> Proof.context ->
(int * thm) list * Proof.context
end
@@ -28,8 +27,7 @@
(** instantiate elimination rules **)
local
- val (cpfalse, cfalse) =
- `SMT2_Utils.mk_cprop (Thm.cterm_of @{theory} @{const False})
+ val (cpfalse, cfalse) = `SMT2_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
@@ -102,8 +100,7 @@
in
fun unfold_special_quants_conv ctxt =
- SMT2_Utils.if_exists_conv (is_some o special_quant)
- (Conv.top_conv special_quant_conv ctxt)
+ SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
val setup_unfolded_quants =
fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
@@ -144,8 +141,7 @@
"must have the same kind: " ^ Syntax.string_of_term ctxt t)
fun check_trigger_conv ctxt ct =
- if proper_quant false proper_trigger (SMT2_Utils.term_of ct) then
- Conv.all_conv ct
+ if proper_quant false proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
else check_trigger_error ctxt (Thm.term_of ct)
@@ -198,12 +194,10 @@
Pattern.matches thy (t', u) andalso not (t aconv u))
in not (Term.exists_subterm some_match u) end
- val pat =
- SMT2_Utils.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Utils.destT1
- fun mk_pat ct = Thm.apply (SMT2_Utils.instT' ct pat) ct
+ val pat = SMT2_Util.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Util.destT1
+ fun mk_pat ct = Thm.apply (SMT2_Util.instT' ct pat) ct
- fun mk_clist T = pairself (Thm.cterm_of @{theory})
- (HOLogic.cons_const T, HOLogic.nil_const T)
+ fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T)
fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern})
val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})
@@ -236,20 +230,17 @@
| has_trigger _ = false
fun try_trigger_conv cv ct =
- if SMT2_Utils.under_quant has_trigger (SMT2_Utils.term_of ct) then
- Conv.all_conv ct
+ if SMT2_Util.under_quant has_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
else Conv.try_conv cv ct
fun infer_trigger_conv ctxt =
if Config.get ctxt SMT2_Config.infer_triggers then
- try_trigger_conv
- (SMT2_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
+ try_trigger_conv (SMT2_Util.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
else Conv.all_conv
in
fun trigger_conv ctxt =
- SMT2_Utils.prop_conv
- (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
+ SMT2_Util.prop_conv (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
val setup_trigger =
fold SMT2_Builtin.add_builtin_fun_ext''
@@ -281,8 +272,7 @@
Syntax.string_of_term ctxt t)
fun check_weight_conv ctxt ct =
- if SMT2_Utils.under_quant proper_trigger (SMT2_Utils.term_of ct) then
- Conv.all_conv ct
+ if SMT2_Util.under_quant proper_trigger (SMT2_Util.term_of ct) then Conv.all_conv ct
else check_weight_error ctxt (Thm.term_of ct)
@@ -304,12 +294,11 @@
fun add_weight_conv NONE _ = Conv.all_conv
| add_weight_conv (SOME weight) ctxt =
let val cv = Conv.rewr_conv (mk_weight_eq weight)
- in SMT2_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
+ in SMT2_Util.under_quant_conv (K (under_trigger_conv cv)) ctxt end
in
fun weight_conv weight ctxt =
- SMT2_Utils.prop_conv
- (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
+ SMT2_Util.prop_conv (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
val setup_weight = SMT2_Builtin.add_builtin_fun_ext'' @{const_name SMT2.weight}
@@ -364,12 +353,11 @@
"case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
fun unfold_conv _ =
- SMT2_Utils.if_true_conv (is_case_bool o Term.head_of)
- (expand_head_conv (Conv.rewr_conv thm))
+ SMT2_Util.if_true_conv (is_case_bool o Term.head_of) (expand_head_conv (Conv.rewr_conv thm))
in
fun rewrite_case_bool_conv ctxt =
- SMT2_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
+ SMT2_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
val setup_case_bool =
SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
@@ -409,8 +397,7 @@
in
fun unfold_abs_min_max_conv ctxt =
- SMT2_Utils.if_exists_conv (is_some o abs_min_max ctxt)
- (Conv.top_conv unfold_amm_conv ctxt)
+ SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) defs
@@ -478,7 +465,7 @@
fun mk_number_eq ctxt i lhs =
let
- val eq = SMT2_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
+ val eq = SMT2_Util.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
val ctxt' = put_simpset HOL_ss ctxt addsimps @{thms Int.int_numeral}
val tac = HEADGOAL (Simplifier.simp_tac ctxt')
in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
@@ -500,11 +487,10 @@
and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
and expand_conv ctxt =
- SMT2_Utils.if_conv (is_nat_const o Term.head_of)
- (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
- (int_conv ctxt)
+ SMT2_Util.if_conv (is_nat_const o Term.head_of)
+ (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt) (int_conv ctxt)
- and nat_conv ctxt = SMT2_Utils.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
+ and nat_conv ctxt = SMT2_Util.if_exists_conv is_nat_const' (Conv.top_sweep_conv expand_conv ctxt)
val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
in
@@ -544,13 +530,12 @@
addsimps @{thms Num.numeral_One minus_zero})
fun norm_num_conv ctxt =
- SMT2_Utils.if_conv (is_strange_number ctxt)
- (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
+ SMT2_Util.if_conv (is_strange_number ctxt) (Simplifier.rewrite (put_simpset proper_num_ss ctxt))
+ Conv.no_conv
in
fun normalize_numerals_conv ctxt =
- SMT2_Utils.if_exists_conv (is_strange_number ctxt)
- (Conv.top_sweep_conv norm_num_conv ctxt)
+ SMT2_Util.if_exists_conv (is_strange_number ctxt) (Conv.top_sweep_conv norm_num_conv ctxt)
end
@@ -584,19 +569,18 @@
structure Extra_Norms = Generic_Data
(
- type T = extra_norm SMT2_Utils.dict
+ type T = extra_norm SMT2_Util.dict
val empty = []
val extend = I
- fun merge data = SMT2_Utils.dict_merge fst data
+ fun merge data = SMT2_Util.dict_merge fst data
)
-fun add_extra_norm (cs, norm) =
- Extra_Norms.map (SMT2_Utils.dict_update (cs, norm))
+fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT2_Util.dict_update (cs, norm))
fun apply_extra_norms ctxt ithms =
let
val cs = SMT2_Config.solver_class_of ctxt
- val es = SMT2_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
+ val es = SMT2_Util.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
local
--- a/src/HOL/Tools/SMT2/smt2_real.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_real.ML Thu Mar 13 13:18:14 2014 +0100
@@ -21,8 +21,8 @@
local
fun real_num _ i = SOME (string_of_int i ^ ".0")
- fun is_linear [t] = SMT2_Utils.is_number t
- | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u
+ fun is_linear [t] = SMT2_Util.is_number t
+ | is_linear [t, u] = SMT2_Util.is_number t orelse SMT2_Util.is_number u
| is_linear _ = false
fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
--- a/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:14 2014 +0100
@@ -10,7 +10,7 @@
datatype outcome = Unsat | Sat | Unknown
type solver_config = {
name: string,
- class: Proof.context -> SMT2_Utils.class,
+ class: Proof.context -> SMT2_Util.class,
avail: unit -> bool,
command: unit -> string list,
options: Proof.context -> string list,
@@ -142,7 +142,7 @@
type solver_config = {
name: string,
- class: Proof.context -> SMT2_Utils.class,
+ class: Proof.context -> SMT2_Util.class,
avail: unit -> bool,
command: unit -> string list,
options: Proof.context -> string list,
--- a/src/HOL/Tools/SMT2/smt2_systems.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/Tools/SMT2/smt2_setup_solvers.ML
+(* Title: HOL/Tools/SMT2/smt2_systems.ML
Author: Sascha Boehme, TU Muenchen
Setup SMT solvers.
*)
-signature SMT2_SETUP_SOLVERS =
+signature SMT2_SYSTEMS =
sig
datatype z3_non_commercial =
Z3_Non_Commercial_Unknown |
@@ -14,7 +14,7 @@
val z3_extensions: bool Config.T
end
-structure SMT2_Setup_Solvers: SMT2_SETUP_SOLVERS =
+structure SMT2_Systems: SMT2_SYSTEMS =
struct
(* helper functions *)
@@ -168,7 +168,7 @@
supports_filter = true,
outcome = z3_on_first_or_last_line,
cex_parser = SOME Z3_New_Model.parse_counterex,
- replay = SOME Z3_New_Proof_Replay.replay }
+ replay = SOME Z3_New_Replay.replay }
end
--- a/src/HOL/Tools/SMT2/smt2_translate.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_translate.ML Thu Mar 13 13:18:14 2014 +0100
@@ -33,7 +33,7 @@
assms: (int * thm) list }
(*translation*)
- val add_config: SMT2_Utils.class * (Proof.context -> config) -> Context.generic -> Context.generic
+ val add_config: SMT2_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
val translate: Proof.context -> string list -> (int * thm) list -> string * replay_data
end
@@ -175,7 +175,7 @@
in Abs (Name.uu, U, q $ eta I (Term.domain_type U) (Bound 0)) end
fun expf k i T t =
- let val Ts = drop i (fst (SMT2_Utils.dest_funT k T))
+ let val Ts = drop i (fst (SMT2_Util.dest_funT k T))
in
Term.incr_boundvars (length Ts) t
|> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
@@ -256,7 +256,7 @@
fun apply i t T ts =
let
val (ts1, ts2) = chop i ts
- val (_, U) = SMT2_Utils.dest_funT i T
+ val (_, U) = SMT2_Util.dest_funT i T
in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
in
@@ -459,7 +459,7 @@
| _ => raise TERM ("bad SMT term", [t]))
and transs t T ts =
- let val (Us, U) = SMT2_Utils.dest_funT (length ts) T
+ let val (Us, U) = SMT2_Util.dest_funT (length ts) T
in
fold_map transT Us ##>> transT U #-> (fn Up =>
add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
@@ -474,21 +474,21 @@
structure Configs = Generic_Data
(
- type T = (Proof.context -> config) SMT2_Utils.dict
+ type T = (Proof.context -> config) SMT2_Util.dict
val empty = []
val extend = I
- fun merge data = SMT2_Utils.dict_merge fst data
+ fun merge data = SMT2_Util.dict_merge fst data
)
-fun add_config (cs, cfg) = Configs.map (SMT2_Utils.dict_update (cs, cfg))
+fun add_config (cs, cfg) = Configs.map (SMT2_Util.dict_update (cs, cfg))
fun get_config ctxt =
let val cs = SMT2_Config.solver_class_of ctxt
in
- (case SMT2_Utils.dict_get (Configs.get (Context.Proof ctxt)) cs of
+ (case SMT2_Util.dict_get (Configs.get (Context.Proof ctxt)) cs of
SOME cfg => cfg ctxt
| NONE => error ("SMT: no translation configuration found " ^
- "for solver class " ^ quote (SMT2_Utils.string_of_class cs)))
+ "for solver class " ^ quote (SMT2_Util.string_of_class cs)))
end
fun translate ctxt comments ithms =
@@ -498,7 +498,7 @@
fun no_dtyps (tr_context, ctxt) ts =
((Termtab.empty, [], tr_context, ctxt), ts)
- val ts1 = map (Envir.beta_eta_contract o SMT2_Utils.prop_of o snd) ithms
+ val ts1 = map (Envir.beta_eta_contract o SMT2_Util.prop_of o snd) ithms
val ((funcs, dtyps, tr_context, ctxt1), ts2) =
((empty_tr_context, ctxt), ts1)
--- a/src/HOL/Tools/SMT2/smt2_util.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_util.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/Tools/SMT2/smt2_utils.ML
+(* Title: HOL/Tools/SMT2/smt2_util.ML
Author: Sascha Boehme, TU Muenchen
General utility functions.
*)
-signature SMT2_UTILS =
+signature SMT2_UTIL =
sig
(*basic combinators*)
val repeat: ('a -> 'a option) -> 'a -> 'a
@@ -61,7 +61,7 @@
val prop_conv: conv -> conv
end
-structure SMT2_Utils: SMT2_UTILS =
+structure SMT2_Util: SMT2_UTIL =
struct
(* basic combinators *)
--- a/src/HOL/Tools/SMT2/smtlib2_interface.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/smtlib2_interface.ML Thu Mar 13 13:18:14 2014 +0100
@@ -7,9 +7,8 @@
signature SMTLIB2_INTERFACE =
sig
- val smtlib2C: SMT2_Utils.class
- val add_logic: int * (term list -> string option) -> Context.generic ->
- Context.generic
+ val smtlib2C: SMT2_Util.class
+ val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
val translate_config: Proof.context -> SMT2_Translate.config
end
@@ -24,8 +23,8 @@
local
fun int_num _ i = SOME (string_of_int i)
- fun is_linear [t] = SMT2_Utils.is_number t
- | is_linear [t, u] = SMT2_Utils.is_number t orelse SMT2_Utils.is_number u
+ fun is_linear [t] = SMT2_Util.is_number t
+ | is_linear [t, u] = SMT2_Util.is_number t orelse SMT2_Util.is_number u
| is_linear _ = false
fun times _ _ ts =
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML Thu Mar 13 13:18:14 2014 +0100
@@ -6,7 +6,7 @@
signature Z3_NEW_INTERFACE =
sig
- val smtlib2_z3C: SMT2_Utils.class
+ val smtlib2_z3C: SMT2_Util.class
datatype sym = Sym of string * sym list
type mk_builtins = {
@@ -145,26 +145,21 @@
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
-val eq = SMT2_Utils.mk_const_pat @{theory} @{const_name HOL.eq} SMT2_Utils.destT1
-fun mk_eq ct cu = Thm.mk_binop (SMT2_Utils.instT' ct eq) ct cu
+val eq = SMT2_Util.mk_const_pat @{theory} @{const_name HOL.eq} SMT2_Util.destT1
+fun mk_eq ct cu = Thm.mk_binop (SMT2_Util.instT' ct eq) ct cu
val if_term =
- SMT2_Utils.mk_const_pat @{theory} @{const_name If}
- (SMT2_Utils.destT1 o SMT2_Utils.destT2)
-fun mk_if cc ct cu =
- Thm.mk_binop (Thm.apply (SMT2_Utils.instT' ct if_term) cc) ct cu
+ SMT2_Util.mk_const_pat @{theory} @{const_name If} (SMT2_Util.destT1 o SMT2_Util.destT2)
+fun mk_if cc ct = Thm.mk_binop (Thm.apply (SMT2_Util.instT' ct if_term) cc) ct
-val access =
- SMT2_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT2_Utils.destT1
-fun mk_access array = Thm.apply (SMT2_Utils.instT' array access) array
+val access = SMT2_Util.mk_const_pat @{theory} @{const_name fun_app} SMT2_Util.destT1
+fun mk_access array = Thm.apply (SMT2_Util.instT' array access) array
-val update = SMT2_Utils.mk_const_pat @{theory} @{const_name fun_upd}
- (Thm.dest_ctyp o SMT2_Utils.destT1)
+val update =
+ SMT2_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT2_Util.destT1)
fun mk_update array index value =
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
- in
- Thm.apply (Thm.mk_binop (SMT2_Utils.instTs cTs update) array index) value
- end
+ in Thm.apply (Thm.mk_binop (SMT2_Util.instTs cTs update) array index) value end
val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
val add = Thm.cterm_of @{theory} @{const plus (int)}
--- a/src/HOL/Tools/SMT2/z3_new_model.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_model.ML Thu Mar 13 13:18:14 2014 +0100
@@ -122,10 +122,8 @@
| trans_expr T (Value i) = pair (Var (("value", i), T))
| trans_expr T (Array a) = trans_array T a
| trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
- let val Ts = fst (SMT2_Utils.dest_funT (length es') (Term.fastype_of t))
- in
- fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
- end)
+ let val Ts = fst (SMT2_Util.dest_funT (length es') (Term.fastype_of t))
+ in fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t end)
and trans_array T a =
let val (dT, rT) = Term.dest_funT T
@@ -164,7 +162,7 @@
fun translate ((t, k), (e, cs)) =
let
val T = Term.fastype_of t
- val (Us, U) = SMT2_Utils.dest_funT k (Term.fastype_of t)
+ val (Us, U) = SMT2_Util.dest_funT k (Term.fastype_of t)
fun mk_full_def u' pats =
pats
--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,17 +1,17 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_replay.ML
+(* Title: HOL/Tools/SMT2/z3_new_replay.ML
Author: Sascha Boehme, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Z3 proof replay.
*)
-signature Z3_NEW_PROOF_REPLAY =
+signature Z3_NEW_REPLAY =
sig
val replay: Proof.context -> SMT2_Translate.replay_data -> string list ->
(int list * Z3_New_Proof.z3_step list) * thm
end
-structure Z3_New_Proof_Replay: Z3_NEW_PROOF_REPLAY =
+structure Z3_New_Replay: Z3_NEW_REPLAY =
struct
fun params_of t = Term.strip_qnt_vars @{const_name all} t
@@ -21,7 +21,7 @@
val maxidx = Thm.maxidx_of thm + 1
val vs = params_of (Thm.prop_of thm)
val vars = map_index (fn (i, (n, T)) => Var ((n, i + maxidx), T)) vs
- in Drule.forall_elim_list (map (SMT2_Utils.certify ctxt) vars) thm end
+ in Drule.forall_elim_list (map (SMT2_Util.certify ctxt) vars) thm end
fun add_paramTs names t =
fold2 (fn n => fn (_, T) => AList.update (op =) (n, T)) names (params_of t)
@@ -29,7 +29,7 @@
fun new_fixes ctxt nTs =
let
val (ns, ctxt') = Variable.variant_fixes (replicate (length nTs) "") ctxt
- fun mk (n, T) n' = (n, SMT2_Utils.certify ctxt' (Free (n', T)))
+ fun mk (n, T) n' = (n, SMT2_Util.certify ctxt' (Free (n', T)))
in (ctxt', Symtab.make (map2 mk nTs ns)) end
fun forall_elim_term ct (Const (@{const_name all}, _) $ (a as Abs _)) =
@@ -56,12 +56,12 @@
fun replay_thm ctxt assumed nthms
(Z3_New_Proof.Z3_Step {id, rule, concl, fixes, is_fix_step, ...}) =
- if Z3_New_Proof_Methods.is_assumption rule then
+ if Z3_New_Replay_Methods.is_assumption rule then
(case Inttab.lookup assumed id of
SOME (_, thm) => thm
- | NONE => Thm.assume (SMT2_Utils.certify ctxt concl))
+ | NONE => Thm.assume (SMT2_Util.certify ctxt concl))
else
- under_fixes (Z3_New_Proof_Methods.method_for rule) ctxt
+ under_fixes (Z3_New_Replay_Methods.method_for rule) ctxt
(if is_fix_step then (map snd nthms, []) else ([], nthms)) fixes concl
fun replay_step ctxt assumed (step as Z3_New_Proof.Z3_Step {id, prems, fixes, ...}) proofs =
@@ -77,26 +77,26 @@
| rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
- remove_fun_app, Z3_New_Proof_Literals.rewrite_true]
+ remove_fun_app, Z3_New_Replay_Literals.rewrite_true]
fun rewrite _ [] = I
| rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
fun lookup_assm assms_net ct =
- Z3_New_Proof_Tools.net_instances assms_net ct
+ Z3_New_Replay_Util.net_instances assms_net ct
|> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
in
fun add_asserted outer_ctxt rewrite_rules assms steps ctxt =
let
- val eqs = map (rewrite ctxt [Z3_New_Proof_Literals.rewrite_true]) rewrite_rules
+ val eqs = map (rewrite ctxt [Z3_New_Replay_Literals.rewrite_true]) rewrite_rules
val eqs' = union Thm.eq_thm eqs prep_rules
val assms_net =
assms
|> map (apsnd (rewrite ctxt eqs'))
|> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
- |> Z3_New_Proof_Tools.thm_net_of snd
+ |> Z3_New_Replay_Util.thm_net_of snd
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
@@ -117,9 +117,9 @@
fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...})
(cx as ((is, thms), (ctxt, ptab))) =
- if Z3_New_Proof_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
+ if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then
let
- val ct = SMT2_Utils.certify ctxt concl
+ val ct = SMT2_Util.certify ctxt concl
val thm1 =
Thm.trivial ct
|> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
@@ -154,7 +154,7 @@
end
fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
- @{thm reflexive}, Z3_New_Proof_Literals.true_thm]
+ @{thm reflexive}, Z3_New_Replay_Literals.true_thm]
val intro_def_rules = @{lemma
"(~ P | P) & (P | ~ P)"
@@ -181,7 +181,7 @@
({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output =
let
val (steps, ctxt1) = Z3_New_Proof.parse typs terms output ctxt
- val ctxt2 = put_simpset (Z3_New_Proof_Tools.make_simpset ctxt1 []) ctxt1
+ val ctxt2 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt1 []) ctxt1
val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
val proofs = fold (replay_step ctxt3 assumed) steps assumed
val (_, Z3_New_Proof.Z3_Step {id, ...}) = split_last steps
--- a/src/HOL/Tools/SMT2/z3_new_replay_literals.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_literals.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_literals.ML
+(* Title: HOL/Tools/SMT2/z3_new_replay_literals.ML
Author: Sascha Boehme, TU Muenchen
Proof tools related to conjunctions and disjunctions.
*)
-signature Z3_NEW_PROOF_LITERALS =
+signature Z3_NEW_REPLAY_LITERALS =
sig
(*literal table*)
type littab = thm Termtab.table
@@ -30,7 +30,7 @@
val prove_conj_disj_eq: cterm -> thm
end
-structure Z3_New_Proof_Literals: Z3_NEW_PROOF_LITERALS =
+structure Z3_New_Replay_Literals: Z3_NEW_REPLAY_LITERALS =
struct
@@ -39,11 +39,10 @@
type littab = thm Termtab.table
-fun make_littab thms =
- fold (Termtab.update o `SMT2_Utils.prop_of) thms Termtab.empty
+fun make_littab thms = fold (Termtab.update o `SMT2_Util.prop_of) thms Termtab.empty
-fun insert_lit thm = Termtab.update (`SMT2_Utils.prop_of thm)
-fun delete_lit thm = Termtab.delete (SMT2_Utils.prop_of thm)
+fun insert_lit thm = Termtab.update (`SMT2_Util.prop_of thm)
+fun delete_lit thm = Termtab.delete (SMT2_Util.prop_of thm)
fun lookup_lit lits = Termtab.lookup lits
fun get_first_lit f =
Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
@@ -91,7 +90,7 @@
(** explosion of conjunctions and disjunctions **)
local
- val precomp = Z3_New_Proof_Tools.precompose2
+ val precomp = Z3_New_Replay_Util.precompose2
fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
val dest_conj1 = precomp destc @{thm conjunct1}
@@ -115,7 +114,7 @@
| NONE => NONE)
fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
- val dneg_rule = Z3_New_Proof_Tools.precompose destn @{thm notnotD}
+ val dneg_rule = Z3_New_Replay_Util.precompose destn @{thm notnotD}
in
(*
@@ -150,7 +149,7 @@
(*
extract a literal by applying previously collected rules
*)
-fun extract_lit thm rules = fold Z3_New_Proof_Tools.compose rules thm
+fun extract_lit thm rules = fold Z3_New_Replay_Util.compose rules thm
(*
@@ -162,9 +161,9 @@
val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
fun explode1 thm =
- if Termtab.defined tab (SMT2_Utils.prop_of thm) then cons thm
+ if Termtab.defined tab (SMT2_Util.prop_of thm) then cons thm
else
- (case dest_rules (SMT2_Utils.prop_of thm) of
+ (case dest_rules (SMT2_Util.prop_of thm) of
SOME (rule1, rule2) =>
explode2 rule1 thm #>
explode2 rule2 thm #>
@@ -173,13 +172,13 @@
and explode2 dest_rule thm =
if full orelse
- exists_lit is_conj (Termtab.defined tab) (SMT2_Utils.prop_of thm)
- then explode1 (Z3_New_Proof_Tools.compose dest_rule thm)
- else cons (Z3_New_Proof_Tools.compose dest_rule thm)
+ exists_lit is_conj (Termtab.defined tab) (SMT2_Util.prop_of thm)
+ then explode1 (Z3_New_Replay_Util.compose dest_rule thm)
+ else cons (Z3_New_Replay_Util.compose dest_rule thm)
fun explode0 thm =
- if not is_conj andalso is_dneg (SMT2_Utils.prop_of thm)
- then [Z3_New_Proof_Tools.compose dneg_rule thm]
+ if not is_conj andalso is_dneg (SMT2_Util.prop_of thm)
+ then [Z3_New_Replay_Util.compose dneg_rule thm]
else explode1 thm []
in explode0 end
@@ -195,7 +194,7 @@
fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
- |> Z3_New_Proof_Tools.discharge thm1 |> Z3_New_Proof_Tools.discharge thm2
+ |> Z3_New_Replay_Util.discharge thm1 |> Z3_New_Replay_Util.discharge thm2
fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -219,12 +218,12 @@
fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
| dest_disj t = raise TERM ("dest_disj", [t])
- val precomp = Z3_New_Proof_Tools.precompose
+ val precomp = Z3_New_Replay_Util.precompose
val dnegE = precomp (single o d2 o d1) @{thm notnotD}
val dnegI = precomp (single o d1) @{lemma "P ==> ~~P" by fast}
fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
- val precomp2 = Z3_New_Proof_Tools.precompose2
+ val precomp2 = Z3_New_Replay_Util.precompose2
fun dni f = apsnd f o Thm.dest_binop o f o d1
val negIffE = precomp2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
val negIffI = precomp2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
@@ -243,17 +242,16 @@
fun lookup_rule t =
(case t of
- @{const Not} $ (@{const Not} $ t) =>
- (Z3_New_Proof_Tools.compose dnegI, lookup t)
+ @{const Not} $ (@{const Not} $ t) => (Z3_New_Replay_Util.compose dnegI, lookup t)
| @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
- (Z3_New_Proof_Tools.compose negIffI, lookup (iff_const $ u $ t))
+ (Z3_New_Replay_Util.compose negIffI, lookup (iff_const $ u $ t))
| @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
let fun rewr lit = lit COMP @{thm not_sym}
in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
| _ =>
(case as_dneg lookup t of
- NONE => (Z3_New_Proof_Tools.compose negIffE, as_negIff lookup t)
- | x => (Z3_New_Proof_Tools.compose dnegE, x)))
+ NONE => (Z3_New_Replay_Util.compose negIffE, as_negIff lookup t)
+ | x => (Z3_New_Replay_Util.compose dnegE, x)))
fun join1 (s, t) =
(case lookup t of
@@ -286,7 +284,7 @@
val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
fun contra_left conj thm =
let
- val rules = explode_term conj (SMT2_Utils.prop_of thm)
+ val rules = explode_term conj (SMT2_Util.prop_of thm)
fun contra_lits (t, rs) =
(case t of
@{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
@@ -303,9 +301,10 @@
val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
in
+
fun contradict conj ct =
- iff_intro (Z3_New_Proof_Tools.under_assumption (contra_left conj) ct)
- (contra_right ct)
+ iff_intro (Z3_New_Replay_Util.under_assumption (contra_left conj) ct) (contra_right ct)
+
end
local
@@ -315,8 +314,8 @@
fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
- val thm1 = Z3_New_Proof_Tools.under_assumption (prove r cr o make_tab l) cl
- val thm2 = Z3_New_Proof_Tools.under_assumption (prove l cl o make_tab r) cr
+ val thm1 = Z3_New_Replay_Util.under_assumption (prove r cr o make_tab l) cl
+ val thm2 = Z3_New_Replay_Util.under_assumption (prove l cl o make_tab r) cr
in iff_intro thm1 thm2 end
datatype conj_disj = CONJ | DISJ | NCON | NDIS
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof.ML
+(* Title: HOL/Tools/SMT2/z3_new_replay_methods.ML
Author: Sascha Boehme, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Proof methods for replaying Z3 proofs.
*)
-signature Z3_NEW_PROOF_METHODS =
+signature Z3_NEW_REPLAY_METHODS =
sig
(*abstraction*)
type abs_context = int * term Termtab.table
@@ -53,7 +53,7 @@
val method_for: Z3_New_Proof.z3_rule -> z3_method
end
-structure Z3_New_Proof_Methods: Z3_NEW_PROOF_METHODS =
+structure Z3_New_Replay_Methods: Z3_NEW_REPLAY_METHODS =
struct
type z3_method = Proof.context -> thm list -> term -> thm
@@ -90,7 +90,7 @@
fun dest_thm thm = dest_prop (Thm.concl_of thm)
-fun certify_prop ctxt t = SMT2_Utils.certify ctxt (as_prop t)
+fun certify_prop ctxt t = SMT2_Util.certify ctxt (as_prop t)
fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
| try_provers ctxt rule ((name, prover) :: named_provers) thms t =
@@ -116,12 +116,12 @@
fun match_instantiate ctxt t thm =
let
- val cert = SMT2_Utils.certify ctxt
+ val cert = SMT2_Util.certify ctxt
val thm' = match_instantiateT ctxt t thm
in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
fun apply_rule ctxt t =
- (case Z3_New_Proof_Rules.apply ctxt (certify_prop ctxt t) of
+ (case Z3_New_Replay_Rules.apply ctxt (certify_prop ctxt t) of
SOME thm => thm
| NONE => raise Fail "apply_rule")
--- a/src/HOL/Tools/SMT2/z3_new_replay_rules.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_rules.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,25 +1,23 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_rules.ML
+(* Title: HOL/Tools/SMT2/z3_new_replay_rules.ML
Author: Sascha Boehme, TU Muenchen
Custom rules for Z3 proof replay.
*)
-signature Z3_NEW_PROOF_RULES =
+signature Z3_NEW_REPLAY_RULES =
sig
val apply: Proof.context -> cterm -> thm option
end
-structure Z3_New_Proof_Rules: Z3_NEW_PROOF_RULES =
+structure Z3_New_Replay_Rules: Z3_NEW_REPLAY_RULES =
struct
-val eq = Thm.eq_thm
-
structure Data = Generic_Data
(
type T = thm Net.net
val empty = Net.empty
val extend = I
- val merge = Net.merge eq
+ val merge = Net.merge Thm.eq_thm
)
fun maybe_instantiate ct thm =
@@ -40,8 +38,8 @@
val prep = `Thm.prop_of
-fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
-fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
+fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net
+fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net
val add = Thm.declaration_attribute (Data.map o ins)
val del = Thm.declaration_attribute (Data.map o del)
--- a/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_replay_util.ML Thu Mar 13 13:18:14 2014 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/Tools/SMT2/z3_new_proof_tools.ML
+(* Title: HOL/Tools/SMT2/z3_new_replay_util.ML
Author: Sascha Boehme, TU Muenchen
Helper functions required for Z3 proof replay.
*)
-signature Z3_NEW_PROOF_TOOLS =
+signature Z3_NEW_REPLAY_UTIL =
sig
(*theorem nets*)
val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
@@ -25,7 +25,7 @@
val make_simpset: Proof.context -> thm list -> simpset
end
-structure Z3_New_Proof_Tools: Z3_NEW_PROOF_TOOLS =
+structure Z3_New_Replay_Util: Z3_NEW_REPLAY_UTIL =
struct
@@ -63,8 +63,7 @@
(* proof combinators *)
fun under_assumption f ct =
- let val ct' = SMT2_Utils.mk_cprop ct
- in Thm.implies_intr ct' (f (Thm.assume ct')) end
+ let val ct' = SMT2_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
fun discharge p pq = Thm.implies_elim pq p
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:14 2014 +0100
@@ -122,7 +122,7 @@
|> Config.put SMT2_Config.infer_triggers (Config.get ctxt smt2_triggers)
|> not (Config.get ctxt smt2_builtins)
? (SMT2_Builtin.filter_builtins is_boring_builtin_typ
- #> Config.put SMT2_Setup_Solvers.z3_extensions false)
+ #> Config.put SMT2_Systems.z3_extensions false)
|> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances
default_max_new_mono_instances