make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
"max_relevant" is more reliable than "max_relevant_per_iter";
also made sure that the option is monotone -- larger values should lead to more axioms -- which wasn't always the case before;
SOS for Vampire makes a difference of about 3% (i.e. 3% more proofs are found)
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 09:42:28 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 25 17:49:52 2010 +0200
@@ -19,7 +19,7 @@
has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- default_max_relevant_per_iter: int,
+ default_max_relevant: int,
default_theory_relevant: bool,
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
@@ -52,7 +52,7 @@
has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- default_max_relevant_per_iter: int,
+ default_max_relevant: int,
default_theory_relevant: bool,
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
@@ -159,7 +159,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- default_max_relevant_per_iter = 80 (* FUDGE *),
+ default_max_relevant = 500 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -186,7 +186,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- default_max_relevant_per_iter = 40 (* FUDGE *),
+ default_max_relevant = 350 (* FUDGE *),
default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -199,10 +199,11 @@
val vampire_config : prover_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
- arguments = fn _ => fn timeout =>
- "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
- " --thanks Andrei --input_file",
- has_incomplete_mode = false,
+ arguments = fn complete => fn timeout =>
+ ("--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
+ " --thanks Andrei --input_file")
+ |> not complete ? prefix "--sos on ",
+ has_incomplete_mode = true,
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -215,7 +216,7 @@
(Unprovable, "Satisfiability detected"),
(Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option")],
- default_max_relevant_per_iter = 45 (* FUDGE *),
+ default_max_relevant = 400 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -255,7 +256,7 @@
| SOME sys => sys
fun remote_config system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses : prover_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
@@ -267,26 +268,26 @@
known_failures =
known_failures @ known_perl_failures @
[(TimedOut, "says Timeout")],
- default_max_relevant_per_iter = default_max_relevant_per_iter,
+ default_max_relevant = default_max_relevant,
default_theory_relevant = default_theory_relevant,
explicit_forall = true,
use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
fun remotify_config system_name system_versions
- ({proof_delims, known_failures, default_max_relevant_per_iter,
+ ({proof_delims, known_failures, default_max_relevant,
default_theory_relevant, use_conjecture_for_hypotheses, ...}
: prover_config) : prover_config =
remote_config system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses
val remotify_name = prefix "remote_"
fun remote_prover name system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses =
(remotify_name name,
remote_config system_name system_versions proof_delims known_failures
- default_max_relevant_per_iter default_theory_relevant
+ default_max_relevant default_theory_relevant
use_conjecture_for_hypotheses)
fun remotify_prover (name, config) system_name system_versions =
(remotify_name name, remotify_config system_name system_versions config)
@@ -294,11 +295,11 @@
val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
val remote_sine_e =
- remote_prover "sine_e" "SInE" [] []
- [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
+ remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
+ 1000 (* FUDGE *) false true
val remote_snark =
remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
- 50 (* FUDGE *) false true
+ 350 (* FUDGE *) false true
(* Setup *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 09:42:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 25 17:49:52 2010 +0200
@@ -19,8 +19,8 @@
full_types: bool,
explicit_apply: bool,
relevance_threshold: real,
- relevance_decay: real,
- max_relevant_per_iter: int option,
+ relevance_decay: real option,
+ max_relevant: int option,
theory_relevant: bool option,
isar_proof: bool,
isar_shrink_factor: int,
@@ -87,8 +87,8 @@
full_types: bool,
explicit_apply: bool,
relevance_threshold: real,
- relevance_decay: real,
- max_relevant_per_iter: int option,
+ relevance_decay: real option,
+ max_relevant: int option,
theory_relevant: bool option,
isar_proof: bool,
isar_shrink_factor: int,
@@ -187,7 +187,7 @@
val seq = extract_clause_sequence output
val name_map = extract_clause_formula_relation output
fun renumber_conjecture j =
- conjecture_prefix ^ Int.toString (j - j0)
+ conjecture_prefix ^ string_of_int (j - j0)
|> AList.find (fn (s, ss) => member (op =) ss s) name_map
|> map (fn s => find_index (curry (op =) s) seq + 1)
fun name_for_number j =
@@ -210,12 +210,11 @@
fun prover_fun atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
- known_failures, default_max_relevant_per_iter, default_theory_relevant,
+ known_failures, default_max_relevant, default_theory_relevant,
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_decay,
- max_relevant_per_iter, theory_relevant, isar_proof,
- isar_shrink_factor, timeout, ...} : params)
+ relevance_threshold, relevance_decay, max_relevant, theory_relevant,
+ isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
let
@@ -223,7 +222,7 @@
val thy = ProofContext.theory_of ctxt
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
- fun print s = (priority s; if debug then tracing s else ())
+ val print = priority
fun print_v f = () |> verbose ? print o f
fun print_d f = () |> debug ? print o f
@@ -232,8 +231,7 @@
SOME axioms => axioms
| NONE =>
(relevant_facts full_types relevance_threshold relevance_decay
- (the_default default_max_relevant_per_iter
- max_relevant_per_iter)
+ (the_default default_max_relevant max_relevant)
(the_default default_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
@@ -257,6 +255,7 @@
else error ("No such directory: " ^ the_dest_dir ^ ".")
end;
+ val measure_run_time = verbose orelse Config.get ctxt measure_runtime
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
(* write out problem file and call prover *)
fun command_line complete timeout probfile =
@@ -264,10 +263,8 @@
val core = File.shell_path command ^ " " ^ arguments complete timeout ^
" " ^ File.shell_path probfile
in
- (if Config.get ctxt measure_runtime then
- "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
- else
- "exec " ^ core) ^ " 2>&1"
+ (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
+ else "exec " ^ core) ^ " 2>&1"
end
fun split_time s =
let
@@ -296,8 +293,7 @@
prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
else
I)
- |>> (if Config.get ctxt measure_runtime then split_time
- else rpair 0)
+ |>> (if measure_run_time then split_time else rpair 0)
val (proof, outcome) =
extract_proof_and_outcome complete res_code proof_delims
known_failures output
@@ -354,6 +350,11 @@
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
(full_types, minimize_command, proof, axiom_names, th, subgoal)
+ |>> (fn message =>
+ message ^ (if verbose then
+ "\nATP CPU time: " ^ string_of_int msecs ^ " ms."
+ else
+ ""))
| SOME failure => (string_for_failure failure, [])
in
{outcome = outcome, message = message, pool = pool,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 09:42:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Aug 25 17:49:52 2010 +0200
@@ -11,11 +11,11 @@
only: bool}
val trace : bool Unsynchronized.ref
- val name_thms_pair_from_ref :
+ val name_thm_pairs_from_ref :
Proof.context -> unit Symtab.table -> thm list -> Facts.ref
- -> (unit -> string * bool) * thm list
+ -> ((unit -> string * bool) * (bool * thm)) list
val relevant_facts :
- bool -> real -> real -> int -> bool -> relevance_override
+ bool -> real -> real option -> int -> bool -> relevance_override
-> Proof.context * (thm list * 'a) -> term list -> term
-> ((string * bool) * thm) list
end;
@@ -37,13 +37,22 @@
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
-fun name_thms_pair_from_ref ctxt reserved chained_ths xref =
- let val ths = ProofContext.get_fact ctxt xref in
- (fn () => let
- val name = Facts.string_of_ref xref
- val name = name |> Symtab.defined reserved name ? quote
- val chained = forall (member Thm.eq_thm chained_ths) ths
- in (name, chained) end, ths)
+fun repair_name reserved multi j name =
+ (name |> Symtab.defined reserved name ? quote) ^
+ (if multi then "(" ^ Int.toString j ^ ")" else "")
+
+fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
+ let
+ val ths = ProofContext.get_fact ctxt xref
+ val name = Facts.string_of_ref xref
+ val multi = length ths > 1
+ in
+ fold (fn th => fn (j, rest) =>
+ (j + 1, (fn () => (repair_name reserved multi j name,
+ member Thm.eq_thm chained_ths th),
+ (multi, th)) :: rest))
+ ths (1, [])
+ |> snd
end
(***************************************************************)
@@ -53,30 +62,44 @@
(*** constants with types ***)
(*An abstraction of Isabelle types*)
-datatype const_typ = CTVar | CType of string * const_typ list
+datatype pseudotype = PVar | PType of string * pseudotype list
+
+fun string_for_pseudotype PVar = "?"
+ | string_for_pseudotype (PType (s, Ts)) =
+ (case Ts of
+ [] => ""
+ | [T] => string_for_pseudotype T
+ | Ts => string_for_pseudotypes Ts ^ " ") ^ s
+and string_for_pseudotypes Ts =
+ "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
(*Is the second type an instance of the first one?*)
-fun match_type (CType(con1,args1)) (CType(con2,args2)) =
- con1=con2 andalso match_types args1 args2
- | match_type CTVar _ = true
- | match_type _ CTVar = false
-and match_types [] [] = true
- | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
+fun match_pseudotype (PType (a, T), PType (b, U)) =
+ a = b andalso match_pseudotypes (T, U)
+ | match_pseudotype (PVar, _) = true
+ | match_pseudotype (_, PVar) = false
+and match_pseudotypes ([], []) = true
+ | match_pseudotypes (T :: Ts, U :: Us) =
+ match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
(*Is there a unifiable constant?*)
-fun const_mem const_tab (c, c_typ) =
- exists (match_types c_typ) (these (Symtab.lookup const_tab c))
+fun pseudoconst_mem f const_tab (c, c_typ) =
+ exists (curry (match_pseudotypes o f) c_typ)
+ (these (Symtab.lookup const_tab c))
-(*Maps a "real" type to a const_typ*)
-fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
- | const_typ_of (TFree _) = CTVar
- | const_typ_of (TVar _) = CTVar
+fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
+ | pseudotype_for (TFree _) = PVar
+ | pseudotype_for (TVar _) = PVar
+(* Pairs a constant with the list of its type instantiations. *)
+fun pseudoconst_for thy (c, T) =
+ (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
+ handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *)
-(*Pairs a constant with the list of its type instantiations (using const_typ)*)
-fun const_with_typ thy (c,typ) =
- let val tvars = Sign.const_typargs thy (c,typ) in
- (c, map const_typ_of tvars) end
- handle TYPE _ => (c, []) (*Variable (locale constant): monomorphic*)
+fun string_for_pseudoconst (s, []) = s
+ | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
+fun string_for_super_pseudoconst (s, [[]]) = s
+ | string_for_super_pseudoconst (s, Tss) =
+ s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
(*Add a const/type pair to the table, but a [] entry means a standard connective,
which we ignore.*)
@@ -86,7 +109,7 @@
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-val fresh_prefix = "Sledgehammer.FRESH."
+val fresh_prefix = "Sledgehammer.skolem."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
val boring_consts =
@@ -99,7 +122,7 @@
introduce a fresh constant to simulate the effect of Skolemization. *)
fun do_term t =
case t of
- Const x => add_const_to_table (const_with_typ thy x)
+ Const x => add_const_to_table (pseudoconst_for thy x)
| Free (s, _) => add_const_to_table (s, [])
| t1 $ t2 => fold do_term [t1, t2]
| Abs (_, _, t') => do_term t'
@@ -166,23 +189,23 @@
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
first by constant name and second by its list of type instantiations. For the
- latter, we need a linear ordering on "const_typ list". *)
+ latter, we need a linear ordering on "pseudotype list". *)
-fun const_typ_ord p =
+fun pseudotype_ord p =
case p of
- (CTVar, CTVar) => EQUAL
- | (CTVar, CType _) => LESS
- | (CType _, CTVar) => GREATER
- | (CType q1, CType q2) =>
- prod_ord fast_string_ord (dict_ord const_typ_ord) (q1, q2)
+ (PVar, PVar) => EQUAL
+ | (PVar, PType _) => LESS
+ | (PType _, PVar) => GREATER
+ | (PType q1, PType q2) =>
+ prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
structure CTtab =
- Table(type key = const_typ list val ord = dict_ord const_typ_ord)
+ Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
fun count_axiom_consts theory_relevant thy (_, th) =
let
fun do_const (a, T) =
- let val (c, cts) = const_with_typ thy (a, T) in
+ let val (c, cts) = pseudoconst_for thy (a, T) in
(* Two-dimensional table update. Constant maps to types maps to
count. *)
CTtab.map_default (cts, 0) (Integer.add 1)
@@ -199,8 +222,8 @@
(**** Actual Filtering Code ****)
(*The frequency of a constant is the sum of those of all instances of its type.*)
-fun const_frequency const_tab (c, cts) =
- CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
+fun pseudoconst_freq match const_tab (c, cts) =
+ CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
(the (Symtab.lookup const_tab c)) 0
handle Option.Option => 0
@@ -214,29 +237,22 @@
fun irrel_log (x : real) = Math.ln (x + 19.0) / 6.4
(* Computes a constant's weight, as determined by its frequency. *)
-val rel_const_weight = rel_log o real oo const_frequency
-val irrel_const_weight = irrel_log o real oo const_frequency
-(* fun irrel_const_weight _ _ = 1.0 FIXME: OLD CODE *)
+val rel_weight = rel_log o real oo pseudoconst_freq match_pseudotypes
+val irrel_weight =
+ irrel_log o real oo pseudoconst_freq (match_pseudotypes o swap)
+(* fun irrel_weight _ _ = 1.0 FIXME: OLD CODE *)
fun axiom_weight const_tab relevant_consts axiom_consts =
- let
- val (rel, irrel) = List.partition (const_mem relevant_consts) axiom_consts
- val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
- val irrel_weight = fold (curry Real.+ o irrel_const_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
-
-(* OLD CODE:
-(*Relevant constants are weighted according to frequency,
- but irrelevant constants are simply counted. Otherwise, Skolem functions,
- which are rare, would harm a formula's chances of being picked.*)
-fun axiom_weight const_tab relevant_consts axiom_consts =
- let
- val rel = filter (const_mem relevant_consts) axiom_consts
- val rel_weight = fold (curry Real.+ o rel_const_weight const_tab) rel 0.0
- val res = rel_weight / (rel_weight + real (length axiom_consts - length rel))
- in if Real.isFinite res then res else 0.0 end
-*)
+ case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
+ ||> filter_out (pseudoconst_mem swap relevant_consts) of
+ ([], []) => 0.0
+ | (_, []) => 1.0
+ | (rel, irrel) =>
+ let
+ val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
+ 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
fun consts_of_term thy t =
Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
@@ -247,83 +263,82 @@
|> consts_of_term thy)
type annotated_thm =
- ((unit -> string * bool) * thm) * (string * const_typ list) list
+ ((unit -> string * bool) * thm) * (string * pseudotype list) list
-(*For a reverse sort, putting the largest values first.*)
-fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
+fun rev_compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
-(* Limit the number of new facts, to prevent runaway acceptance. *)
-fun take_best max_relevant_per_iter (new_pairs : (annotated_thm * real) list) =
- let val nnew = length new_pairs in
- if nnew <= max_relevant_per_iter then
- (map #1 new_pairs, [])
- else
- let
- val new_pairs = sort compare_pairs new_pairs
- val accepted = List.take (new_pairs, max_relevant_per_iter)
- in
- trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
- ", exceeds the limit of " ^ Int.toString max_relevant_per_iter));
- trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
- trace_msg (fn () => "Actually passed: " ^
- space_implode ", " (map (fst o (fn f => f ()) o fst o fst o fst) accepted));
- (map #1 accepted, List.drop (new_pairs, max_relevant_per_iter))
- end
- end;
+fun take_best max (new_pairs : (annotated_thm * real) list) =
+ let
+ val ((perfect, more_perfect), imperfect) =
+ new_pairs |> List.partition (fn (_, w) => w > 0.99999)
+ |>> chop (max - 1) ||> sort rev_compare_pairs
+ val (accepted, rejected) =
+ case more_perfect @ imperfect of
+ [] => (perfect, [])
+ | (q :: qs) => (q :: perfect, qs)
+ in
+ trace_msg (fn () => "Number of candidates: " ^
+ string_of_int (length new_pairs));
+ trace_msg (fn () => "Effective threshold: " ^
+ Real.toString (#2 (hd accepted)));
+ trace_msg (fn () => "Actually passed: " ^
+ (accepted |> map (fn (((name, _), _), weight) =>
+ fst (name ()) ^ " [" ^ Real.toString weight ^ "]")
+ |> commas));
+ (map #1 accepted, rejected)
+ end
val threshold_divisor = 2.0
val ridiculous_threshold = 0.1
-fun relevance_filter ctxt relevance_threshold relevance_decay
- max_relevant_per_iter theory_relevant
- ({add, del, ...} : relevance_override) axioms goal_ts =
+fun relevance_filter ctxt relevance_threshold relevance_decay max_relevant
+ theory_relevant ({add, del, ...} : relevance_override)
+ axioms goal_ts =
let
val thy = ProofContext.theory_of ctxt
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
- val goal_const_tab = get_consts thy (SOME false) goal_ts
- val _ =
- trace_msg (fn () => "Initial constants: " ^
- commas (goal_const_tab |> Symtab.dest
- |> filter (curry (op <>) [] o snd)
- |> map fst))
val add_thms = maps (ProofContext.get_fact ctxt) add
val del_thms = maps (ProofContext.get_fact ctxt) del
- fun iter j threshold rel_const_tab =
+ fun iter j max threshold rel_const_tab rest =
let
+ fun game_over rejects =
+ if j = 0 andalso threshold >= ridiculous_threshold then
+ (* First iteration? Try again. *)
+ iter 0 max (threshold / threshold_divisor) rel_const_tab rejects
+ else
+ (* Add "add:" facts. *)
+ if null add_thms then
+ []
+ else
+ map_filter (fn ((p as (_, th), _), _) =>
+ if member Thm.eq_thm add_thms th then SOME p
+ else NONE) rejects
fun relevant ([], rejects) [] =
- (* Nothing was added this iteration. *)
- if j = 0 andalso threshold >= ridiculous_threshold then
- (* First iteration? Try again. *)
- iter 0 (threshold / threshold_divisor) rel_const_tab
- (map (apsnd SOME) rejects)
- else
- (* Add "add:" facts. *)
- if null add_thms then
- []
- else
- map_filter (fn ((p as (_, th), _), _) =>
- if member Thm.eq_thm add_thms th then SOME p
- else NONE) rejects
+ (* Nothing has been added this iteration. *)
+ game_over (map (apsnd SOME) rejects)
| relevant (new_pairs, rejects) [] =
let
- val (new_rels, more_rejects) =
- take_best max_relevant_per_iter new_pairs
+ val (new_rels, more_rejects) = take_best max new_pairs
val rel_const_tab' =
rel_const_tab |> fold add_const_to_table (maps snd new_rels)
- fun is_dirty c =
- const_mem rel_const_tab' c andalso
- not (const_mem rel_const_tab c)
+ fun is_dirty (c, _) =
+ Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
val rejects =
more_rejects @ rejects
|> map (fn (ax as (_, consts), old_weight) =>
(ax, if exists is_dirty consts then NONE
else SOME old_weight))
val threshold = threshold + (1.0 - threshold) * relevance_decay
+ val max = max - length new_rels
in
- trace_msg (fn () => "relevant this iteration: " ^
- Int.toString (length new_rels));
- map #1 new_rels @ iter (j + 1) threshold rel_const_tab' rejects
+ trace_msg (fn () => "New or updated constants: " ^
+ commas (rel_const_tab' |> Symtab.dest
+ |> subtract (op =) (Symtab.dest rel_const_tab)
+ |> map string_for_super_pseudoconst));
+ map #1 new_rels @
+ (if max = 0 then game_over rejects
+ else iter (j + 1) max threshold rel_const_tab' rejects)
end
| relevant (new_rels, rejects)
(((ax as ((name, th), axiom_consts)), cached_weight)
@@ -335,26 +350,29 @@
| NONE => axiom_weight const_tab rel_const_tab axiom_consts
in
if weight >= threshold then
- (trace_msg (fn () =>
- fst (name ()) ^ " passes: " ^ Real.toString weight
- ^ " consts: " ^ commas (map fst axiom_consts));
- relevant ((ax, weight) :: new_rels, rejects) rest)
+ relevant ((ax, weight) :: new_rels, rejects) rest
else
relevant (new_rels, (ax, weight) :: rejects) rest
end
in
- trace_msg (fn () => "relevant_facts, current threshold: " ^
- Real.toString threshold);
- relevant ([], [])
+ trace_msg (fn () =>
+ "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
+ Real.toString threshold ^ ", constants: " ^
+ commas (rel_const_tab |> Symtab.dest
+ |> filter (curry (op <>) [] o snd)
+ |> map string_for_super_pseudoconst));
+ relevant ([], []) rest
end
in
axioms |> filter_out (member Thm.eq_thm del_thms o snd)
|> map (rpair NONE o pair_consts_axiom theory_relevant thy)
- |> iter 0 relevance_threshold goal_const_tab
+ |> iter 0 max_relevant relevance_threshold
+ (get_consts thy (SOME false) goal_ts)
|> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
end
+
(***************************************************************)
(* Retrieving and filtering lemmas *)
(***************************************************************)
@@ -547,14 +565,7 @@
val name2 = Name_Space.extern full_space name0
in
case find_first check_thms [name1, name2, name0] of
- SOME name =>
- let
- val name =
- name |> Symtab.defined reserved name ? quote
- in
- if multi then name ^ "(" ^ Int.toString j ^ ")"
- else name
- end
+ SOME name => repair_name reserved multi j name
| NONE => ""
end, is_chained th), (multi, th)) :: rest)) ths
#> snd
@@ -567,25 +578,26 @@
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
fun name_thm_pairs ctxt respect_no_atp =
- List.partition (fst o snd) #> op @
- #> map (apsnd snd)
+ List.partition (fst o snd) #> op @ #> map (apsnd snd)
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
(***************************************************************)
(* ATP invocation methods setup *)
(***************************************************************)
-fun relevant_facts full_types relevance_threshold relevance_decay
- max_relevant_per_iter theory_relevant
- (relevance_override as {add, del, only})
+fun relevant_facts full_types relevance_threshold relevance_decay max_relevant
+ theory_relevant (relevance_override as {add, del, only})
(ctxt, (chained_ths, _)) hyp_ts concl_t =
let
+ val relevance_decay =
+ case relevance_decay of
+ SOME x => x
+ | NONE => 0.35 / Math.ln (Real.fromInt (max_relevant + 1))
val add_thms = maps (ProofContext.get_fact ctxt) add
val reserved = reserved_isar_keyword_table ()
val axioms =
(if only then
- maps ((fn (n, ths) => map (pair n o pair false) ths)
- o name_thms_pair_from_ref ctxt reserved chained_ths) add
+ maps (name_thm_pairs_from_ref ctxt reserved chained_ths) add
else
all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
|> name_thm_pairs ctxt (respect_no_atp andalso not only)
@@ -598,11 +610,10 @@
else if relevance_threshold < 0.0 then
axioms
else
- 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 ()))
- |> sort_wrt (fst o fst)
+ relevance_filter ctxt relevance_threshold relevance_decay max_relevant
+ theory_relevant relevance_override axioms
+ (concl_t :: hyp_ts))
+ |> map (apfst (fn f => f ())) |> sort_wrt (fst o fst)
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:42:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 17:49:52 2010 +0200
@@ -40,22 +40,20 @@
"")
end
-fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_decay, isar_proof,
+fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
isar_shrink_factor, ...} : params)
(prover : prover) explicit_apply timeout subgoal state
- name_thms_pairs =
+ axioms =
let
val _ =
- priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
+ priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
val params =
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = relevance_threshold,
- relevance_decay = relevance_decay, max_relevant_per_iter = NONE,
+ relevance_threshold = 1.1, relevance_decay = NONE, max_relevant = NONE,
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 axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
@@ -65,7 +63,7 @@
in
priority (case outcome of
NONE =>
- if length used_thm_names = length name_thms_pairs then
+ if length used_thm_names = length axioms then
"Found proof."
else
"Found proof with " ^ n_theorems used_thm_names ^ "."
@@ -91,10 +89,9 @@
val fudge_msecs = 1000
fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | minimize_theorems
- (params as {debug, atps = atp :: _, full_types, isar_proof,
- isar_shrink_factor, timeout, ...})
- i n state name_thms_pairs =
+ | minimize_theorems (params as {debug, atps = atp :: _, full_types,
+ isar_proof, isar_shrink_factor, timeout, ...})
+ i n state axioms =
let
val thy = Proof.theory_of state
val prover = get_prover_fun thy atp
@@ -104,13 +101,12 @@
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @
- maps (map prop_of o snd) name_thms_pairs))
+ (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
fun do_test timeout =
test_theorems params prover explicit_apply timeout i state
val timer = Timer.startRealTimer ()
in
- (case do_test timeout name_thms_pairs of
+ (case do_test timeout axioms of
result as {outcome = NONE, pool, used_thm_names,
conjecture_shape, ...} =>
let
@@ -120,7 +116,7 @@
|> Time.fromMilliseconds
val (min_thms, {proof, axiom_names, ...}) =
sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_thm_names name_thms_pairs) ([], result)
+ (filter_used_facts used_thm_names axioms) ([], result)
val n = length min_thms
val _ = priority (cat_lines
["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
@@ -152,15 +148,14 @@
val ctxt = Proof.context_of state
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
- val name_thms_pairs =
- map (apfst (fn f => f ())
- o name_thms_pair_from_ref ctxt reserved chained_ths) refs
+ val axioms =
+ maps (map (fn (name, (_, th)) => (name (), [th]))
+ o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
in
case subgoal_count state of
0 => priority "No subgoal!"
| n =>
- (kill_atps ();
- priority (#2 (minimize_theorems params i n state name_thms_pairs)))
+ (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:42:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 17:49:52 2010 +0200
@@ -68,8 +68,8 @@
("overlord", "false"),
("explicit_apply", "false"),
("relevance_threshold", "40"),
- ("relevance_decay", "31"),
- ("max_relevant_per_iter", "smart"),
+ ("relevance_decay", "smart"),
+ ("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1")]
@@ -169,8 +169,9 @@
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_decay =
- 0.01 * Real.fromInt (lookup_int "relevance_decay")
- val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
+ lookup_int_option "relevance_decay"
+ |> Option.map (fn n => 0.01 * Real.fromInt n)
+ val max_relevant = lookup_int_option "max_relevant"
val theory_relevant = lookup_bool_option "theory_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
@@ -179,8 +180,7 @@
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
- relevance_decay = relevance_decay,
- max_relevant_per_iter = max_relevant_per_iter,
+ relevance_decay = relevance_decay, max_relevant = max_relevant,
theory_relevant = theory_relevant, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout}
end