--- a/src/HOL/Tools/atp_wrapper.ML Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Sun Jun 28 15:01:29 2009 +0200
@@ -75,7 +75,7 @@
(* write out problem file and call prover *)
val probfile = prob_pathname subgoalno
- val _ = writer probfile clauses
+ val conj_pos = writer probfile clauses
val (proof, rc) = system_out (
if File.exists cmd then
space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
@@ -92,7 +92,8 @@
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 name (proof, thm_names, ctxt, th, subgoalno)
+ else "Try this command: " ^
+ produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
in (success, message, proof, thm_names, the_filtered_clauses) end;
@@ -109,7 +110,7 @@
(ResHolClause.tptp_write_file (AtpManager.get_full_types()))
command
ResReconstruct.find_failure
- (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
+ (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
timeout ax_clauses fcls name n goal;
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
@@ -174,7 +175,7 @@
(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
+ (ResReconstruct.lemma_list true)
timeout ax_clauses fcls name n goal;
val spass = spass_opts 40 true;
--- a/src/HOL/Tools/res_reconstruct.ML Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Sun Jun 28 15:01:29 2009 +0200
@@ -16,10 +16,11 @@
val setup: Context.theory -> Context.theory
(* extracting lemma list*)
val find_failure: string -> string option
- 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
+ val lemma_list: bool -> string ->
+ string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
(* structured proofs *)
- val structured_proof: string -> string * string vector * Proof.context * Thm.thm * int -> string
+ val structured_proof: string ->
+ string * string vector * (int * int) * Proof.context * Thm.thm * int -> string
end;
structure ResReconstruct : RES_RECONSTRUCT =
@@ -496,17 +497,17 @@
(* === EXTRACTING LEMMAS === *)
(* lines have the form "cnf(108, axiom, ...",
the number (108) has to be extracted)*)
- fun get_step_nums_tstp proofextract =
+ fun get_step_nums false proofextract =
let val toks = String.tokens (not o Char.isAlphaNum)
fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
+ | inputno ("cnf"::ntok::"negated"::"conjecture"::_) = Int.fromString ntok
| inputno _ = NONE
val lines = split_lines proofextract
in List.mapPartial (inputno o toks) lines end
-
- (*String contains multiple lines. We want those of the form
+ (*String contains multiple lines. We want those of the form
"253[0:Inp] et cetera..."
A list consisting of the first number in each line is returned. *)
- fun get_step_nums_dfg proofextract =
+ | get_step_nums true proofextract =
let val toks = String.tokens (not o Char.isAlphaNum)
fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
| inputno _ = NONE
@@ -514,15 +515,19 @@
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, conj_count, _, _, _) =
let
(* get the names of axioms from their numbers*)
fun get_axiom_names thm_names step_nums =
let
- fun is_axiom n = n <= Vector.length thm_names
+ val last_axiom = Vector.length thm_names
+ fun is_axiom n = n <= last_axiom
+ fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count
fun getname i = Vector.sub(thm_names, i-1)
in
- sort_distinct string_ord (filter (fn x => x <> "??.unknown") (map getname (filter is_axiom step_nums)))
+ (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
+ (map getname (filter is_axiom step_nums))),
+ exists is_conj step_nums)
end
val proofextract = get_proof_extract proof
in
@@ -545,22 +550,23 @@
fun sendback_metis_nochained lemmas =
(Markup.markup Markup.sendback o metis_line) (nochained lemmas)
- 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;
+
+ fun lemma_list dfg name result =
+ let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result
+ in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
+ (if used_conj then ""
+ else "\nWarning: Goal is provable because context is inconsistent.")
+ end;
(* === Extracting structured Isar-proof === *)
- fun structured_proof name (result as (proof, thm_names, ctxt, goal, subgoalno)) =
+ fun structured_proof name (result as (proof, thm_names, conj_count, 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 name result
+ val one_line_proof = lemma_list false 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