added Philipp Meyer's implementation of AtpMinimal
together with related changes in the sledgehammer-interface:
adapted type of prover, optional relevance filtering,
public get_prover for registered atps in AtpManager,
included atp_minimize in s/h response;
--- a/src/HOL/ATP_Linkup.thy Mon May 04 14:49:51 2009 +0200
+++ b/src/HOL/ATP_Linkup.thy Mon May 04 23:37:39 2009 +0200
@@ -17,6 +17,7 @@
("Tools/res_atp.ML")
("Tools/atp_manager.ML")
("Tools/atp_wrapper.ML")
+ ("Tools/atp_minimal.ML")
"~~/src/Tools/Metis/metis.ML"
("Tools/metis_tools.ML")
begin
@@ -98,6 +99,8 @@
use "Tools/atp_manager.ML"
use "Tools/atp_wrapper.ML"
+use "Tools/atp_minimal.ML"
+
text {* basic provers *}
setup {* AtpManager.add_prover "spass" AtpWrapper.spass *}
setup {* AtpManager.add_prover "vampire" AtpWrapper.vampire *}
--- a/src/HOL/Tools/atp_manager.ML Mon May 04 14:49:51 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Mon May 04 23:37:39 2009 +0200
@@ -19,9 +19,11 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
+ type prover = int -> (thm * (string * int)) list option -> string -> int ->
+ Proof.context * (thm list * thm) -> bool * string * string * string vector
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
+ val get_prover: string -> theory -> prover option
val sledgehammer: string list -> Proof.state -> unit
end;
@@ -286,7 +288,8 @@
(* named provers *)
-type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string;
+type prover = int -> (thm * (string * int)) list option -> string -> int ->
+ Proof.context * (thm list * thm) -> bool * string * string * string vector
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
@@ -307,13 +310,16 @@
fun print_provers thy = Pretty.writeln
(Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
+fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
+ NONE => NONE
+| SOME (prover, _) => SOME prover;
(* start prover thread *)
fun start_prover name birthtime deadtime i proof_state =
- (case Symtab.lookup (Provers.get (Proof.theory_of proof_state)) name of
+ (case get_prover name (Proof.theory_of proof_state) of
NONE => warning ("Unknown external prover: " ^ quote name)
- | SOME (prover, _) =>
+ | SOME prover =>
let
val (ctxt, (_, goal)) = Proof.get_goal proof_state
val desc =
@@ -322,7 +328,10 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birthtime deadtime (Thread.self (), desc)
- val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
+ val result =
+ let val (success, message, _, _) =
+ prover (get_timeout ()) NONE name i (Proof.get_goal proof_state)
+ in (success, message) end
handle ResHolClause.TOO_TRIVIAL
=> (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/atp_minimal.ML Mon May 04 23:37:39 2009 +0200
@@ -0,0 +1,201 @@
+(* Title: HOL/Tools/atp_minimal.ML
+ Author: Philipp Meyer, TU Muenchen
+
+Minimalization of theorem list for metis by using an external automated theorem prover
+*)
+
+structure AtpMinimal =
+struct
+
+ (* output control *)
+ fun debug str = Output.debug (fn () => str)
+ fun debug_fn f = if !Output.debugging then f() else ()
+ fun answer str = Output.writeln str
+ fun println str = Output.priority str
+
+ fun order_unique name_list = OrdList.make (String.collate Char.compare) name_list
+ fun length_string namelist = Int.toString (length namelist)
+
+ fun print_names name_thms_pairs =
+ let
+ val names = (map fst name_thms_pairs)
+ val ordered = order_unique names
+ in
+ app (fn name => (debug (" " ^ name))) ordered
+ end
+
+ (* minimalization algorithm *)
+ local
+ fun isplit (l,r) [] = (l,r)
+ | isplit (l,r) (h::[]) = (h::l, r)
+ | isplit (l,r) (h1::h2::t) = isplit (h1::l, h2::r) t
+ in
+ fun split lst = isplit ([],[]) lst
+ end
+
+ local
+ fun min p sup [] = raise Empty
+ | min p sup [s0] = [s0]
+ | min p sup s =
+ let
+ val (l0, r0) = split s
+ in
+ if p(sup @ l0)
+ then min p sup l0
+ else
+ if p(sup @ r0)
+ then min p sup r0
+ else
+ let
+ val l = min p (sup @ r0) l0
+ val r = min p (sup @ l) r0
+ in
+ l @ r
+ end
+ end
+ in
+ (* return a minimal subset v of s that satisfies p
+ @pre p(s) & ~p([]) & monotone(p)
+ @post v subset s & p(v) &
+ forall e in v. ~p(v \ e)
+ *)
+ fun minimal p s = min p [] s
+ end
+
+ (* failure check and producing answer*)
+ datatype 'a prove_result = Success of 'a | Failure | Timeout | Error
+
+ val string_of_result = fn
+ Success _ => "Success"
+ | Failure => "Failure"
+ | Timeout => "Timeout"
+ | Error => "Error"
+
+ val failure_strings =
+ [("SPASS beiseite: Ran out of time.", Timeout),
+ ("Timeout", Timeout),
+ ("time limit exceeded", Timeout),
+ ("# Cannot determine problem status within resource limit", Timeout),
+ ("Error", Error)]
+
+ fun produce_answer (success, message, result_string, thm_name_vec) =
+ if success then
+ (Success (Vector.foldr op:: [] thm_name_vec), result_string)
+ else
+ let
+ val failure = get_first (fn (s, t) => if String.isSubstring s result_string then SOME (t, result_string) else NONE) failure_strings
+ in
+ if is_some failure then
+ the failure
+ else
+ (Failure, result_string)
+ end
+
+ (* wrapper for calling external prover *)
+ fun sh_test_thms prover prover_name time_limit subgoalno state name_thms_pairs =
+ let
+ val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
+ val name_thm_pairs = flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
+ val _ = debug_fn (fn () => print_names name_thm_pairs)
+ val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+ val (result, proof) =
+ (produce_answer (prover time_limit (SOME axclauses) prover_name subgoalno (Proof.get_goal state)))
+ val _ = println (string_of_result result)
+ val _ = debug proof
+ in
+ (result, proof)
+ end
+
+ (* minimalization of thms *)
+ fun minimalize prover prover_name time_limit state name_thms_pairs =
+ let
+ val _ = println ("Minimize called with " ^ (length_string name_thms_pairs) ^ " theorems, prover: "
+ ^ prover_name ^ ", time limit: " ^ (Int.toString time_limit) ^ " seconds")
+ val _ = debug_fn (fn () => app (fn (n, tl) => (debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
+ val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
+ fun test_thms thms = case test_thms_fun thms of (Success _, _) => true | _ => false
+ in
+ (* try proove first to check result and get used theorems *)
+ (case test_thms_fun name_thms_pairs of
+ (Success used, _) =>
+ let
+ val ordered_used = order_unique used
+ val to_use =
+ if length ordered_used < length name_thms_pairs then
+ filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
+ else
+ name_thms_pairs
+ val min_thms = (minimal test_thms to_use)
+ val min_names = order_unique (map fst min_thms)
+ val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
+ val _ = debug_fn (fn () => print_names min_thms)
+ in
+ answer ("Try this command: " ^ Markup.markup Markup.sendback ("apply (metis " ^ (space_implode " " min_names) ^ ")"))
+ end
+ | (Timeout, _) =>
+ answer ("Timeout: You may need to increase the time limit of " ^ (Int.toString time_limit) ^ " seconds. Call atp_minimize [time=...] ")
+ | (Error, msg) =>
+ answer ("Error in prover: " ^ msg)
+ | (Failure, _) =>
+ answer "Failure: No proof with the theorems supplied")
+ handle ResHolClause.TOO_TRIVIAL =>
+ answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ | ERROR msg =>
+ answer ("Error: " ^ msg)
+ end
+
+ (* isar command and parsing input *)
+
+ local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
+
+ fun get_thms context =
+ map (fn (name, interval) =>
+ let
+ val thmref = Facts.Named ((name, Position.none), interval)
+ val ths = ProofContext.get_fact context thmref
+ val name' = Facts.string_of_ref thmref
+ in
+ (name', ths)
+ end)
+
+ val default_prover = "remote_vampire"
+ val default_time_limit = 5
+
+ fun get_time_limit_arg time_string =
+ (case Int.fromString time_string of
+ SOME t => t
+ | NONE => error ("Invalid time limit: " ^ quote time_string))
+
+ val get_options =
+ let
+ val def = (default_prover, default_time_limit)
+ in
+ foldl (fn ((name, a), (p, t)) => (case name of
+ "time" => (p, (get_time_limit_arg a))
+ | "atp" => (a, t)
+ | n => error ("Invalid argument: " ^ n))) def
+ end
+
+ fun sh_min_command args thm_names state =
+ let
+ val (prover_name, time_limit) = get_options args
+ val prover =
+ case AtpManager.get_prover prover_name (Proof.theory_of state) of
+ SOME prover => prover
+ | NONE => error ("Unknown prover: " ^ quote prover_name)
+ val name_thms_pairs = get_thms (Proof.context_of state) thm_names
+ in
+ minimalize prover prover_name time_limit state name_thms_pairs
+ end
+
+ val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname) )) []
+ val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+
+ val _ =
+ OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
+ (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
+ Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep ((sh_min_command args thm_names) o Toplevel.proof_of)))
+
+ end
+end
+
--- a/src/HOL/Tools/atp_wrapper.ML Mon May 04 14:49:51 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Mon May 04 23:37:39 2009 +0200
@@ -9,10 +9,10 @@
val destdir: string ref
val problem_name: string ref
val external_prover:
- (thm * (string * int)) list ->
+ (unit -> (thm * (string * int)) list) ->
(Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->
Path.T * string -> (string -> string option) ->
- (string * string vector * Proof.context * thm * int -> string) ->
+ (string -> string * string vector * Proof.context * thm * int -> string) ->
AtpManager.prover
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
@@ -46,7 +46,8 @@
(* basic template *)
-fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno goal =
+fun external_prover relevance_filter write_problem_file (cmd, args) find_failure produce_answer
+ timeout axiom_clauses name subgoalno goal =
let
(* path to unique problem file *)
val destdir' = ! destdir
@@ -65,7 +66,8 @@
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
val probfile = prob_pathname subgoalno
val fname = File.platform_path probfile
- val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
+ val the_ax_clauses = case axiom_clauses of NONE => relevance_filter () | SOME axcls => axcls
+ val thm_names = write_problem_file probfile th subgoalno the_ax_clauses thy
val cmdline =
if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
@@ -80,7 +82,7 @@
val message =
if is_some failure then "External prover failed."
else if rc <> 0 then "External prover failed: " ^ proof
- else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
+ else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
val _ =
if is_some failure
@@ -90,7 +92,7 @@
if rc <> 0
then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
else ()
- in (success, message) end;
+ in (success, message, proof, thm_names) end;
@@ -98,14 +100,14 @@
(* generic TPTP-based provers *)
-fun tptp_prover_opts_full max_new theory_const full command timeout n goal =
+fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses name n goal =
external_prover
- (ResAtp.get_relevant max_new theory_const goal n)
+ (fn () => ResAtp.get_relevant max_new theory_const goal n)
(ResAtp.write_problem_file false)
command
ResReconstruct.find_failure
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
- timeout n goal;
+ timeout ax_clauses name n goal;
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
fun tptp_prover_opts max_new theory_const =
@@ -162,14 +164,14 @@
(* SPASS *)
-fun spass_opts max_new theory_const timeout n goal = external_prover
- (ResAtp.get_relevant max_new theory_const goal n)
+fun spass_opts max_new theory_const timeout ax_clauses name n goal = external_prover
+ (fn () => ResAtp.get_relevant max_new theory_const goal n)
(ResAtp.write_problem_file true)
(Path.explode "$SPASS_HOME/SPASS",
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
ResReconstruct.find_failure
ResReconstruct.lemma_list_dfg
- timeout n goal;
+ timeout ax_clauses name n goal;
val spass = spass_opts 40 true;
--- a/src/HOL/Tools/res_reconstruct.ML Mon May 04 14:49:51 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Mon May 04 23:37:39 2009 +0200
@@ -16,10 +16,10 @@
val setup: Context.theory -> Context.theory
(* extracting lemma list*)
val find_failure: string -> string option
- val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
- val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
+ val lemma_list_dfg: string -> string * string vector * Proof.context * Thm.thm * int -> string
+ val lemma_list_tstp: string -> string * string vector * Proof.context * Thm.thm * int -> string
(* structured proofs *)
- val structured_proof: string * string vector * Proof.context * Thm.thm * int -> string
+ val structured_proof: string -> string * string vector * Proof.context * Thm.thm * int -> string
end;
structure ResReconstruct : RES_RECONSTRUCT =
@@ -514,7 +514,7 @@
in List.mapPartial (inputno o toks) lines end
(*extracting lemmas from tstp-output between the lines from above*)
- fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) =
+ fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) =
let
(* get the names of axioms from their numbers*)
fun get_axiom_names thm_names step_nums =
@@ -532,24 +532,33 @@
(* metis-command *)
fun metis_line [] = "apply metis"
| metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+
+ (* atp_minimize [atp=<prover>] <lemmas> *)
+ fun minimize_line _ [] = ""
+ | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
+ (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas)
(*Used to label theorems chained into the sledgehammer call*)
val chained_hint = "CHAINED";
fun sendback_metis_nochained lemmas =
let val nochained = filter_out (fn y => y = chained_hint)
in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end
- fun lemma_list_tstp result = sendback_metis_nochained (extract_lemmas get_step_nums_tstp result);
- fun lemma_list_dfg result = sendback_metis_nochained (extract_lemmas get_step_nums_dfg result);
-
+ fun lemma_list_tstp name result =
+ let val lemmas = extract_lemmas get_step_nums_tstp result
+ in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;
+ fun lemma_list_dfg name result =
+ let val lemmas = extract_lemmas get_step_nums_dfg result
+ in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;
+
(* === Extracting structured Isar-proof === *)
- fun structured_proof (result as (proof, thm_names, ctxt, goal, subgoalno)) =
+ fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) =
let
(*Could use split_lines, but it can return blank lines...*)
val lines = String.tokens (equal #"\n");
val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
val proofextract = get_proof_extract proof
val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
- val one_line_proof = lemma_list_tstp result
+ val one_line_proof = lemma_list_tstp name result
val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
else decode_tstp_file cnfs ctxt goal subgoalno thm_names
in