generalization of the Sledgehammer minimizer, to make it possible to handle SMT solvers as well
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Oct 21 16:25:40 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200
@@ -357,19 +357,18 @@
relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
- axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms,
- only = true}
+ axioms = axioms |> map Sledgehammer.Unprepared, only = true}
val time_limit =
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, used_thm_names,
- atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.atp_result,
+ val ({outcome, message, used_axioms, run_time_in_msecs = time_atp, ...}
+ : Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K ""))) problem
in
case outcome of
- NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
+ NONE => (message, SH_OK (time_isa, time_atp, used_axioms))
| SOME _ => (message, SH_FAIL (time_isa, time_atp))
end
handle ERROR msg => ("error: " ^ msg, SH_ERROR)
@@ -445,7 +444,7 @@
val params = Sledgehammer_Isar.default_params thy
[("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
val minimize =
- Sledgehammer_Minimize.minimize_theorems params 1 (subgoal_count st)
+ Sledgehammer_Minimize.minimize_facts params 1 (subgoal_count st)
val _ = log separator
in
case minimize st (these (!named_thms)) of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Oct 21 16:25:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Oct 22 09:50:18 2010 +0200
@@ -29,25 +29,24 @@
timeout: Time.time,
expect: string}
- type atp_problem =
+ datatype axiom =
+ Unprepared of (string * locality) * thm |
+ Prepared of term * ((string * locality) * fol_formula) option
+
+ type prover_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
- axioms: (term * ((string * locality) * fol_formula) option) list,
+ axioms: axiom list,
only: bool}
- type atp_result =
+ type prover_result =
{outcome: failure option,
message: string,
- pool: string Symtab.table,
- used_thm_names: (string * locality) list,
- atp_run_time_in_msecs: int,
- output: string,
- tstplike_proof: string,
- axiom_names: (string * locality) list vector,
- conjecture_shape: int list list}
+ used_axioms: (string * locality) list,
+ run_time_in_msecs: int}
- type atp = params -> minimize_command -> atp_problem -> atp_result
+ type prover = params -> minimize_command -> prover_problem -> prover_result
val smtN : string
val dest_dir : string Config.T
@@ -57,10 +56,11 @@
val kill_provers : unit -> unit
val running_provers : unit -> unit
val messages : int option -> unit
- val run_atp : theory -> string -> atp
+ val run_atp : theory -> string -> prover
+ val is_smt_solver_installed : unit -> bool
val run_smt_solver :
- Proof.context -> bool -> Time.time -> ('a * thm) list -> string * 'a list
- val is_smt_solver_installed : unit -> bool
+ bool -> params -> minimize_command -> prover_problem
+ -> string * (string * locality) list
val run_sledgehammer :
params -> bool -> int -> relevance_override -> (string -> minimize_command)
-> Proof.state -> bool * Proof.state
@@ -120,25 +120,24 @@
timeout: Time.time,
expect: string}
-type atp_problem =
+datatype axiom =
+ Unprepared of (string * locality) * thm |
+ Prepared of term * ((string * locality) * fol_formula) option
+
+type prover_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
- axioms: (term * ((string * locality) * fol_formula) option) list,
+ axioms: axiom list,
only: bool}
-type atp_result =
+type prover_result =
{outcome: failure option,
message: string,
- pool: string Symtab.table,
- used_thm_names: (string * locality) list,
- atp_run_time_in_msecs: int,
- output: string,
- tstplike_proof: string,
- axiom_names: (string * locality) list vector,
- conjecture_shape: int list list}
+ used_axioms: (string * locality) list,
+ run_time_in_msecs: int}
-type atp = params -> minimize_command -> atp_problem -> atp_result
+type prover = params -> minimize_command -> prover_problem -> prover_result
(* configuration attributes *)
@@ -176,6 +175,11 @@
(* generic TPTP-based ATPs *)
+fun dest_Unprepared (Unprepared p) = p
+ | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared"
+fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p
+ | prepared_axiom _ (Prepared p) = p
+
(* Important messages are important but not so important that users want to see
them each time. *)
val important_message_keep_factor = 0.1
@@ -186,24 +190,26 @@
use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
- minimize_command ({state, goal, subgoal, axioms, only} : atp_problem) =
+ minimize_command
+ ({state, goal, subgoal, axioms, only} : prover_problem) =
let
val ctxt = Proof.context_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
- val axioms = axioms |> not only
- ? take (the_default default_max_relevant max_relevant)
+ val axioms =
+ axioms |> not only ? take (the_default default_max_relevant max_relevant)
+ |> map (prepared_axiom ctxt)
val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
val problem_prefix = Config.get ctxt problem_prefix
- val atp_problem_file_name =
+ val problem_file_name =
Path.basic ((if overlord then "prob_" ^ atp_name
else problem_prefix ^ serial_string ())
^ "_" ^ string_of_int subgoal)
- val atp_problem_path_name =
+ val problem_path_name =
if dest_dir = "" then
- File.tmp_path atp_problem_file_name
+ File.tmp_path problem_file_name
else if File.exists (Path.explode dest_dir) then
- Path.append (Path.explode dest_dir) atp_problem_file_name
+ Path.append (Path.explode dest_dir) problem_file_name
else
error ("No such directory: " ^ quote dest_dir ^ ".")
val measure_run_time = verbose orelse Config.get ctxt measure_run_time
@@ -288,7 +294,7 @@
File.write (Path.explode (Path.implode probfile ^ "_proof")) output
val ((pool, conjecture_shape, axiom_names),
(output, msecs, tstplike_proof, outcome)) =
- with_path cleanup export run_on atp_problem_path_name
+ with_path cleanup export run_on problem_path_name
val (conjecture_shape, axiom_names) =
repair_conjecture_shape_and_axiom_names output conjecture_shape
axiom_names
@@ -297,7 +303,7 @@
extract_important_message output
else
""
- val (message, used_thm_names) =
+ val (message, used_axioms) =
case outcome of
NONE =>
proof_text isar_proof
@@ -317,10 +323,8 @@
""))
| SOME failure => (string_for_failure failure, [])
in
- {outcome = outcome, message = message, pool = pool,
- used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
- output = output, tstplike_proof = tstplike_proof,
- axiom_names = axiom_names, conjecture_shape = conjecture_shape}
+ {outcome = outcome, message = message, used_axioms = used_axioms,
+ run_time_in_msecs = msecs}
end
fun run_atp thy name = atp_fun false name (get_atp thy name)
@@ -328,8 +332,8 @@
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) =
+ (prover_problem as {state, goal, axioms, ...})
+ (prover as {default_max_relevant, ...}, atp_name) =
let
val ctxt = Proof.context_of state
val birth_time = Time.now ()
@@ -340,8 +344,8 @@
fun go () =
let
fun really_go () =
- atp_fun auto atp_name atp params (minimize_command atp_name)
- atp_problem
+ atp_fun auto atp_name prover params (minimize_command atp_name)
+ prover_problem
|> (fn {outcome, message, ...} =>
(if is_some outcome then "none" else "some", message))
val (outcome_code, message) =
@@ -379,25 +383,31 @@
end
(* 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
+(* FIXME: dummy *)
+fun raw_run_smt_solver remote timeout state axioms i =
+ ("", axioms |> take 5 |> map fst)
+
+fun run_smt_solver remote ({timeout, ...} : params) minimize_command
+ ({state, subgoal, axioms, ...} : prover_problem) =
+ raw_run_smt_solver remote timeout state
+ (map_filter (try dest_Unprepared) axioms) subgoal
+
+fun run_smt_solver_somehow state (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 ctxt = Proof.context_of state
+ val desc = prover_description ctxt params name (length axioms) i n goal
+ val (failure, used_axioms) =
+ raw_run_smt_solver remote timeout state axioms i
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))
+ command_call "smt" (map fst used_axioms))
else
"Error: " ^ failure)
in priority message; success end
@@ -441,15 +451,16 @@
relevant_facts ctxt full_types relevance_thresholds
max_max_relevant relevance_override chained_ths
hyp_ts concl_t
- val atp_problem =
+ val prover_problem =
{state = state, goal = goal, subgoal = i,
- axioms = map (prepare_axiom ctxt) axioms, only = only}
+ axioms = axioms |> map (Prepared o prepare_axiom ctxt),
+ only = only}
val run_atp_somehow =
- run_atp_somehow params auto i n minimize_command atp_problem
+ run_atp_somehow params auto i n minimize_command prover_problem
in
if auto then
- fold (fn atp => fn (true, state) => (true, state)
- | (false, _) => run_atp_somehow atp)
+ fold (fn prover => fn (true, state) => (true, state)
+ | (false, _) => run_atp_somehow prover)
atps (false, state)
else
atps |> (if blocking then Par_List.map else map) run_atp_somehow
@@ -467,7 +478,7 @@
max_relevant relevance_override chained_ths
hyp_ts concl_t
in
- smts |> map (run_smt_solver_somehow ctxt params i n goal axioms)
+ smts |> map (run_smt_solver_somehow state params i n goal axioms)
|> exists I |> rpair state
end
fun run_atps_and_smt_solvers () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Oct 21 16:25:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Oct 22 09:50:18 2010 +0200
@@ -2,7 +2,7 @@
Author: Philipp Meyer, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
-Minimization of theorem list for Metis using automatic theorem provers.
+Minimization of fact list for Metis using ATPs.
*)
signature SLEDGEHAMMER_MINIMIZE =
@@ -10,7 +10,7 @@
type locality = Sledgehammer_Filter.locality
type params = Sledgehammer.params
- val minimize_theorems :
+ val minimize_facts :
params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
-> ((string * locality) * thm list) list option * string
val run_minimize :
@@ -24,7 +24,6 @@
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_Translate
-open Sledgehammer_Reconstruct
open Sledgehammer
(* wrapper for calling external prover *)
@@ -34,9 +33,9 @@
| string_for_failure Interrupted = "Interrupted."
| string_for_failure _ = "Unknown error."
-fun n_theorems names =
+fun n_facts names =
let val n = length names in
- string_of_int n ^ " theorem" ^ plural_s n ^
+ string_of_int n ^ " fact" ^ plural_s n ^
(if n > 0 then
": " ^ (names |> map fst
|> sort_distinct string_ord |> space_implode " ")
@@ -44,45 +43,45 @@
"")
end
-fun test_theorems ({debug, verbose, overlord, provers, full_types, isar_proof,
- isar_shrink_factor, ...} : params)
- (atp : atp) explicit_apply timeout subgoal state axioms =
+fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,
+ isar_shrink_factor, ...} : params) (prover : prover)
+ explicit_apply timeout subgoal state axioms =
let
val _ =
- priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
+ priority ("Testing " ^ n_facts (map fst axioms) ^ "...")
val params =
{blocking = true, debug = debug, verbose = verbose, overlord = overlord,
provers = provers, full_types = full_types,
explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
- max_relevant = SOME 65536 (* a large number *), isar_proof = isar_proof,
+ max_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
- val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
+ val axioms =
+ axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n))
val {context = ctxt, goal, ...} = Proof.goal state
- val atp_problem =
- {state = state, goal = goal, subgoal = subgoal,
- axioms = map (prepare_axiom ctxt) axioms, only = true}
- val result as {outcome, used_thm_names, ...} = atp params (K "") atp_problem
+ val prover_problem =
+ {state = state, goal = goal, subgoal = subgoal, axioms = axioms,
+ only = true}
+ val result as {outcome, used_axioms, ...} =
+ prover params (K "") prover_problem
in
priority (case outcome of
- NONE =>
- if length used_thm_names = length axioms then
- "Found proof."
- else
- "Found proof with " ^ n_theorems used_thm_names ^ "."
- | SOME failure => string_for_failure failure);
+ SOME failure => string_for_failure failure
+ | NONE =>
+ if length used_axioms = length axioms then "Found proof."
+ else "Found proof with " ^ n_facts used_axioms ^ ".");
result
end
(* minimalization of thms *)
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun filter_used_axioms used = filter (member (op =) used o fst)
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
case test (xs @ seen) of
- result as {outcome = NONE, used_thm_names, ...} : atp_result =>
- sublinear_minimize test (filter_used_facts used_thm_names xs)
- (filter_used_facts used_thm_names seen, result)
+ result as {outcome = NONE, used_axioms, ...} : prover_result =>
+ sublinear_minimize test (filter_used_axioms used_axioms xs)
+ (filter_used_axioms used_axioms seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
@@ -90,48 +89,40 @@
timeout. *)
val fudge_msecs = 1000
-fun minimize_theorems {provers = [], ...} _ _ _ _ = error "No prover is set."
- | minimize_theorems (params as {debug, provers = prover :: _, full_types,
- isar_proof, isar_shrink_factor, timeout, ...})
- i (_ : int) state axioms =
+fun minimize_facts {provers = [], ...} _ _ _ _ = error "No prover is set."
+ | minimize_facts (params as {provers = prover_name :: _, timeout, ...})
+ i (_ : int) state axioms =
let
val thy = Proof.theory_of state
- val atp = run_atp thy prover
+ val prover = run_atp thy prover_name
val msecs = Time.toMilliseconds timeout
- val _ = priority ("Sledgehammer minimize: prover " ^ quote prover ^ ".")
- val {context = ctxt, goal, ...} = Proof.goal state
+ val _ = priority ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
+ val {goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
val explicit_apply =
not (forall (Meson.is_fol_term thy)
(concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
fun do_test timeout =
- test_theorems params atp explicit_apply timeout i state
+ test_facts params prover explicit_apply timeout i state
val timer = Timer.startRealTimer ()
in
(case do_test timeout axioms of
- result as {outcome = NONE, pool, used_thm_names,
- conjecture_shape, ...} =>
+ result as {outcome = NONE, used_axioms, ...} =>
let
val time = Timer.checkRealTimer timer
val new_timeout =
Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
|> Time.fromMilliseconds
- val (min_thms, {tstplike_proof, axiom_names, ...}) =
+ val (min_thms, {message, ...}) =
sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_thm_names axioms) ([], result)
+ (filter_used_axioms used_axioms axioms) ([], result)
val n = length min_thms
val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+ ["Minimized: " ^ string_of_int n ^ " fact" ^ plural_s n] ^
(case length (filter (curry (op =) Chained o snd o fst) min_thms) of
0 => ""
| n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- ("Minimized command", full_types, K "", tstplike_proof,
- axiom_names, goal, i) |> fst)
- end
+ in (SOME min_thms, message) end
| {outcome = SOME TimedOut, ...} =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \
\option (e.g., \"timeout = " ^
@@ -159,7 +150,7 @@
0 => priority "No subgoal!"
| n =>
(kill_provers ();
- priority (#2 (minimize_theorems params i n state axioms)))
+ priority (#2 (minimize_facts params i n state axioms)))
end
end;