--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Oct 21 14:55:09 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Oct 21 16:25:40 2010 +0200
@@ -199,19 +199,19 @@
\prew
\slshape
-Sledgehammer: Prover ``\textit{e}'' for subgoal 1: \\
+Sledgehammer: ``\textit{e}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis hd.simps}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{e}] (\textit{hd.simps}). \\[3\smallskipamount]
%
-Sledgehammer: Prover ``\textit{spass}'' for subgoal 1: \\
+Sledgehammer: ``\textit{spass}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis insert\_Nil last\_ConsL}). \\
To minimize the number of lemmas, try this: \\
\textbf{sledgehammer} \textit{minimize} [\textit{prover} = \textit{spass}] (\textit{insert\_Nil last\_ConsL}). \\[3\smallskipamount]
%
-Sledgehammer: Prover ``\textit{remote\_vampire}'' for subgoal 1: \\
+Sledgehammer: ``\textit{remote\_vampire}'' for subgoal 1: \\
$([a] = [b]) = (a = b)$ \\
Try this command: \textbf{by} (\textit{metis One\_nat\_def\_raw empty\_replicate} \\
\phantom{Try this command: \textbf{by} (\textit{metis~}}\textit{insert\_Nil last\_ConsL replicate\_Suc}). \\
@@ -220,6 +220,7 @@
\phantom{\textbf{sledgehammer}~}(\textit{One\_nat\_def\_raw empty\_replicate insert\_Nil} \\
\phantom{\textbf{sledgehammer}~(}\textit{last\_ConsL replicate\_Suc}).
\postw
+%%% TODO: Mention SInE-E
Sledgehammer ran E, SPASS, and the remote version of Vampire in parallel. If E
is not installed (\S\ref{installation}), you will see references to
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 21 16:25:40 2010 +0200
@@ -318,7 +318,7 @@
fun default_atp_name () =
hd (#provers (Sledgehammer_Isar.default_params thy []))
handle Empty => error "No ATP available."
- fun get_atp name = (name, Sledgehammer.get_atp_fun thy name)
+ fun get_atp name = (name, Sledgehammer.run_atp thy name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_atp name
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Oct 21 16:25:40 2010 +0200
@@ -25,7 +25,7 @@
val vampireN : string
val sine_eN : string
val snarkN : string
- val remote_atp_prefix : string
+ val remote_prefix : string
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val available_atps : theory -> string list
@@ -64,7 +64,7 @@
val vampireN = "vampire"
val sine_eN = "sine_e"
val snarkN = "snark"
-val remote_atp_prefix = "remote_"
+val remote_prefix = "remote_"
structure Data = Theory_Data
(
@@ -229,11 +229,11 @@
fun remote_atp name system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses =
- (remote_atp_prefix ^ name,
+ (remote_prefix ^ name,
remote_config system_name system_versions proof_delims known_failures
default_max_relevant use_conjecture_for_hypotheses)
fun remotify_atp (name, config) system_name system_versions =
- (remote_atp_prefix ^ name, remotify_config system_name system_versions config)
+ (remote_prefix ^ name, remotify_config system_name system_versions config)
val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"]
val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 21 16:25:40 2010 +0200
@@ -49,6 +49,7 @@
type atp = params -> minimize_command -> atp_problem -> atp_result
+ val smtN : string
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
@@ -56,7 +57,10 @@
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val get_atp_fun : theory -> string -> atp
+ val run_atp : theory -> string -> atp
+ val run_smt_solver :
+ Proof.context -> bool -> Time.time -> ('a * thm) list -> string * 'a list
+ val is_smt_solver_installed : unit -> bool
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -82,9 +86,18 @@
"Async_Manager". *)
val das_Tool = "Sledgehammer"
+val smtN = "smt"
+val smt_names = [smtN, remote_prefix ^ smtN]
+
fun available_provers thy =
- priority ("Available provers: " ^
- commas (sort_strings (available_atps thy)) ^ ".")
+ let
+ val (remote_provers, local_provers) =
+ sort_strings (available_atps thy) @ smt_names
+ |> List.partition (String.isPrefix remote_prefix)
+ in
+ priority ("Available provers: " ^ commas (local_provers @ remote_provers) ^
+ ".")
+ end
fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
fun running_provers () = Async_Manager.running_threads das_Tool "provers"
@@ -145,6 +158,22 @@
|> Exn.release
|> tap (after path)
+fun prover_description ctxt ({blocking, verbose, ...} : params) name num_axioms
+ i n goal =
+ quote name ^
+ (if verbose then
+ " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
+ else
+ "") ^
+ " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
+ (if blocking then
+ ""
+ else
+ "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+
+fun proof_banner auto =
+ if auto then "Sledgehammer found a proof" else "Try this command"
+
(* generic TPTP-based ATPs *)
(* Important messages are important but not so important that users want to see
@@ -268,15 +297,13 @@
extract_important_message output
else
""
- val banner = if auto then "Sledgehammer found a proof"
- else "Try this command"
val (message, used_thm_names) =
case outcome of
NONE =>
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (banner, full_types, minimize_command, tstplike_proof, axiom_names,
- goal, subgoal)
+ (proof_banner auto, full_types, minimize_command, tstplike_proof,
+ axiom_names, goal, subgoal)
|>> (fn message =>
message ^ (if verbose then
"\nATP real CPU time: " ^ string_of_int msecs ^
@@ -296,30 +323,20 @@
axiom_names = axiom_names, conjecture_shape = conjecture_shape}
end
-fun get_atp_fun thy name = atp_fun false name (get_atp thy name)
+fun run_atp thy name = atp_fun false name (get_atp thy name)
-fun run_atp (params as {blocking, debug, verbose, max_relevant, timeout, expect,
- ...})
- auto i n minimize_command
- (atp_problem as {state, goal, axioms, ...})
- (atp as {default_max_relevant, ...}, atp_name) =
+fun run_atp_somehow (params as {blocking, debug, max_relevant, timeout,
+ expect, ...})
+ auto i n minimize_command
+ (atp_problem as {state, goal, axioms, ...})
+ (atp as {default_max_relevant, ...}, atp_name) =
let
val ctxt = Proof.context_of state
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
val max_relevant = the_default default_max_relevant max_relevant
val num_axioms = Int.min (length axioms, max_relevant)
- val desc =
- "ATP " ^ quote atp_name ^
- (if verbose then
- " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
- else
- "") ^
- " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
- (if blocking then
- ""
- else
- "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+ val desc = prover_description ctxt params atp_name num_axioms i n goal
fun go () =
let
fun really_go () =
@@ -361,10 +378,36 @@
(false, state))
end
-val auto_max_relevant_divisor = 2
+(* FIXME: dummy *)
+fun run_smt_solver ctxt remote timeout axioms =
+ ("", axioms |> take 5 |> map fst)
+
+(* FIXME: dummy *)
+fun is_smt_solver_installed () = true
+
+fun run_smt_solver_somehow ctxt (params as {timeout, ...}) i n goal axioms
+ (remote, name) =
+ let
+ val desc =
+ prover_description ctxt params name (length axioms) i n goal
+ val (failure, used_thm_names) = run_smt_solver ctxt remote timeout axioms
+ val success = (failure = "")
+ val message =
+ das_Tool ^ ": " ^ desc ^ "\n" ^
+ (if success then
+ sendback_line (proof_banner false)
+ (apply_on_subgoal i n ^
+ command_call "smt" (map fst used_thm_names))
+ else
+ "Error: " ^ failure)
+ in priority message; success end
+
+val smt_default_max_relevant = 300 (* FUDGE *)
+val auto_max_relevant_divisor = 2 (* FUDGE *)
fun run_sledgehammer (params as {blocking, provers, full_types,
- relevance_thresholds, max_relevant, ...})
+ relevance_thresholds, max_relevant, timeout,
+ ...})
auto i (relevance_override as {only, ...}) minimize_command
state =
if null provers then
@@ -375,37 +418,67 @@
let
val _ = Proof.assert_backward state
val thy = Proof.theory_of state
+ val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i
val _ = () |> not blocking ? kill_provers
val _ = if auto then () else priority "Sledgehammering..."
- val atps = map (`(get_atp thy)) provers
- fun go () =
- let
- val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val max_max_relevant =
- case max_relevant of
- SOME n => n
- | NONE =>
- 0 |> fold (Integer.max o #default_max_relevant o fst) atps
- |> auto ? (fn n => n div auto_max_relevant_divisor)
- val axioms =
- relevant_facts ctxt full_types relevance_thresholds
- max_max_relevant relevance_override chained_ths
- hyp_ts concl_t
- val atp_problem =
- {state = state, goal = goal, subgoal = i,
- axioms = map (prepare_axiom ctxt) axioms, only = only}
- val run_atp = run_atp params auto i n minimize_command atp_problem
- in
- if auto then
- fold (fn atp => fn (true, state) => (true, state)
- | (false, _) => run_atp atp)
- atps (false, state)
- else
- (if blocking then Par_List.map else map) run_atp atps
- |> exists fst |> rpair state
- end
- in if blocking then go () else Future.fork (tap go) |> K (false, state) end
+ val (smts, atps) =
+ provers |> List.partition (member (op =) smt_names)
+ |>> (take 1 #> map (`(String.isPrefix remote_prefix)))
+ ||> map (`(get_atp thy))
+ fun run_atps (res as (success, state)) =
+ if success orelse null atps then
+ res
+ else
+ let
+ val max_max_relevant =
+ case max_relevant of
+ SOME n => n
+ | NONE =>
+ 0 |> fold (Integer.max o #default_max_relevant o fst) atps
+ |> auto ? (fn n => n div auto_max_relevant_divisor)
+ val axioms =
+ relevant_facts ctxt full_types relevance_thresholds
+ max_max_relevant relevance_override chained_ths
+ hyp_ts concl_t
+ val atp_problem =
+ {state = state, goal = goal, subgoal = i,
+ axioms = map (prepare_axiom ctxt) axioms, only = only}
+ val run_atp_somehow =
+ run_atp_somehow params auto i n minimize_command atp_problem
+ in
+ if auto then
+ fold (fn atp => fn (true, state) => (true, state)
+ | (false, _) => run_atp_somehow atp)
+ atps (false, state)
+ else
+ atps |> (if blocking then Par_List.map else map) run_atp_somehow
+ |> exists fst |> rpair state
+ end
+ fun run_smt_solvers (res as (success, state)) =
+ if success orelse null smts then
+ res
+ else
+ let
+ val max_relevant =
+ max_relevant |> the_default smt_default_max_relevant
+ val axioms =
+ relevant_facts ctxt full_types relevance_thresholds
+ max_relevant relevance_override chained_ths
+ hyp_ts concl_t
+ in
+ smts |> map (run_smt_solver_somehow ctxt params i n goal axioms)
+ |> exists I |> rpair state
+ end
+ fun run_atps_and_smt_solvers () =
+ [run_atps, run_smt_solvers]
+ |> Par_List.map (fn f => f (false, state) |> K ())
+ in
+ if blocking then
+ (false, state) |> run_atps |> not auto ? run_smt_solvers
+ else
+ Future.fork (tap run_atps_and_smt_solvers) |> K (false, state)
+ end
val setup =
dest_dir_setup
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 21 16:25:40 2010 +0200
@@ -131,18 +131,19 @@
fun merge p : T = AList.merge (op =) (K true) p)
fun maybe_remote_atp thy name =
- name |> not (is_atp_installed thy name) ? prefix remote_atp_prefix
+ name |> not (is_atp_installed thy name) ? prefix remote_prefix
+fun maybe_remote_smt_solver thy =
+ smtN |> not (is_smt_solver_installed ()) ? prefix remote_prefix
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value thy =
(filter (is_atp_installed thy) [spassN] @
[maybe_remote_atp thy eN,
- if forall (is_atp_installed thy) [spassN, eN] then
- remote_atp_prefix ^ vampireN
- else
- maybe_remote_atp thy vampireN,
- remote_atp_prefix ^ sine_eN])
+ if forall (is_atp_installed thy) [spassN, eN] then remote_prefix ^ vampireN
+ else maybe_remote_atp thy vampireN,
+ remote_prefix ^ sine_eN,
+ maybe_remote_smt_solver thy])
|> space_implode " "
val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 21 16:25:40 2010 +0200
@@ -96,7 +96,7 @@
i (_ : int) state axioms =
let
val thy = Proof.theory_of state
- val atp = get_atp_fun thy prover
+ val atp = run_atp thy prover
val msecs = Time.toMilliseconds timeout
val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".")
val {context = ctxt, goal, ...} = Proof.goal state
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 21 14:55:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Oct 21 16:25:40 2010 +0200
@@ -20,6 +20,9 @@
val repair_conjecture_shape_and_axiom_names :
string -> int list list -> (string * locality) list vector
-> int list list * (string * locality) list vector
+ val apply_on_subgoal : int -> int -> string
+ val command_call : string -> string list -> string
+ val sendback_line : string -> string -> string
val metis_proof_text : metis_params -> text_result
val isar_proof_text : isar_params -> metis_params -> text_result
val proof_text : bool -> isar_params -> metis_params -> text_result
@@ -111,21 +114,22 @@
fun string_for_label (s, num) = s ^ string_of_int num
-fun metis_using [] = ""
- | metis_using ls =
+fun apply_on_subgoal _ 1 = "by "
+ | apply_on_subgoal 1 _ = "apply "
+ | apply_on_subgoal i _ = "prefer " ^ string_of_int i ^ " apply "
+fun command_call name [] = name
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+fun sendback_line banner command =
+ banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
+fun using_labels [] = ""
+ | using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_apply _ 1 = "by "
- | metis_apply 1 _ = "apply "
- | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply "
fun metis_name full_types = if full_types then "metisFT" else "metis"
-fun metis_call full_types [] = metis_name full_types
- | metis_call full_types ss =
- "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")"
+fun metis_call full_types ss = command_call (metis_name full_types) ss
fun metis_command full_types i n (ls, ss) =
- metis_using ls ^ metis_apply i n ^ metis_call full_types ss
+ using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
fun metis_line banner full_types i n ss =
- banner ^ ": " ^
- Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
+ sendback_line banner (metis_command full_types i n ([], ss))
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of