got rid of the "theory_relevant" option;
instead, have fudge factors that behave more smoothly for all provers
--- a/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 01 16:46:11 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Wed Sep 01 17:27:10 2010 +0200
@@ -467,11 +467,11 @@
filter. If the option is set to \textit{smart}, it is set to a value that was
empirically found to be appropriate for the ATP. A typical value would be 300.
-\opsmartx{theory\_relevant}{theory\_irrelevant}
-Specifies whether the theory from which a fact comes should be taken into
-consideration by the relevance filter. If the option is set to \textit{smart},
-it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
-empirical results suggest that these are the best settings.
+%\opsmartx{theory\_relevant}{theory\_irrelevant}
+%Specifies whether the theory from which a fact comes should be taken into
+%consideration by the relevance filter. If the option is set to \textit{smart},
+%it is taken to be \textit{true} for SPASS and \textit{false} for the other ATPs;
+%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
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 17:27:10 2010 +0200
@@ -103,15 +103,14 @@
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 {relevance_thresholds, full_types, max_relevant, ...} =
+ Sledgehammer_Isar.default_params thy args
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
SF.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) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 01 17:27:10 2010 +0200
@@ -20,7 +20,6 @@
proof_delims: (string * string) list,
known_failures: (failure * string) list,
default_max_relevant: int,
- default_theory_relevant: bool,
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
@@ -53,7 +52,6 @@
proof_delims: (string * string) list,
known_failures: (failure * string) list,
default_max_relevant: int,
- default_theory_relevant: bool,
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
@@ -160,7 +158,6 @@
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
default_max_relevant = 500 (* FUDGE *),
- default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -187,7 +184,6 @@
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
default_max_relevant = 350 (* FUDGE *),
- default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -217,7 +213,6 @@
(Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option")],
default_max_relevant = 400 (* FUDGE *),
- default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -256,8 +251,8 @@
| SOME sys => sys
fun remote_config system_name system_versions proof_delims known_failures
- default_max_relevant default_theory_relevant
- use_conjecture_for_hypotheses : prover_config =
+ default_max_relevant use_conjecture_for_hypotheses
+ : prover_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
@@ -269,26 +264,21 @@
known_failures @ known_perl_failures @
[(TimedOut, "says Timeout")],
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,
- default_theory_relevant, use_conjecture_for_hypotheses, ...}
- : prover_config) : prover_config =
+ use_conjecture_for_hypotheses, ...} : prover_config) : prover_config =
remote_config system_name system_versions proof_delims known_failures
- default_max_relevant default_theory_relevant
- use_conjecture_for_hypotheses
+ default_max_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 default_theory_relevant
- use_conjecture_for_hypotheses =
+ default_max_relevant use_conjecture_for_hypotheses =
(remotify_name name,
remote_config system_name system_versions proof_delims known_failures
- default_max_relevant default_theory_relevant
- use_conjecture_for_hypotheses)
+ default_max_relevant use_conjecture_for_hypotheses)
fun remotify_prover (name, config) system_name system_versions =
(remotify_name name, remotify_config system_name system_versions config)
@@ -296,10 +286,10 @@
val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
val remote_sine_e =
remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
- 1000 (* FUDGE *) false true
+ 1000 (* FUDGE *) true
val remote_snark =
remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
- 350 (* FUDGE *) false true
+ 350 (* FUDGE *) true
(* Setup *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 17:27:10 2010 +0200
@@ -22,7 +22,6 @@
explicit_apply: bool,
relevance_thresholds: real * real,
max_relevant: int option,
- theory_relevant: bool option,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time,
@@ -91,7 +90,6 @@
explicit_apply: bool,
relevance_thresholds: real * real,
max_relevant: int option,
- theory_relevant: bool option,
isar_proof: bool,
isar_shrink_factor: int,
timeout: Time.time,
@@ -215,11 +213,11 @@
fun prover_fun atp_name
{exec, required_execs, arguments, has_incomplete_mode, proof_delims,
- known_failures, default_max_relevant, default_theory_relevant,
- explicit_forall, use_conjecture_for_hypotheses}
+ known_failures, default_max_relevant, explicit_forall,
+ use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_thresholds, max_relevant, theory_relevant, isar_proof,
- isar_shrink_factor, timeout, ...} : params)
+ relevance_thresholds, max_relevant, isar_proof, isar_shrink_factor,
+ timeout, ...} : params)
minimize_command
({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override,
axioms} : problem) =
@@ -236,7 +234,6 @@
| NONE =>
(relevant_facts ctxt full_types relevance_thresholds
(the_default default_max_relevant max_relevant)
- (the_default default_theory_relevant theory_relevant)
relevance_override chained_ths hyp_ts concl_t
|> tap ((fn n => print_v (fn () =>
"Selected " ^ string_of_int n ^ " fact" ^ plural_s n ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 01 17:27:10 2010 +0200
@@ -34,7 +34,7 @@
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
val relevant_facts :
- Proof.context -> bool -> real * real -> int -> bool -> relevance_override
+ Proof.context -> bool -> real * real -> int -> relevance_override
-> thm list -> term list -> term -> ((string * locality) * thm) list
end;
@@ -46,10 +46,28 @@
val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
-(* experimental feature *)
+(* experimental features *)
val term_patterns = false
+val respect_no_atp = true
-val respect_no_atp = true
+(* FUDGE *)
+val worse_irrel_freq = Unsynchronized.ref 100.0
+val higher_order_irrel_weight = Unsynchronized.ref 1.05
+val abs_rel_weight = Unsynchronized.ref 0.5
+val abs_irrel_weight = Unsynchronized.ref 2.0
+val skolem_irrel_weight = Unsynchronized.ref 0.75
+val theory_const_rel_weight = Unsynchronized.ref 0.5
+val theory_const_irrel_weight = Unsynchronized.ref 0.25
+val intro_bonus = Unsynchronized.ref 0.15
+val elim_bonus = Unsynchronized.ref 0.15
+val simp_bonus = Unsynchronized.ref 0.15
+val local_bonus = Unsynchronized.ref 0.55
+val assum_bonus = Unsynchronized.ref 1.05
+val chained_bonus = Unsynchronized.ref 1.5
+val max_imperfect = Unsynchronized.ref 11.5
+val max_imperfect_exp = Unsynchronized.ref 1.0
+val threshold_divisor = Unsynchronized.ref 2.0
+val ridiculous_threshold = Unsynchronized.ref 0.1
datatype locality = General | Intro | Elim | Simp | Local | Assum | Chained
@@ -235,8 +253,9 @@
(*Inserts a dummy "constant" referring to the theory name, so that relevance
takes the given theory into account.*)
-fun theory_const_prop_of theory_relevant th =
- if theory_relevant then
+fun theory_const_prop_of th =
+ if exists (curry (op <) 0.0) [!theory_const_rel_weight,
+ !theory_const_irrel_weight] then
let
val name = Context.theory_name (theory_of_thm th)
val t = Const (name ^ theory_const_suffix, @{typ bool})
@@ -262,7 +281,7 @@
structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
-fun count_axiom_consts theory_relevant thy =
+fun count_axiom_consts thy =
let
fun do_const const (s, T) ts =
(* Two-dimensional table update. Constant maps to types maps to count. *)
@@ -275,7 +294,7 @@
| (Free x, ts) => do_const false x ts
| (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
- in do_term o theory_const_prop_of theory_relevant o snd end
+ in do_term o theory_const_prop_of o snd end
(**** Actual Filtering Code ****)
@@ -298,10 +317,6 @@
rare ones. *)
fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
-(* FUDGE *)
-val worse_irrel_freq = Unsynchronized.ref 100.0
-val higher_order_irrel_weight = Unsynchronized.ref 1.05
-
(* Irrelevant constants are treated differently. We associate lower penalties to
very rare constants and very common ones -- the former because they can't
lead to the inclusion of too many new facts, and the latter because they are
@@ -313,13 +328,6 @@
* pow_int (!higher_order_irrel_weight) (order - 1)
end
-(* FUDGE *)
-val abs_rel_weight = Unsynchronized.ref 0.5
-val abs_irrel_weight = Unsynchronized.ref 2.0
-val skolem_irrel_weight = Unsynchronized.ref 0.75
-val theory_const_rel_weight = Unsynchronized.ref 0.5
-val theory_const_irrel_weight = Unsynchronized.ref 0.25
-
(* Computes a constant's weight, as determined by its frequency. *)
fun generic_pconst_weight abs_weight skolem_weight theory_const_weight
weight_for f const_tab (c as (s, PType (m, _))) =
@@ -335,14 +343,6 @@
generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
(!theory_const_irrel_weight) irrel_weight_for swap const_tab
-(* FUDGE *)
-val intro_bonus = Unsynchronized.ref 0.15
-val elim_bonus = Unsynchronized.ref 0.15
-val simp_bonus = Unsynchronized.ref 0.15
-val local_bonus = Unsynchronized.ref 0.55
-val assum_bonus = Unsynchronized.ref 1.05
-val chained_bonus = Unsynchronized.ref 1.5
-
fun locality_bonus General = 0.0
| locality_bonus Intro = !intro_bonus
| locality_bonus Elim = !elim_bonus
@@ -388,19 +388,14 @@
fun pconsts_in_axiom thy t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
(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
+fun pair_consts_axiom thy axiom =
+ case axiom |> snd |> theory_const_prop_of |> pconsts_in_axiom thy of
[] => NONE
| consts => SOME ((axiom, consts), NONE)
type annotated_thm =
(((unit -> string) * locality) * thm) * (string * ptype) list
-(* FUDGE *)
-val max_imperfect = Unsynchronized.ref 11.5
-val max_imperfect_exp = Unsynchronized.ref 1.0
-
fun take_most_relevant max_relevant remaining_max
(candidates : (annotated_thm * real) list) =
let
@@ -431,16 +426,11 @@
else
tab
-(* FUDGE *)
-val threshold_divisor = Unsynchronized.ref 2.0
-val ridiculous_threshold = Unsynchronized.ref 0.1
-
-fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
+fun relevance_filter ctxt threshold0 decay max_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 const_tab = fold (count_axiom_consts thy) axioms Symtab.empty
val goal_const_tab =
pconsts_in_terms thy false (SOME false) goal_ts
|> fold (if_empty_replace_with_locality thy axioms)
@@ -533,7 +523,7 @@
end
in
axioms |> filter_out (member Thm.eq_thm del_thms o snd)
- |> map_filter (pair_consts_axiom theory_relevant thy)
+ |> map_filter (pair_consts_axiom thy)
|> iter 0 max_relevant threshold0 goal_const_tab []
|> tap (fn res => trace_msg (fn () =>
"Total relevant: " ^ Int.toString (length res)))
@@ -791,8 +781,8 @@
(***************************************************************)
fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
- theory_relevant (relevance_override as {add, del, only})
- chained_ths hyp_ts concl_t =
+ (relevance_override as {add, del, only}) chained_ths hyp_ts
+ concl_t =
let
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.0 / Real.fromInt (max_relevant + 1))
@@ -814,8 +804,8 @@
else if threshold0 < 0.0 then
axioms
else
- relevance_filter ctxt threshold0 decay max_relevant theory_relevant
- relevance_override axioms (concl_t :: hyp_ts))
+ relevance_filter ctxt threshold0 decay max_relevant relevance_override
+ axioms (concl_t :: hyp_ts))
|> map (apfst (apfst (fn f => f ())))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 01 17:27:10 2010 +0200
@@ -70,7 +70,6 @@
("explicit_apply", "false"),
("relevance_thresholds", "45 85"),
("max_relevant", "smart"),
- ("theory_relevant", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1")]
@@ -83,7 +82,6 @@
("no_overlord", "overlord"),
("partial_types", "full_types"),
("implicit_apply", "explicit_apply"),
- ("theory_irrelevant", "theory_relevant"),
("no_isar_proof", "isar_proof")]
val params_for_minimize =
@@ -180,7 +178,6 @@
lookup_int_pair "relevance_thresholds"
|> pairself (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")
val timeout = lookup_time "timeout"
@@ -189,9 +186,8 @@
{blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
atps = atps, full_types = full_types, explicit_apply = explicit_apply,
relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
- theory_relevant = theory_relevant, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, timeout = timeout,
- expect = expect}
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ timeout = timeout, expect = expect}
end
fun get_params thy = extract_params (default_raw_params thy)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Sep 01 16:46:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Sep 01 17:27:10 2010 +0200
@@ -53,8 +53,8 @@
{blocking = true, debug = debug, verbose = verbose, overlord = overlord,
atps = atps, full_types = full_types, explicit_apply = explicit_apply,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
- theory_relevant = NONE, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ timeout = timeout, expect = ""}
val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, facts, goal} = Proof.goal state
val problem =