--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 12:49:43 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 13:10:58 2010 +0200
@@ -8,9 +8,7 @@
signature ATP_SYSTEMS =
sig
datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
@@ -39,9 +37,9 @@
(* prover configuration *)
datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+ MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
@@ -72,6 +70,10 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
" on a line of its own."
+ | string_for_failure OldVampire =
+ "Isabelle requires a more recent version of Vampire. To install it, follow \
+ \the instructions from the Sledgehammer manual (\"isabelle doc\
+ \ sledgehammer\")."
| string_for_failure NoPerl = "Perl" ^ missing_message_tail
| string_for_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
@@ -143,6 +145,7 @@
max_new_relevant_facts_per_iter = 60 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
+
val e = ("e", e_config)
@@ -169,8 +172,10 @@
max_new_relevant_facts_per_iter = 35 (* FIXME *),
prefers_theory_relevant = true,
explicit_forall = true}
+
val spass = ("spass", spass_config)
+
(* Vampire *)
val vampire_config : prover_config =
@@ -189,12 +194,15 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
- (OutOfResources, "Refutation not found")],
+ (OutOfResources, "Refutation not found"),
+ (OldVampire, "input_file")],
max_new_relevant_facts_per_iter = 50 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
+
val vampire = ("vampire", vampire_config)
+
(* Remote prover invocation via SystemOnTPTP *)
val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -236,13 +244,15 @@
explicit_forall = true}
val remote_name = prefix "remote_"
-
fun remote_prover (name, config) atp_prefix =
(remote_name name, remote_config atp_prefix config)
val remote_e = remote_prover e "EP---"
val remote_vampire = remote_prover vampire "Vampire---9"
+
+(* Setup *)
+
fun is_installed ({exec, required_execs, ...} : prover_config) =
forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
fun maybe_remote (name, config) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 17 12:49:43 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 17 13:10:58 2010 +0200
@@ -206,27 +206,37 @@
(* generic TPTP-based provers *)
-fun prover_fun name
+fun prover_fun atp_name
{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, timeout, ...} : params)
+ ({debug, verbose, overlord, full_types, explicit_apply,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
minimize_command
({subgoal, goal, 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
+
+ fun print s = (priority s; if debug then tracing s else ())
+ fun print_v f = () |> verbose ? print o f
+ fun print_d f = () |> debug ? print o f
+
val the_axioms =
case axioms of
SOME axioms => axioms
- | NONE => relevant_facts full_types relevance_threshold
- relevance_convergence defs_relevant
- max_new_relevant_facts_per_iter
- (the_default prefers_theory_relevant theory_relevant)
- relevance_override goal hyp_ts concl_t
+ | NONE =>
+ (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)
+ relevance_override goal 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))
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -235,7 +245,7 @@
fun prob_pathname nr =
let
val probfile =
- Path.basic ((if overlord then "prob_" ^ name
+ Path.basic ((if overlord then "prob_" ^ atp_name
else the_problem_prefix ^ serial_string ())
^ "_" ^ string_of_int nr)
in
@@ -290,6 +300,8 @@
extract_proof_and_outcome complete res_code proof_delims
known_failures output
in (output, msecs, proof, outcome) end
+ val _ = print_d (fn () => "Preparing problem for " ^
+ quote atp_name ^ "...")
val readable_names = debug andalso overlord
val (problem, pool, conjecture_offset, axiom_names) =
prepare_problem ctxt readable_names explicit_forall full_types
@@ -298,6 +310,7 @@
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
+ val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
val result =
do_run false
|> (fn (_, msecs0, _, SOME _) =>
@@ -343,15 +356,16 @@
fun get_prover_fun thy name = prover_fun name (get_prover thy name)
fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
- relevance_override minimize_command proof_state name =
+ relevance_override minimize_command proof_state
+ atp_name =
let
val thy = Proof.theory_of proof_state
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
- val prover = get_prover_fun thy name
+ val prover = get_prover_fun thy atp_name
val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
- "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+ "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
in
Async_Manager.launch das_Tool verbose birth_time death_time desc
@@ -361,7 +375,7 @@
{subgoal = i, goal = (ctxt, (facts, goal)),
relevance_override = relevance_override, axioms = NONE}
in
- prover params (minimize_command name) problem |> #message
+ prover params (minimize_command atp_name) problem |> #message
handle ERROR message => "Error: " ^ message ^ "\n"
| exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^
"\n"
--- a/src/Provers/quantifier1.ML Tue Aug 17 12:49:43 2010 +0200
+++ b/src/Provers/quantifier1.ML Tue Aug 17 13:10:58 2010 +0200
@@ -17,7 +17,7 @@
And analogously for t=x, but the eqn is not turned around!
NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)";
- "!x. x=t --> P(x)" is covered by the congreunce rule for -->;
+ "!x. x=t --> P(x)" is covered by the congruence rule for -->;
"!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule.
As must be "? x. t=x & P(x)".
@@ -26,7 +26,7 @@
Gries etc call this the "1 point rules"
The above also works for !x1..xn. and ?x1..xn by moving the defined
-qunatifier inside first, but not for nested bounded quantifiers.
+quantifier inside first, but not for nested bounded quantifiers.
For set comprehensions the basic permutations
... & x = t & ... -> x = t & (... & ...)