speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 17:45:22 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 18:45:41 2010 +0200
@@ -13,8 +13,8 @@
MalformedOutput | UnknownError
type prover_config =
- {executable: string * string,
- required_executables: (string * string) list,
+ {exec: string * string,
+ required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -44,8 +44,8 @@
MalformedOutput | UnknownError
type prover_config =
- {executable: string * string,
- required_executables: (string * string) list,
+ {exec: string * string,
+ required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -124,8 +124,8 @@
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
val e_config : prover_config =
- {executable = ("E_HOME", "eproof"),
- required_executables = [],
+ {exec = ("E_HOME", "eproof"),
+ required_execs = [],
arguments = fn _ => fn timeout =>
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
string_of_int (to_generous_secs timeout),
@@ -148,8 +148,8 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
- {executable = ("ISABELLE_ATP", "scripts/spass"),
- required_executables = [("SPASS_HOME", "SPASS")],
+ {exec = ("ISABELLE_ATP", "scripts/spass"),
+ required_execs = [("SPASS_HOME", "SPASS")],
(* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
@@ -173,8 +173,8 @@
(* Vampire *)
val vampire_config : prover_config =
- {executable = ("VAMPIRE_HOME", "vampire"),
- required_executables = [],
+ {exec = ("VAMPIRE_HOME", "vampire"),
+ required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
" --input_file ",
@@ -186,6 +186,7 @@
known_failures =
[(Unprovable, "UNPROVABLE"),
(IncompleteUnprovable, "CANNOT PROVE"),
+ (TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found")],
max_new_relevant_facts_per_iter = 50 (* FIXME *),
@@ -221,8 +222,8 @@
({proof_delims, known_failures, max_new_relevant_facts_per_iter,
prefers_theory_relevant, explicit_forall, ...} : prover_config)
: prover_config =
- {executable = ("ISABELLE_ATP", "scripts/remote_atp"),
- required_executables = [],
+ {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
+ required_execs = [],
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system atp_prefix,
@@ -243,8 +244,8 @@
val remote_e = remote_prover e "EP---"
val remote_vampire = remote_prover vampire "Vampire---9"
-fun is_installed ({executable, required_executables, ...} : prover_config) =
- forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
+fun is_installed ({exec, required_execs, ...} : prover_config) =
+ forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
fun maybe_remote (name, config) =
name |> not (is_installed config) ? remote_name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 17:45:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 18:45:41 2010 +0200
@@ -672,9 +672,9 @@
(* generic TPTP-based provers *)
fun prover_fun name
- {executable, required_executables, arguments, proof_delims,
- known_failures, max_new_relevant_facts_per_iter,
- prefers_theory_relevant, explicit_forall}
+ {exec, required_execs, arguments, proof_delims, known_failures,
+ max_new_relevant_facts_per_iter, prefers_theory_relevant,
+ explicit_forall}
({debug, overlord, full_types, explicit_apply, relevance_threshold,
relevance_convergence, theory_relevant, defs_relevant, isar_proof,
isar_shrink_factor, ...} : params)
@@ -713,7 +713,7 @@
else error ("No such directory: " ^ the_dest_dir ^ ".")
end;
- val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)
+ val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
(* write out problem file and call prover *)
fun command_line complete probfile =
let
@@ -737,8 +737,7 @@
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
in (output, as_time t) end;
fun run_on probfile =
- case filter (curry (op =) "" o getenv o fst)
- (executable :: required_executables) of
+ case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
(home_var, _) :: _ =>
error ("The environment variable " ^ quote home_var ^ " is not set.")
| [] =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 17:45:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 18:45:41 2010 +0200
@@ -18,6 +18,7 @@
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
struct
+open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -26,38 +27,40 @@
(* wrapper for calling external prover *)
fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure IncompleteUnprovable = "Failed."
| string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "Failed."
- | string_for_failure OldSpass = "Error."
- | string_for_failure MalformedOutput = "Error."
- | string_for_failure UnknownError = "Failed."
-fun string_for_outcome NONE = "Success."
- | string_for_outcome (SOME failure) = string_for_failure failure
+ | string_for_failure _ = "Unknown error."
-fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
- name_thms_pairs =
+fun n_theorems name_thms_pairs =
+ let val n = length name_thms_pairs in
+ string_of_int n ^ " theorem" ^ plural_s n ^
+ (if n > 0 then
+ ": " ^ space_implode " " (sort_distinct string_ord name_thms_pairs)
+ else
+ "")
+ end
+
+fun sledgehammer_test_theorems (params : params) (prover : prover) timeout
+ subgoal state name_thms_pairs =
let
- val num_axioms = length name_thms_pairs
val _ =
- priority ("Testing " ^ string_of_int num_axioms ^
- " theorem" ^ plural_s num_axioms ^
- (if num_axioms > 0 then
- ": " ^ space_implode " "
- (name_thms_pairs
- |> map fst |> sort_distinct string_ord)
- else
- "") ^ "...")
+ priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
relevance_override = {add = [], del = [], only = false},
axioms = SOME axioms}
+ val result as {outcome, used_thm_names, ...} =
+ prover params (K "") timeout problem
in
- prover params (K "") timeout problem
- |> tap (fn result : prover_result =>
- priority (string_for_outcome (#outcome result)))
+ priority (case outcome of
+ NONE =>
+ if length used_thm_names = length name_thms_pairs then
+ "Found proof."
+ else
+ "Found proof with " ^ n_theorems used_thm_names ^ "."
+ | SOME failure => string_for_failure failure);
+ result
end
(* minimalization of thms *)
@@ -73,29 +76,40 @@
(filter_used_facts used_thm_names seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
-fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
- isar_proof, isar_shrink_factor, ...})
- i n state name_thms_pairs =
+(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
+ preprocessing time is included in the estimate below but isn't part of the
+ timeout. *)
+val fudge_msecs = 250
+
+fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
+ | minimize_theorems
+ (params as {debug, verbose, overlord, atps as atp :: _, full_types,
+ explicit_apply, relevance_threshold, relevance_convergence,
+ theory_relevant, defs_relevant, isar_proof,
+ isar_shrink_factor, minimize_timeout, ...})
+ i n state name_thms_pairs =
let
val thy = Proof.theory_of state
- val prover = case atps of
- [atp_name] => get_prover_fun thy atp_name
- | _ => error "Expected a single ATP."
+ val prover = get_prover_fun thy atp
val msecs = Time.toMilliseconds minimize_timeout
val _ =
- priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
+ priority ("Sledgehammer minimizer: ATP " ^ quote atp ^
" with a time limit of " ^ string_of_int msecs ^ " ms.")
- val test_facts =
- sledgehammer_test_theorems params prover minimize_timeout i state
- val {context = ctxt, goal, ...} = Proof.goal state;
+ fun test_facts timeout =
+ sledgehammer_test_theorems params prover timeout i state
+ val {context = ctxt, goal, ...} = Proof.goal state
+ val timer = Timer.startRealTimer ()
in
- (* FIXME: merge both "test_facts" calls *)
- (case test_facts name_thms_pairs of
+ (case test_facts minimize_timeout name_thms_pairs of
result as {outcome = NONE, pool, used_thm_names,
conjecture_shape, ...} =>
let
+ val time = Timer.checkRealTimer timer
+ val new_timeout =
+ Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
+ |> Time.fromMilliseconds
val (min_thms, {proof, internal_thm_names, ...}) =
- sublinear_minimize test_facts
+ sublinear_minimize (test_facts new_timeout)
(filter_used_facts used_thm_names name_thms_pairs) ([], result)
val m = length min_thms
val _ = priority (cat_lines