--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:05:22 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Aug 25 09:32:43 2010 +0200
@@ -469,10 +469,10 @@
it is taken to be \textit{true} for SPASS and \textit{false} for E and Vampire,
because empirical results suggest that these are the best settings.
-\opfalse{defs\_relevant}{defs\_irrelevant}
-Specifies whether the definition of constants occurring in the formula to prove
-should be considered particularly relevant. Enabling this option tends to lead
-to larger problems and typically slows down the ATPs.
+%\opfalse{defs\_relevant}{defs\_irrelevant}
+%Specifies whether the definition of constants occurring in the formula to prove
+%should be considered particularly relevant. Enabling this option tends to lead
+%to larger problems and typically slows down the ATPs.
\end{enum}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:32:43 2010 +0200
@@ -22,7 +22,6 @@
relevance_decay: real,
max_relevant_per_iter: int option,
theory_relevant: bool option,
- defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time}
@@ -91,7 +90,6 @@
relevance_decay: real,
max_relevant_per_iter: int option,
theory_relevant: bool option,
- defs_relevant: bool,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time}
@@ -216,8 +214,8 @@
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
relevance_threshold, relevance_decay,
- max_relevant_per_iter, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
+ max_relevant_per_iter, theory_relevant, isar_proof,
+ isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
let
@@ -234,7 +232,6 @@
SOME axioms => axioms
| NONE =>
(relevant_facts full_types relevance_threshold relevance_decay
- defs_relevant
(the_default default_max_relevant_per_iter
max_relevant_per_iter)
(the_default default_theory_relevant theory_relevant)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:32:43 2010 +0200
@@ -15,7 +15,7 @@
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-> (unit -> string * bool) * thm list
val relevant_facts :
- bool -> real -> real -> bool -> int -> bool -> relevance_override
+ bool -> real -> real -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
-> ((string * bool) * thm) list
end;
@@ -244,9 +244,9 @@
in if Real.isFinite res then res else 0.0 end
*)
-(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
+(* Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list
+ -> ('a * 'b) list. *)
fun add_expand_pairs (x, ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys
-
fun consts_of_term thy t =
Symtab.fold add_expand_pairs (get_consts thy (SOME true) [t]) []
@@ -254,30 +254,6 @@
(axiom, axiom |> snd |> theory_const_prop_of theory_relevant
|> consts_of_term thy)
-exception CONST_OR_FREE of unit
-
-fun dest_Const_or_Free (Const x) = x
- | dest_Const_or_Free (Free x) = x
- | dest_Const_or_Free _ = raise CONST_OR_FREE ()
-
-(*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
-fun defines thy thm gctypes =
- let val tm = prop_of thm
- fun defs lhs rhs =
- let val (rator,args) = strip_comb lhs
- val ct = const_with_typ thy (dest_Const_or_Free rator)
- in
- forall is_Var args andalso const_mem gctypes ct andalso
- subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
- end
- handle CONST_OR_FREE () => false
- in
- case tm of
- @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
- defs lhs rhs
- | _ => false
- end;
-
type annotated_thm =
((unit -> string * bool) * thm) * (string * const_typ list) list
@@ -306,7 +282,7 @@
val threshold_divisor = 2.0
val ridiculous_threshold = 0.1
-fun relevance_filter ctxt relevance_threshold relevance_decay defs_relevant
+fun relevance_filter ctxt relevance_threshold relevance_decay
max_relevant_per_iter theory_relevant
({add, del, ...} : relevance_override) axioms goal_ts =
let
@@ -366,8 +342,7 @@
SOME w => w
| NONE => axiom_weight const_tab rel_const_tab axiom_consts
in
- if weight >= threshold orelse
- (defs_relevant andalso defines thy th rel_const_tab) then
+ if weight >= threshold then
(trace_msg (fn () =>
fst (name ()) ^ " passes: " ^ Real.toString weight
^ " consts: " ^ commas (map fst axiom_consts));
@@ -608,7 +583,7 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types relevance_threshold relevance_decay defs_relevant
+fun relevant_facts full_types relevance_threshold relevance_decay
max_relevant_per_iter theory_relevant
(relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
@@ -631,7 +606,7 @@
else if relevance_threshold < 0.0 then
axioms
else
- relevance_filter ctxt relevance_threshold relevance_decay defs_relevant
+ relevance_filter ctxt relevance_threshold relevance_decay
max_relevant_per_iter theory_relevant relevance_override
axioms (concl_t :: hyp_ts))
|> map (apfst (fn f => f ()))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:32:43 2010 +0200
@@ -41,8 +41,8 @@
end
fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_decay, defs_relevant,
- isar_proof, isar_shrink_factor, ...} : params)
+ relevance_threshold, relevance_decay, isar_proof,
+ isar_shrink_factor, ...} : params)
(prover : prover) explicit_apply timeout subgoal state
name_thms_pairs =
let
@@ -53,9 +53,8 @@
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_decay = relevance_decay, max_relevant_per_iter = NONE,
- theory_relevant = NONE, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout}
+ theory_relevant = NONE, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout}
val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:32:43 2010 +0200
@@ -71,7 +71,6 @@
("relevance_decay", "31"),
("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
- ("defs_relevant", "false"),
("isar_proof", "false"),
("isar_shrink_factor", "1")]
@@ -84,7 +83,6 @@
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
("theory_irrelevant", "theory_relevant"),
- ("defs_irrelevant", "defs_relevant"),
("no_isar_proof", "isar_proof")]
val params_for_minimize =
@@ -174,7 +172,6 @@
0.01 * Real.fromInt (lookup_int "relevance_decay")
val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
val theory_relevant = lookup_bool_option "theory_relevant"
- val defs_relevant = lookup_bool "defs_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
val timeout = lookup_time "timeout"
@@ -184,9 +181,8 @@
relevance_threshold = relevance_threshold,
relevance_decay = relevance_decay,
max_relevant_per_iter = max_relevant_per_iter,
- theory_relevant = theory_relevant, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout}
+ theory_relevant = theory_relevant, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout}
end
fun get_params thy = extract_params (default_raw_params thy)