--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 16:42:37 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 17:09:05 2010 +0200
@@ -18,8 +18,8 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
+ default_max_relevant_per_iter: int,
+ default_theory_relevant: bool,
explicit_forall: bool}
val string_for_failure : failure -> string
@@ -49,8 +49,8 @@
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
- max_new_relevant_facts_per_iter: int,
- prefers_theory_relevant: bool,
+ default_max_relevant_per_iter: int,
+ default_theory_relevant: bool,
explicit_forall: bool}
val missing_message_tail =
@@ -144,8 +144,8 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 50 (* FIXME *),
- prefers_theory_relevant = false,
+ default_max_relevant_per_iter = 50 (* FIXME *),
+ default_theory_relevant = false,
explicit_forall = false}
val e = ("e", e_config)
@@ -171,8 +171,8 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- max_new_relevant_facts_per_iter = 35 (* FIXME *),
- prefers_theory_relevant = true,
+ default_max_relevant_per_iter = 35 (* FIXME *),
+ default_theory_relevant = true,
explicit_forall = true}
val spass = ("spass", spass_config)
@@ -198,8 +198,8 @@
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found"),
(VampireTooOld, "not a valid option")],
- max_new_relevant_facts_per_iter = 45 (* FIXME *),
- prefers_theory_relevant = false,
+ default_max_relevant_per_iter = 45 (* FIXME *),
+ default_theory_relevant = false,
explicit_forall = false}
val vampire = ("vampire", vampire_config)
@@ -220,9 +220,10 @@
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
-fun get_system prefix = Synchronized.change_result systems (fn systems =>
- (if null systems then get_systems () else systems)
- |> `(find_first (String.isPrefix prefix)));
+fun get_system prefix =
+ Synchronized.change_result systems
+ (fn systems => (if null systems then get_systems () else systems)
+ |> `(find_first (String.isPrefix prefix)))
fun the_system prefix =
(case get_system prefix of
@@ -230,8 +231,8 @@
| SOME sys => sys);
fun remote_config atp_prefix
- ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
- prefers_theory_relevant, ...} : prover_config) : prover_config =
+ ({proof_delims, known_failures, default_max_relevant_per_iter,
+ default_theory_relevant, ...} : prover_config) : prover_config =
{exec = ("ISABELLE_ATP", "scripts/remote_atp"),
required_execs = [],
arguments = fn _ => fn timeout =>
@@ -241,8 +242,8 @@
known_failures =
known_failures @ known_perl_failures @
[(TimedOut, "says Timeout")],
- max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
- prefers_theory_relevant = prefers_theory_relevant,
+ default_max_relevant_per_iter = default_max_relevant_per_iter,
+ default_theory_relevant = default_theory_relevant,
explicit_forall = true}
val remote_name = prefix "remote_"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 16:42:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 17:09:05 2010 +0200
@@ -20,6 +20,7 @@
explicit_apply: bool,
relevance_threshold: real,
relevance_convergence: real,
+ max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
@@ -89,6 +90,7 @@
explicit_apply: bool,
relevance_threshold: real,
relevance_convergence: real,
+ max_relevant_per_iter: int option,
theory_relevant: bool option,
defs_relevant: bool,
isar_proof: bool,
@@ -208,10 +210,11 @@
fun prover_fun atp_name
{exec, required_execs, arguments, proof_delims, known_failures,
- max_new_relevant_facts_per_iter, prefers_theory_relevant,
+ default_max_relevant_per_iter, default_theory_relevant,
explicit_forall}
({debug, verbose, overlord, full_types, explicit_apply,
- relevance_threshold, relevance_convergence, theory_relevant,
+ relevance_threshold, relevance_convergence,
+ max_relevant_per_iter, theory_relevant,
defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, relevance_override, axioms} : problem) =
@@ -231,8 +234,10 @@
(print_d (fn () => "Selecting relevant facts for " ^ quote atp_name ^
".");
relevant_facts full_types relevance_threshold relevance_convergence
- defs_relevant max_new_relevant_facts_per_iter
- (the_default prefers_theory_relevant theory_relevant)
+ defs_relevant
+ (the_default default_max_relevant_per_iter
+ max_relevant_per_iter)
+ (the_default default_theory_relevant theory_relevant)
relevance_override goal 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_fact_minimize.ML Wed Aug 18 16:42:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 18 17:09:05 2010 +0200
@@ -43,9 +43,9 @@
end
fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- ...} : params)
+ relevance_threshold, relevance_convergence,
+ defs_relevant, isar_proof, isar_shrink_factor, ...}
+ : params)
(prover : prover) explicit_apply timeout subgoal state
name_thms_pairs =
let
@@ -56,9 +56,10 @@
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
- theory_relevant = theory_relevant, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout, minimize_timeout = timeout}
+ max_relevant_per_iter = NONE, theory_relevant = NONE,
+ defs_relevant = defs_relevant, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout,
+ minimize_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 =
@@ -98,10 +99,8 @@
fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
| minimize_theorems
- (params as {debug, verbose, overlord, atps as atp :: _, full_types,
- relevance_threshold, relevance_convergence, theory_relevant,
- defs_relevant, isar_proof, isar_shrink_factor,
- minimize_timeout, ...})
+ (params as {debug, atps = atp :: _, full_types, isar_proof,
+ isar_shrink_factor, minimize_timeout, ...})
i n state name_thms_pairs =
let
val thy = Proof.theory_of state
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 18 16:42:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 18 17:09:05 2010 +0200
@@ -69,6 +69,7 @@
("explicit_apply", "false"),
("relevance_threshold", "50"),
("relevance_convergence", "320"),
+ ("max_relevant_per_iter", "smart"),
("theory_relevant", "smart"),
("defs_relevant", "false"),
("isar_proof", "false"),
@@ -158,6 +159,10 @@
SOME n => n
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value.")
+ fun lookup_int_option name =
+ case lookup name of
+ SOME "smart" => NONE
+ | _ => SOME (lookup_int name)
val debug = lookup_bool "debug"
val verbose = debug orelse lookup_bool "verbose"
val overlord = lookup_bool "overlord"
@@ -168,6 +173,7 @@
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_convergence =
0.01 * Real.fromInt (lookup_int "relevance_convergence")
+ 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"
@@ -179,6 +185,7 @@
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_convergence = relevance_convergence,
+ 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, minimize_timeout = minimize_timeout}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 16:42:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 17:09:05 2010 +0200
@@ -420,8 +420,8 @@
type instantiations). If false, the constant always receives all of its
arguments and is used as a predicate. *)
fun is_predicate NONE s =
- s = "equal" orelse String.isPrefix type_const_prefix s orelse
- String.isPrefix class_prefix s
+ s = "equal" orelse s = "$false" orelse s = "$true" orelse
+ String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
| is_predicate (SOME the_const_tab) s =
case Symtab.lookup the_const_tab s of
SOME {min_arity, max_arity, sub_level} =>