# HG changeset patch # User blanchet # Date 1282043458 -7200 # Node ID b8760b6e7c65b8a00f5a3d9366fd4975ba13fc94 # Parent 6e7f8121b4f73cd74afd26c5c30a77ba00d82599# Parent 6769ccd90ad6ca7eccc65dd70c1a0f6e7190b845 merged diff -r 6e7f8121b4f7 -r b8760b6e7c65 src/HOL/Tools/ATP/atp_systems.ML --- 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) = diff -r 6e7f8121b4f7 -r b8760b6e7c65 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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" diff -r 6e7f8121b4f7 -r b8760b6e7c65 src/Provers/quantifier1.ML --- 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 & (... & ...)