--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Dec 17 22:23:56 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Dec 17 23:18:39 2010 +0100
@@ -15,7 +15,7 @@
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
NoRealZ3 | MalformedInput | MalformedOutput | Interrupted | Crashed |
- InternalError | UnknownError
+ InternalError | UnknownError of string
type step_name = string * string option
@@ -26,13 +26,14 @@
type 'a proof = 'a uniform_formula step list
val strip_spaces : (char -> bool) -> string -> string
+ val short_output : bool -> string -> string
val string_for_failure : string -> failure -> string
val extract_important_message : string -> string
val extract_known_failure :
(failure * string) list -> string -> failure option
val extract_tstplike_proof_and_outcome :
- bool -> int -> (string * string) list -> (failure * string) list -> string
- -> string * failure option
+ bool -> bool -> int -> (string * string) list -> (failure * string) list
+ -> string -> string * failure option
val is_same_step : step_name * step_name -> bool
val atp_proof_from_tstplike_string : bool -> string -> string proof
val map_term_names_in_atp_proof :
@@ -49,7 +50,7 @@
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | NoRealZ3 |
MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError |
- UnknownError
+ UnknownError of string
fun strip_spaces_in_list _ [] = []
| strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -72,6 +73,15 @@
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
+fun elide_string threshold s =
+ if size s > threshold then
+ String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
+ String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
+ else
+ s
+fun short_output verbose output =
+ if verbose then elide_string 1000 output else ""
+
fun missing_message_tail prover =
" appears to be missing. You will need to install it if you want to run " ^
prover ^ "s remotely."
@@ -112,9 +122,10 @@
| string_for_failure prover Crashed = "The " ^ prover ^ " crashed."
| string_for_failure prover InternalError =
"An internal " ^ prover ^ " error occurred."
- | string_for_failure prover UnknownError =
+ | string_for_failure prover (UnknownError string) =
(* "An" is correct for "ATP" and "SMT". *)
- "An " ^ prover ^ " error occurred."
+ "An " ^ prover ^ " error occurred" ^
+ (if string = "" then "." else ":\n" ^ string)
fun extract_delimited (begin_delim, end_delim) output =
output |> first_field begin_delim |> the |> snd
@@ -146,16 +157,17 @@
|> find_first (fn (_, pattern) => String.isSubstring pattern output)
|> Option.map fst
-fun extract_tstplike_proof_and_outcome complete res_code proof_delims
+fun extract_tstplike_proof_and_outcome verbose complete res_code proof_delims
known_failures output =
case extract_known_failure known_failures output of
NONE => (case extract_tstplike_proof proof_delims output of
"" => ("", SOME (if res_code = 0 andalso output = "" then
Interrupted
else
- UnknownError))
- | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
- else ("", SOME UnknownError))
+ UnknownError (short_output verbose output)))
+ | tstplike_proof =>
+ if res_code = 0 then (tstplike_proof, NONE)
+ else ("", SOME (UnknownError (short_output verbose output))))
| SOME failure =>
("", SOME (if failure = IncompleteUnprovable andalso complete then
Unprovable
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 17 22:23:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 17 23:18:39 2010 +0100
@@ -111,9 +111,15 @@
AList.defined (op =) negated_alias_params s orelse
member (op =) property_dependent_params s orelse s = "expect"
-fun check_raw_param (s, _) =
- if is_known_raw_param s then ()
- else error ("Unknown parameter: " ^ quote s ^ ".")
+fun is_prover_list ctxt s =
+ case space_explode " " s of
+ ss as _ :: _ => forall (is_prover_available ctxt) ss
+ | _ => false
+
+fun check_and_repair_raw_param ctxt (name, value) =
+ if is_known_raw_param name then (name, value)
+ else if is_prover_list ctxt name andalso null value then ("provers", [name])
+ else error ("Unknown parameter: " ^ quote name ^ ".")
fun unalias_raw_param (name, value) =
case AList.lookup (op =) alias_params name of
@@ -282,7 +288,8 @@
fun hammer_away override_params subcommand opt_i relevance_override state =
let
val ctxt = Proof.context_of state
- val _ = app check_raw_param override_params
+ val override_params =
+ override_params |> map (check_and_repair_raw_param ctxt)
in
if subcommand = runN then
let val i = the_default 1 opt_i in
@@ -323,9 +330,9 @@
(case default_raw_params ctxt |> rev of
[] => "none"
| params =>
- (map check_raw_param params;
- params |> map string_for_raw_param
- |> sort_strings |> cat_lines)))
+ params |> map (check_and_repair_raw_param ctxt)
+ |> map string_for_raw_param
+ |> sort_strings |> cat_lines))
end))
val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 22:23:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Dec 17 23:18:39 2010 +0100
@@ -10,9 +10,7 @@
type locality = Sledgehammer_Filter.locality
type params = Sledgehammer_Provers.params
- val filter_used_facts :
- (string * locality) list -> ((string * locality) * thm list) list
- -> ((string * locality) * thm list) list
+ val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
val minimize_facts :
params -> bool -> int -> int -> Proof.state
-> ((string * locality) * thm list) list
@@ -169,7 +167,7 @@
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
string_of_int (10 + msecs div 1000) ^ "\").")
- | {outcome = SOME UnknownError, ...} =>
+ | {outcome = SOME (UnknownError _), ...} =>
(* Failure sometimes mean timeout, unfortunately. *)
(NONE, "Failure: No proof was found with the current time limit. You \
\can increase the time limit using the \"timeout\" \
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 22:23:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 17 23:18:39 2010 +0100
@@ -53,6 +53,12 @@
type prover = params -> minimize_command -> prover_problem -> prover_result
(* for experimentation purposes -- do not use in production code *)
+ val smt_weights : bool Unsynchronized.ref
+ val smt_weight_min_facts : int Unsynchronized.ref
+ val smt_min_weight : int Unsynchronized.ref
+ val smt_max_weight : int Unsynchronized.ref
+ val smt_max_weight_index : int Unsynchronized.ref
+ val smt_weight_curve : (int -> int) Unsynchronized.ref
val smt_max_iters : int Unsynchronized.ref
val smt_iter_fact_frac : real Unsynchronized.ref
val smt_iter_time_frac : real Unsynchronized.ref
@@ -73,9 +79,13 @@
val dest_dir : string Config.T
val problem_prefix : string Config.T
val measure_run_time : bool Config.T
+ val weight_smt_fact :
+ theory -> int -> ((string * locality) * thm) * int
+ -> (string * locality) * (int option * thm)
val untranslated_fact : prover_fact -> (string * locality) * thm
val smt_weighted_fact :
- prover_fact -> (string * locality) * (int option * thm)
+ theory -> int -> prover_fact * int
+ -> (string * locality) * (int option * thm)
val available_provers : Proof.context -> unit
val kill_provers : unit -> unit
val running_provers : unit -> unit
@@ -277,7 +287,26 @@
fun proof_banner auto =
if auto then "Auto Sledgehammer found a proof" else "Try this command"
-(* generic TPTP-based ATPs *)
+val smt_weights = Unsynchronized.ref true
+val smt_weight_min_facts = Unsynchronized.ref 20
+
+(* FUDGE *)
+val smt_min_weight = Unsynchronized.ref 0
+val smt_max_weight = Unsynchronized.ref 10
+val smt_max_weight_index = Unsynchronized.ref 200
+val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
+
+fun smt_fact_weight j num_facts =
+ if !smt_weights andalso num_facts >= !smt_weight_min_facts then
+ SOME (!smt_max_weight
+ - (!smt_max_weight - !smt_min_weight + 1)
+ * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
+ div !smt_weight_curve (!smt_max_weight_index))
+ else
+ NONE
+
+fun weight_smt_fact thy num_facts ((info, th), j) =
+ (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
fun untranslated_fact (Untranslated_Fact p) = p
| untranslated_fact (ATP_Translated_Fact (_, p)) = p
@@ -285,8 +314,11 @@
fun atp_translated_fact _ (ATP_Translated_Fact p) = p
| atp_translated_fact ctxt fact =
translate_atp_fact ctxt (untranslated_fact fact)
-fun smt_weighted_fact (SMT_Weighted_Fact p) = p
- | smt_weighted_fact fact = untranslated_fact fact |> apsnd (pair NONE)
+fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
+ | smt_weighted_fact thy num_facts (fact, j) =
+ (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
+
+(* generic TPTP-based ATPs *)
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
@@ -364,7 +396,7 @@
I)
|>> (if measure_run_time then split_time else rpair NONE)
val (tstplike_proof, outcome) =
- extract_tstplike_proof_and_outcome complete res_code
+ extract_tstplike_proof_and_outcome verbose complete res_code
proof_delims known_failures output
in (output, msecs, tstplike_proof, outcome) end
val readable_names = debug andalso overlord
@@ -471,11 +503,12 @@
| failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
(case AList.lookup (op =) smt_failures code of
SOME failure => failure
- | NONE => UnknownError)
+ | NONE => UnknownError ("Abnormal termination with exit code " ^
+ string_of_int code ^ "."))
| failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
| failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
if String.isPrefix internal_error_prefix msg then InternalError
- else UnknownError
+ else UnknownError msg
(* FUDGE *)
val smt_max_iters = Unsynchronized.ref 8
@@ -602,7 +635,10 @@
: prover_problem) =
let
val ctxt = Proof.context_of state
- val facts = facts |> map smt_weighted_fact
+ val thy = Proof.theory_of state
+ val num_facts = length facts
+ val facts = facts ~~ (0 upto num_facts - 1)
+ |> map (smt_weighted_fact thy num_facts)
val {outcome, used_facts, run_time_in_msecs} =
smt_filter_loop name params state subgoal smt_head facts
val (chained_lemmas, other_lemmas) = split_used_facts (map fst used_facts)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 22:23:56 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Dec 17 23:18:39 2010 +0100
@@ -12,14 +12,6 @@
type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command
type params = Sledgehammer_Provers.params
- (* for experimentation purposes -- do not use in production code *)
- val smt_weights : bool Unsynchronized.ref
- val smt_weight_min_facts : int Unsynchronized.ref
- val smt_min_weight : int Unsynchronized.ref
- val smt_max_weight : int Unsynchronized.ref
- val smt_max_weight_index : int Unsynchronized.ref
- val smt_weight_curve : (int -> int) Unsynchronized.ref
-
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -66,22 +58,38 @@
{state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count, facts = take num_facts facts,
smt_head = smt_head}
+ fun really_go () =
+ prover params (minimize_command name) problem
+ |> (fn {outcome, used_facts, message, ...} =>
+ if is_some outcome then
+ ("none", message)
+ else
+ let
+ val (used_facts, message) =
+ if length used_facts >= implicit_minimization_threshold then
+ minimize_facts params true subgoal subgoal_count state
+ (filter_used_facts used_facts
+ (map (apsnd single o untranslated_fact) facts))
+ |>> Option.map (map fst)
+ else
+ (SOME used_facts, message)
+ val _ =
+ case (debug, used_facts) of
+ (true, SOME (used_facts as _ :: _)) =>
+ facts ~~ (0 upto length facts - 1)
+ |> map (fn (fact, j) =>
+ fact |> untranslated_fact |> apsnd (K j))
+ |> filter_used_facts used_facts
+ |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+ |> commas
+ |> enclose ("Fact" ^ plural_s num_facts ^ " in " ^
+ quote name ^ " proof (of " ^
+ string_of_int num_facts ^ "): ") "."
+ |> Output.urgent_message
+ | _ => ()
+ in ("some", message) end)
fun go () =
let
- fun really_go () =
- prover params (minimize_command name) problem
- |> (fn {outcome, used_facts, message, ...} =>
- if is_some outcome then
- ("none", message)
- else
- ("some",
- if length used_facts >= implicit_minimization_threshold then
- minimize_facts params true subgoal subgoal_count state
- (filter_used_facts used_facts
- (map (apsnd single o untranslated_fact) facts))
- |> snd
- else
- message))
val (outcome_code, message) =
if debug then
really_go ()
@@ -124,27 +132,6 @@
(false, state))
end
-val smt_weights = Unsynchronized.ref true
-val smt_weight_min_facts = Unsynchronized.ref 20
-
-(* FUDGE *)
-val smt_min_weight = Unsynchronized.ref 0
-val smt_max_weight = Unsynchronized.ref 10
-val smt_max_weight_index = Unsynchronized.ref 200
-val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
-
-fun smt_fact_weight j num_facts =
- if !smt_weights andalso num_facts >= !smt_weight_min_facts then
- SOME (!smt_max_weight
- - (!smt_max_weight - !smt_min_weight + 1)
- * !smt_weight_curve (Int.max (0, !smt_max_weight_index - j - 1))
- div !smt_weight_curve (!smt_max_weight_index))
- else
- NONE
-
-fun weight_smt_fact thy num_facts (fact, j) =
- fact |> apsnd (pair (smt_fact_weight j num_facts) o Thm.transfer thy)
-
fun class_of_smt_solver ctxt name =
ctxt |> select_smt_solver name
|> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
@@ -154,6 +141,9 @@
| smart_par_list_map f [x] = [f x]
| smart_par_list_map f xs = Par_List.map f xs
+fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
+ | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
+
(* FUDGE *)
val auto_max_relevant_divisor = 2
@@ -181,32 +171,29 @@
| NONE => ()
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
- fun run_provers get_facts translate maybe_smt_head provers
- (res as (success, state)) =
- if success orelse null provers then
- res
- else
- let
- val facts = get_facts ()
- val num_facts = length facts
- val facts = facts ~~ (0 upto num_facts - 1)
- |> map (translate num_facts)
- val problem =
- {state = state, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts,
- smt_head = maybe_smt_head (map smt_weighted_fact facts) i}
- val run_prover = run_prover params auto minimize_command only
- in
- if auto then
- fold (fn prover => fn (true, state) => (true, state)
- | (false, _) => run_prover problem prover)
- provers (false, state)
- else
- provers
- |> (if blocking then smart_par_list_map else map)
- (run_prover problem)
- |> exists fst |> rpair state
- end
+ fun run_provers state get_facts translate maybe_smt_head provers =
+ let
+ val facts = get_facts ()
+ val num_facts = length facts
+ val facts = facts ~~ (0 upto num_facts - 1)
+ |> map (translate num_facts)
+ val problem =
+ {state = state, goal = goal, subgoal = i, subgoal_count = n,
+ facts = facts,
+ smt_head = maybe_smt_head
+ (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
+ val run_prover = run_prover params auto minimize_command only
+ in
+ if auto then
+ fold (fn prover => fn (true, state) => (true, state)
+ | (false, _) => run_prover problem prover)
+ provers (false, state)
+ else
+ provers
+ |> (if blocking then smart_par_list_map else map)
+ (run_prover problem)
+ |> exists fst |> rpair state
+ end
fun get_facts label no_dangerous_types relevance_fudge provers =
let
val max_max_relevant =
@@ -235,24 +222,27 @@
else
())
end
- val run_atps =
- run_provers
- (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
- (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
- (K (K NONE)) atps
+ fun run_atps (accum as (success, _)) =
+ if success orelse null atps then
+ accum
+ else
+ run_provers state
+ (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
+ (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
+ (K (K NONE)) atps
fun run_smts (accum as (success, _)) =
if success orelse null smts then
accum
else
let
val facts = get_facts "SMT solver" true smt_relevance_fudge smts
- val translate = SMT_Weighted_Fact oo weight_smt_fact thy
- val maybe_smt_head = try o SMT_Solver.smt_filter_head state
+ val weight = SMT_Weighted_Fact oo weight_smt_fact thy
+ fun smt_head facts =
+ try (SMT_Solver.smt_filter_head state (facts ()))
in
smts |> map (`(class_of_smt_solver ctxt))
|> AList.group (op =)
- |> map (fn (_, smts) => run_provers (K facts) translate
- maybe_smt_head smts accum)
+ |> map (run_provers state (K facts) weight smt_head o snd)
|> exists fst |> rpair state
end
fun run_atps_and_smt_solvers () =