--- a/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 30 10:38:28 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Mon Aug 30 18:07:58 2010 +0200
@@ -447,7 +447,7 @@
\label{relevance-filter}
\begin{enum}
-\opdefault{relevance\_thresholds}{int\_pair}{45~95}
+\opdefault{relevance\_thresholds}{int\_pair}{45~90}
Specifies the thresholds above which facts are considered relevant by the
relevance filter. The first threshold is used for the first iteration of the
relevance filter and the second threshold is used for the last iteration (if it
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Aug 30 10:38:28 2010 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Aug 30 18:07:58 2010 +0200
@@ -12,6 +12,7 @@
"Tools/mirabelle_quickcheck.ML"
"Tools/mirabelle_refute.ML"
"Tools/mirabelle_sledgehammer.ML"
+ "Tools/mirabelle_sledgehammer_filter.ML"
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon Aug 30 18:07:58 2010 +0200
@@ -0,0 +1,164 @@
+(* Title: HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
+ Author: Jasmin Blanchette, TU Munich
+*)
+
+structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
+struct
+
+val relevance_filter_args =
+ [("abs_rel_weight", Sledgehammer_Fact_Filter.abs_rel_weight),
+ ("abs_irrel_weight", Sledgehammer_Fact_Filter.abs_irrel_weight),
+ ("skolem_irrel_weight", Sledgehammer_Fact_Filter.skolem_irrel_weight),
+ ("theory_bonus", Sledgehammer_Fact_Filter.theory_bonus),
+ ("local_bonus", Sledgehammer_Fact_Filter.local_bonus),
+ ("chained_bonus", Sledgehammer_Fact_Filter.chained_bonus),
+ ("max_imperfect", Sledgehammer_Fact_Filter.max_imperfect),
+ ("max_imperfect_exp", Sledgehammer_Fact_Filter.max_imperfect_exp),
+ ("threshold_divisor", Sledgehammer_Fact_Filter.threshold_divisor),
+ ("ridiculous_threshold", Sledgehammer_Fact_Filter.ridiculous_threshold)]
+
+structure Prooftab =
+ Table(type key = int * int val ord = prod_ord int_ord int_ord);
+
+val proof_table = Unsynchronized.ref Prooftab.empty
+
+val num_successes = Unsynchronized.ref ([] : (int * int) list)
+val num_failures = Unsynchronized.ref ([] : (int * int) list)
+val num_found_proofs = Unsynchronized.ref ([] : (int * int) list)
+val num_lost_proofs = Unsynchronized.ref ([] : (int * int) list)
+val num_found_facts = Unsynchronized.ref ([] : (int * int) list)
+val num_lost_facts = Unsynchronized.ref ([] : (int * int) list)
+
+fun get id c = the_default 0 (AList.lookup (op =) (!c) id)
+fun add id c n =
+ c := (case AList.lookup (op =) (!c) id of
+ SOME m => AList.update (op =) (id, m + n) (!c)
+ | NONE => (id, n) :: !c)
+
+fun init proof_file _ thy =
+ let
+ fun do_line line =
+ case line |> space_explode ":" of
+ [line_num, col_num, proof] =>
+ SOME (pairself (the o Int.fromString) (line_num, col_num),
+ proof |> space_explode " " |> filter_out (curry (op =) ""))
+ | _ => NONE
+ val proofs = File.read (Path.explode proof_file)
+ val proof_tab =
+ proofs |> space_explode "\n"
+ |> map_filter do_line
+ |> AList.coalesce (op =)
+ |> Prooftab.make
+ in proof_table := proof_tab; thy end
+
+fun percentage a b = if b = 0 then "N/A" else string_of_int (a * 100 div b)
+fun percentage_alt a b = percentage a (a + b)
+
+fun done id ({log, ...} : Mirabelle.done_args) =
+ if get id num_successes + get id num_failures > 0 then
+ (log "";
+ log ("Number of overall successes: " ^
+ string_of_int (get id num_successes));
+ log ("Number of overall failures: " ^ string_of_int (get id num_failures));
+ log ("Overall success rate: " ^
+ percentage_alt (get id num_successes) (get id num_failures) ^ "%");
+ log ("Number of found proofs: " ^ string_of_int (get id num_found_proofs));
+ log ("Number of lost proofs: " ^ string_of_int (get id num_lost_proofs));
+ log ("Proof found rate: " ^
+ percentage_alt (get id num_found_proofs) (get id num_lost_proofs) ^
+ "%");
+ log ("Number of found facts: " ^ string_of_int (get id num_found_facts));
+ log ("Number of lost facts: " ^ string_of_int (get id num_lost_facts));
+ log ("Fact found rate: " ^
+ percentage_alt (get id num_found_facts) (get id num_lost_facts) ^
+ "%"))
+ else
+ ()
+
+val default_max_relevant = 300
+
+fun with_index (i, s) = s ^ "@" ^ string_of_int i
+
+fun action args id ({pre, pos, log, ...} : Mirabelle.run_args) =
+ case (Position.line_of pos, Position.column_of pos) of
+ (SOME line_num, SOME col_num) =>
+ (case Prooftab.lookup (!proof_table) (line_num, col_num) of
+ SOME proofs =>
+ let
+ val {context = ctxt, facts, goal} = Proof.goal pre
+ val thy = ProofContext.theory_of ctxt
+ val args =
+ args
+ |> filter (fn (key, value) =>
+ case AList.lookup (op =) relevance_filter_args key of
+ SOME rf => (rf := the (Real.fromString value); false)
+ | NONE => true)
+
+ val {relevance_thresholds, full_types, max_relevant, theory_relevant,
+ ...} = Sledgehammer_Isar.default_params thy args
+ val subgoal = 1
+ val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
+ val facts =
+ Sledgehammer_Fact_Filter.relevant_facts ctxt full_types
+ relevance_thresholds
+ (the_default default_max_relevant max_relevant)
+ (the_default false theory_relevant)
+ {add = [], del = [], only = false} facts hyp_ts concl_t
+ |> map (fst o fst)
+ val (found_facts, lost_facts) =
+ List.concat proofs |> sort_distinct string_ord
+ |> map (fn fact => (find_index (curry (op =) fact) facts, fact))
+ |> List.partition (curry (op <=) 0 o fst)
+ |>> sort (prod_ord int_ord string_ord) ||> map snd
+ val found_proofs = filter (forall (member (op =) facts)) proofs
+ val n = length found_proofs
+ val _ =
+ if n = 0 then
+ (add id num_failures 1; log "Failure")
+ else
+ (add id num_successes 1;
+ add id num_found_proofs n;
+ log ("Success (" ^ string_of_int n ^ " of " ^
+ string_of_int (length proofs) ^ " proofs)"))
+ val _ = add id num_lost_proofs (length proofs - n)
+ val _ = add id num_found_facts (length found_facts)
+ val _ = add id num_lost_facts (length lost_facts)
+ val _ =
+ if null found_facts then
+ ()
+ else
+ let
+ val found_weight =
+ Real.fromInt (fold (fn (n, _) =>
+ Integer.add (n * n)) found_facts 0)
+ / Real.fromInt (length found_facts)
+ |> Math.sqrt |> Real.ceil
+ in
+ log ("Found facts (among " ^ string_of_int (length facts) ^
+ ", weight " ^ string_of_int found_weight ^ "): " ^
+ commas (map with_index found_facts))
+ end
+ val _ = if null lost_facts then
+ ()
+ else
+ log ("Lost facts (among " ^ string_of_int (length facts) ^
+ "): " ^ commas lost_facts)
+ in () end
+ | NONE => log "No known proof")
+ | _ => ()
+
+val proof_fileK = "proof_file"
+
+fun invoke args =
+ let
+ val (pf_args, other_args) =
+ args |> List.partition (curry (op =) proof_fileK o fst)
+ val proof_file = case pf_args of
+ [] => error "No \"proof_file\" specified"
+ | (_, s) :: _ => s
+ in Mirabelle.register (init proof_file, action other_args, done) end
+
+end;
+
+(* Workaround to keep the "mirabelle.pl" script happy *)
+structure Mirabelle_Sledgehammer_filter = Mirabelle_Sledgehammer_Filter;
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Aug 30 10:38:28 2010 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Aug 30 18:07:58 2010 +0200
@@ -51,7 +51,11 @@
}
my $tools = "";
if ($#action_files >= 0) {
- $tools = "uses " . join(" ", @action_files);
+ # uniquify
+ my $s = join ("\n", @action_files);
+ my @action_files = split(/\n/, $s . "\n" . $s);
+ %action_files = sort(@action_files);
+ $tools = "uses " . join(" ", sort(keys(%action_files)));
}
open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
@@ -71,7 +75,7 @@
END
-foreach (split(/:/, $actions)) {
+foreach (reverse(split(/:/, $actions))) {
if (m/([^[]*)(?:\[(.*)\])?/) {
my ($name, $settings_str) = ($1, $2 || "");
$name =~ s/^([a-z])/\U$1/;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 30 10:38:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 30 18:07:58 2010 +0200
@@ -216,11 +216,10 @@
relevance_thresholds, max_relevant, theory_relevant, isar_proof,
isar_shrink_factor, timeout, ...} : params)
minimize_command
- ({subgoal, goal, relevance_override, axioms} : problem) =
+ ({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override,
+ axioms} : problem) =
let
- val (ctxt, (_, th)) = goal;
- val thy = ProofContext.theory_of ctxt
- val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
+ val (_, hyp_ts, concl_t) = strip_subgoal th subgoal
val print = priority
fun print_v f = () |> verbose ? print o f
@@ -230,10 +229,10 @@
case axioms of
SOME axioms => axioms
| NONE =>
- (relevant_facts full_types relevance_thresholds
+ (relevant_facts ctxt full_types relevance_thresholds
(the_default default_max_relevant max_relevant)
(the_default default_theory_relevant theory_relevant)
- relevance_override goal hyp_ts concl_t
+ relevance_override chained_ths hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
" for " ^ quote atp_name ^ ".")) o length))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 10:38:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 30 18:07:58 2010 +0200
@@ -13,14 +13,22 @@
only: bool}
val trace : bool Unsynchronized.ref
- val term_patterns : bool Unsynchronized.ref
+ val abs_rel_weight : real Unsynchronized.ref
+ val abs_irrel_weight : real Unsynchronized.ref
+ val skolem_irrel_weight : real Unsynchronized.ref
+ val theory_bonus : real Unsynchronized.ref
+ val local_bonus : real Unsynchronized.ref
+ val chained_bonus : real Unsynchronized.ref
+ val max_imperfect : real Unsynchronized.ref
+ val max_imperfect_exp : real Unsynchronized.ref
+ val threshold_divisor : real Unsynchronized.ref
+ val ridiculous_threshold : real Unsynchronized.ref
val name_thm_pairs_from_ref :
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
-> ((string * locality) * thm) list
val relevant_facts :
- bool -> real * real -> int -> bool -> relevance_override
- -> Proof.context * (thm list * 'a) -> term list -> term
- -> ((string * locality) * thm) list
+ Proof.context -> bool -> real * real -> int -> bool -> relevance_override
+ -> thm list -> term list -> term -> ((string * locality) * thm) list
end;
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -32,7 +40,7 @@
fun trace_msg msg = if !trace then tracing (msg ()) else ()
(* experimental feature *)
-val term_patterns = Unsynchronized.ref false
+val term_patterns = false
val respect_no_atp = true
@@ -108,7 +116,7 @@
and pconst_args thy const (s, T) ts =
(if const then map ptype (these (try (Sign.const_typargs thy) (s, T)))
else []) @
- (if !term_patterns then map (pterm thy) ts else [])
+ (if term_patterns then map (pterm thy) ts else [])
and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts)
fun string_for_hyper_pconst (s, pss) =
@@ -134,7 +142,7 @@
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-fun get_pconsts thy also_skolems pos ts =
+fun pconsts_in_terms thy also_skolems pos ts =
let
val flip = Option.map not
(* We include free variables, as well as constants, to handle locales. For
@@ -148,7 +156,7 @@
(Const x, ts) => do_const true x ts
| (Free x, ts) => do_const false x ts
| (Abs (_, _, t'), ts) =>
- null ts ? add_pconst_to_table true (abs_name, [])
+ (null ts ? add_pconst_to_table true (abs_name, []))
#> fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
fun do_quantifier will_surely_be_skolemized body_t =
@@ -256,10 +264,9 @@
fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
(* FUDGE *)
-val abs_rel_weight = 0.5
-val abs_irrel_weight = 2.0
-val skolem_rel_weight = 2.0 (* impossible *)
-val skolem_irrel_weight = 0.5
+val abs_rel_weight = Unsynchronized.ref 0.5
+val abs_irrel_weight = Unsynchronized.ref 2.0
+val skolem_irrel_weight = Unsynchronized.ref 0.75
(* Computes a constant's weight, as determined by its frequency. *)
fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
@@ -267,36 +274,57 @@
else if String.isPrefix skolem_prefix s then skolem_weight
else logx (pconst_freq (match_patterns o f) const_tab c)
-val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I
-val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log
- swap
+fun rel_weight const_tab =
+ generic_weight (!abs_rel_weight) 0.0 rel_log I const_tab
+fun irrel_weight const_tab =
+ generic_weight (!abs_irrel_weight) (!skolem_irrel_weight) irrel_log swap
+ const_tab
(* FUDGE *)
-fun locality_multiplier General = 1.0
- | locality_multiplier Theory = 1.1
- | locality_multiplier Local = 1.3
- | locality_multiplier Chained = 2.0
+val theory_bonus = Unsynchronized.ref 0.1
+val local_bonus = Unsynchronized.ref 0.55
+val chained_bonus = Unsynchronized.ref 1.5
+
+fun locality_bonus General = 0.0
+ | locality_bonus Theory = !theory_bonus
+ | locality_bonus Local = !local_bonus
+ | locality_bonus Chained = !chained_bonus
fun axiom_weight loc const_tab relevant_consts axiom_consts =
case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
| (rel, irrel) =>
- case irrel |> filter_out (pconst_mem swap rel) of
- [] => 1.0
- | irrel =>
- let
- val rel_weight =
- fold (curry Real.+ o rel_weight const_tab) rel 0.0
- |> curry Real.* (locality_multiplier loc)
- val irrel_weight =
- fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
- val res = rel_weight / (rel_weight + irrel_weight)
- in if Real.isFinite res then res else 0.0 end
+ let
+ val irrel = irrel |> filter_out (pconst_mem swap rel)
+ val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
+ val irrel_weight =
+ ~ (locality_bonus loc)
+ |> fold (curry (op +) o irrel_weight const_tab) irrel
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
+
+(* FIXME: experiment
+fun debug_axiom_weight loc const_tab relevant_consts axiom_consts =
+ case axiom_consts |> List.partition (pconst_hyper_mem I relevant_consts)
+ ||> filter_out (pconst_hyper_mem swap relevant_consts) of
+ ([], _) => 0.0
+ | (rel, irrel) =>
+ let
+val _ = tracing (PolyML.makestring ("REL: ", rel))
+val _ = tracing (PolyML.makestring ("IRREL: ", irrel))(*###*)
+ val irrel = irrel |> filter_out (pconst_mem swap rel)
+ val rel_weight = 0.0 |> fold (curry (op +) o rel_weight const_tab) rel
+ val irrel_weight =
+ ~ (locality_bonus loc)
+ |> fold (curry (op +) o irrel_weight const_tab) irrel
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
+*)
fun pconsts_in_axiom thy t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (get_pconsts thy true (SOME true) [t]) []
+ (pconsts_in_terms thy true (SOME true) [t]) []
fun pair_consts_axiom theory_relevant thy axiom =
case axiom |> snd |> theory_const_prop_of theory_relevant
|> pconsts_in_axiom thy of
@@ -306,22 +334,27 @@
type annotated_thm =
(((unit -> string) * locality) * thm) * (string * pattern list) list
-fun take_most_relevant max_max_imperfect max_relevant remaining_max
+(* FUDGE *)
+val max_imperfect = Unsynchronized.ref 10.0
+val max_imperfect_exp = Unsynchronized.ref 1.0
+
+fun take_most_relevant max_relevant remaining_max
(candidates : (annotated_thm * real) list) =
let
val max_imperfect =
- Real.ceil (Math.pow (max_max_imperfect,
- Real.fromInt remaining_max
- / Real.fromInt max_relevant))
+ Real.ceil (Math.pow (!max_imperfect,
+ Math.pow (Real.fromInt remaining_max
+ / Real.fromInt max_relevant, !max_imperfect_exp)))
val (perfect, imperfect) =
- candidates |> List.partition (fn (_, w) => w > 0.99999)
- ||> sort (Real.compare o swap o pairself snd)
+ candidates |> sort (Real.compare o swap o pairself snd)
+ |> take_prefix (fn (_, w) => w > 0.99999)
val ((accepts, more_rejects), rejects) =
chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
in
- trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
- " of " ^ Int.toString (length candidates) ^ "): " ^ (accepts
- |> map (fn ((((name, _), _), _), weight) =>
+ trace_msg (fn () =>
+ "Actually passed (" ^ Int.toString (length accepts) ^ " of " ^
+ Int.toString (length candidates) ^ "): " ^
+ (accepts |> map (fn ((((name, _), _), _), weight) =>
name () ^ " [" ^ Real.toString weight ^ "]")
|> commas));
(accepts, more_rejects @ rejects)
@@ -329,16 +362,15 @@
fun if_empty_replace_with_locality thy axioms loc tab =
if Symtab.is_empty tab then
- get_pconsts thy false (SOME false)
+ pconsts_in_terms thy false (SOME false)
(map_filter (fn ((_, loc'), th) =>
if loc' = loc then SOME (prop_of th) else NONE) axioms)
else
tab
(* FUDGE *)
-val threshold_divisor = 2.0
-val ridiculous_threshold = 0.1
-val max_max_imperfect_fudge_factor = 0.66
+val threshold_divisor = Unsynchronized.ref 2.0
+val ridiculous_threshold = Unsynchronized.ref 0.1
fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
({add, del, ...} : relevance_override) axioms goal_ts =
@@ -347,13 +379,11 @@
val const_tab =
fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
val goal_const_tab =
- get_pconsts thy false (SOME false) goal_ts
+ pconsts_in_terms thy false (SOME false) goal_ts
|> fold (if_empty_replace_with_locality thy axioms)
[Chained, Local, Theory]
val add_thms = maps (ProofContext.get_fact ctxt) add
val del_thms = maps (ProofContext.get_fact ctxt) del
- val max_max_imperfect =
- Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
let
fun game_over rejects =
@@ -364,23 +394,21 @@
map_filter (fn ((p as (_, th), _), _) =>
if member Thm.eq_thm add_thms th then SOME p
else NONE) rejects
- fun relevant [] rejects hopeless [] =
+ fun relevant [] rejects [] =
(* Nothing has been added this iteration. *)
- if j = 0 andalso threshold >= ridiculous_threshold then
+ if j = 0 andalso threshold >= !ridiculous_threshold then
(* First iteration? Try again. *)
- iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
+ iter 0 max_relevant (threshold / !threshold_divisor) rel_const_tab
hopeless hopeful
else
game_over (rejects @ hopeless)
- | relevant candidates rejects hopeless [] =
+ | relevant candidates rejects [] =
let
val (accepts, more_rejects) =
- take_most_relevant max_max_imperfect max_relevant remaining_max
- candidates
+ take_most_relevant max_relevant remaining_max candidates
val rel_const_tab' =
rel_const_tab
- |> fold (add_pconst_to_table false)
- (maps (snd o fst) accepts)
+ |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
fun is_dirty (c, _) =
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
val (hopeful_rejects, hopeless_rejects) =
@@ -410,7 +438,7 @@
iter (j + 1) remaining_max threshold rel_const_tab'
hopeless_rejects hopeful_rejects)
end
- | relevant candidates rejects hopeless
+ | relevant candidates rejects
(((ax as (((_, loc), th), axiom_consts)), cached_weight)
:: hopeful) =
let
@@ -418,18 +446,18 @@
case cached_weight of
SOME w => w
| NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
-(* TODO: experiment
+(* FIXME: experiment
val name = fst (fst (fst ax)) ()
-val _ = if String.isPrefix "lift.simps(3" name then
-tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
+val _ = if String.isSubstring "abs_of_neg" name then
+tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight loc const_tab rel_const_tab axiom_consts))
else
()
*)
in
if weight >= threshold then
- relevant ((ax, weight) :: candidates) rejects hopeless hopeful
+ relevant ((ax, weight) :: candidates) rejects hopeful
else
- relevant candidates ((ax, weight) :: rejects) hopeless hopeful
+ relevant candidates ((ax, weight) :: rejects) hopeful
end
in
trace_msg (fn () =>
@@ -438,7 +466,7 @@
commas (rel_const_tab |> Symtab.dest
|> filter (curry (op <>) [] o snd)
|> map string_for_hyper_pconst));
- relevant [] [] hopeless hopeful
+ relevant [] [] hopeful
end
in
axioms |> filter_out (member Thm.eq_thm del_thms o snd)
@@ -508,6 +536,11 @@
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
+(* FIXME: make more reliable *)
+val exists_low_level_class_const =
+ exists_Const (fn (s, _) =>
+ String.isSubstring (Long_Name.separator ^ "class" ^ Long_Name.separator) s)
+
fun is_metastrange_theorem th =
case head_of (concl_of th) of
Const (a, _) => (a <> @{const_name Trueprop} andalso
@@ -588,7 +621,8 @@
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
- is_metastrange_theorem thm orelse is_that_fact thm
+ exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
+ is_that_fact thm
end
fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
@@ -673,9 +707,9 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types (threshold0, threshold1) max_relevant
+fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
theory_relevant (relevance_override as {add, del, only})
- (ctxt, (chained_ths, _)) hyp_ts concl_t =
+ chained_ths hyp_ts concl_t =
let
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 30 10:38:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 30 18:07:58 2010 +0200
@@ -67,7 +67,7 @@
("verbose", "false"),
("overlord", "false"),
("explicit_apply", "false"),
- ("relevance_thresholds", "45 95"),
+ ("relevance_thresholds", "45 90"),
("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 30 10:38:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 30 18:07:58 2010 +0200
@@ -218,8 +218,10 @@
count_combformula combformula
val optional_helpers =
- [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
- (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
+ [(["c_COMBI"], @{thms COMBI_def}),
+ (["c_COMBK"], @{thms COMBK_def}),
+ (["c_COMBB"], @{thms COMBB_def}),
+ (["c_COMBC"], @{thms COMBC_def}),
(["c_COMBS"], @{thms COMBS_def})]
val optional_typed_helpers =
[(["c_True", "c_False", "c_If"], @{thms True_or_False}),