# HG changeset patch # User immler@in.tum.de # Date 1241473059 -7200 # Node ID ac8669134e7aca0a78b671525d1b7ef70e6a1a93 # Parent 64ff53fc0c0cb5322b3993433d433c737e1f8148 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; diff -r 64ff53fc0c0c -r ac8669134e7a src/HOL/ATP_Linkup.thy --- 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 *} diff -r 64ff53fc0c0c -r ac8669134e7a src/HOL/Tools/atp_manager.ML --- 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 diff -r 64ff53fc0c0c -r ac8669134e7a src/HOL/Tools/atp_minimal.ML --- /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 + diff -r 64ff53fc0c0c -r ac8669134e7a src/HOL/Tools/atp_wrapper.ML --- 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; diff -r 64ff53fc0c0c -r ac8669134e7a src/HOL/Tools/res_reconstruct.ML --- 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=] *) + 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