--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri May 14 16:15:10 2010 +0200
@@ -20,9 +20,9 @@
explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
- convergence: real,
+ relevance_convergence: real,
theory_relevant: bool option,
- follow_defs: bool,
+ defs_relevant: bool,
isar_proof: bool,
shrink_factor: int,
timeout: Time.time,
@@ -79,9 +79,9 @@
explicit_apply: bool,
respect_no_atp: bool,
relevance_threshold: real,
- convergence: real,
+ relevance_convergence: real,
theory_relevant: bool option,
- follow_defs: bool,
+ defs_relevant: bool,
isar_proof: bool,
shrink_factor: int,
timeout: Time.time,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Fri May 14 16:15:10 2010 +0200
@@ -237,11 +237,12 @@
(name, {home_var, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
(params as {debug, overlord, respect_no_atp, relevance_threshold,
- convergence, theory_relevant, follow_defs, isar_proof, ...})
+ relevance_convergence, theory_relevant, defs_relevant,
+ isar_proof, ...})
minimize_command timeout =
generic_prover overlord
- (get_relevant_facts respect_no_atp relevance_threshold convergence
- follow_defs max_axiom_clauses
+ (get_relevant_facts respect_no_atp relevance_threshold
+ relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant))
(prepare_clauses false)
(write_tptp_file (debug andalso overlord)) home_var
@@ -309,12 +310,12 @@
fun generic_dfg_prover
(name, {home_var, executable, arguments, proof_delims, known_failures,
max_axiom_clauses, prefers_theory_relevant})
- (params as {overlord, respect_no_atp, relevance_threshold, convergence,
- theory_relevant, follow_defs, ...})
+ (params as {overlord, respect_no_atp, relevance_threshold,
+ relevance_convergence, theory_relevant, defs_relevant, ...})
minimize_command timeout =
generic_prover overlord
- (get_relevant_facts respect_no_atp relevance_threshold convergence
- follow_defs max_axiom_clauses
+ (get_relevant_facts respect_no_atp relevance_threshold
+ relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant))
(prepare_clauses true) write_dfg_file home_var executable
(arguments timeout) proof_delims known_failures name params
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri May 14 16:15:10 2010 +0200
@@ -253,7 +253,7 @@
end
end;
-fun relevant_clauses ctxt convergence follow_defs max_new
+fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
(relevance_override as {add, del, only}) thy ctab =
let
val thms_for_facts =
@@ -268,7 +268,7 @@
val (newrels, more_rejects) = take_best max_new newpairs
val new_consts = maps #2 newrels
val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
- val newp = p + (1.0-p) / convergence
+ val newp = p + (1.0 - p) / relevance_convergence
in
trace_msg (fn () => "relevant this iteration: " ^
Int.toString (length newrels));
@@ -283,7 +283,7 @@
else clause_weight ctab rel_consts consts_typs
in
if p <= weight orelse
- (follow_defs andalso defines thy (#1 clsthm) rel_consts) then
+ (defs_relevant andalso defines thy (#1 clsthm) rel_consts) then
(trace_msg (fn () => name ^ " clause " ^ Int.toString n ^
" passes: " ^ Real.toString weight);
relevant ((ax, weight) :: newrels, rejects) axs)
@@ -297,8 +297,9 @@
end
in iter end
-fun relevance_filter ctxt relevance_threshold convergence follow_defs max_new
- theory_relevant relevance_override thy axioms goals =
+fun relevance_filter ctxt relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant relevance_override
+ thy axioms goals =
if relevance_threshold > 0.0 then
let
val const_tab = List.foldl (count_axiom_consts theory_relevant thy)
@@ -308,8 +309,9 @@
trace_msg (fn () => "Initial constants: " ^
commas (Symtab.keys goal_const_tab))
val relevant =
- relevant_clauses ctxt convergence follow_defs max_new relevance_override
- thy const_tab relevance_threshold goal_const_tab
+ relevant_clauses ctxt relevance_convergence defs_relevant max_new
+ relevance_override thy const_tab relevance_threshold
+ goal_const_tab
(map (pair_consts_typs_axiom theory_relevant thy)
axioms)
in
@@ -504,8 +506,8 @@
fun is_first_order thy = forall (Meson.is_fol_term thy) o map prop_of
-fun get_relevant_facts respect_no_atp relevance_threshold convergence
- follow_defs max_new theory_relevant
+fun get_relevant_facts respect_no_atp relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant
(relevance_override as {add, only, ...})
(ctxt, (chain_ths, th)) goal_cls =
if (only andalso null add) orelse relevance_threshold > 1.0 then
@@ -519,9 +521,9 @@
|> restrict_to_logic thy is_FO
|> remove_unwanted_clauses
in
- relevance_filter ctxt relevance_threshold convergence follow_defs max_new
- theory_relevant relevance_override thy included_cls
- (map prop_of goal_cls)
+ relevance_filter ctxt relevance_threshold relevance_convergence
+ defs_relevant max_new theory_relevant relevance_override
+ thy included_cls (map prop_of goal_cls)
end
(* prepare for passing to writer,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri May 14 16:15:10 2010 +0200
@@ -52,14 +52,6 @@
open Sledgehammer_FOL_Clause
open Sledgehammer_Fact_Preprocessor
-(* Parameter "full_types" below indicates that full type information is to be
- exported.
-
- If "explicit_apply" is false, each function will be directly applied to as
- many arguments as possible, avoiding use of the "apply" operator. Use of
- "hBOOL" is also minimized.
-*)
-
fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
(*True if the constant ever appears outside of the top-level position in literals.
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 15:27:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 14 16:15:10 2010 +0200
@@ -94,9 +94,9 @@
("explicit_apply", "false"),
("respect_no_atp", "true"),
("relevance_threshold", "50"),
- ("convergence", "320"),
+ ("relevance_convergence", "320"),
("theory_relevant", "smart"),
- ("follow_defs", "false"),
+ ("defs_relevant", "false"),
("isar_proof", "false"),
("shrink_factor", "1"),
("minimize_timeout", "5 s")]
@@ -111,7 +111,7 @@
("implicit_apply", "explicit_apply"),
("ignore_no_atp", "respect_no_atp"),
("theory_irrelevant", "theory_relevant"),
- ("dont_follow_defs", "follow_defs"),
+ ("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
val params_for_minimize =
@@ -194,9 +194,10 @@
val respect_no_atp = lookup_bool "respect_no_atp"
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
- val convergence = 0.01 * Real.fromInt (lookup_int "convergence")
+ val relevance_convergence =
+ 0.01 * Real.fromInt (lookup_int "relevance_convergence")
val theory_relevant = lookup_bool_option "theory_relevant"
- val follow_defs = lookup_bool "follow_defs"
+ val defs_relevant = lookup_bool "defs_relevant"
val isar_proof = lookup_bool "isar_proof"
val shrink_factor = Int.max (1, lookup_int "shrink_factor")
val timeout = lookup_time "timeout"
@@ -205,9 +206,9 @@
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
- convergence = convergence, theory_relevant = theory_relevant,
- follow_defs = follow_defs, isar_proof = isar_proof,
- shrink_factor = shrink_factor, timeout = timeout,
+ relevance_convergence = relevance_convergence,
+ theory_relevant = theory_relevant, defs_relevant = defs_relevant,
+ isar_proof = isar_proof, shrink_factor = shrink_factor, timeout = timeout,
minimize_timeout = minimize_timeout}
end