# HG changeset patch # User blanchet # Date 1337800788 -7200 # Node ID 96c9b8381909a368b5386c4731975942229143e4 # Parent 2aea51a142008e76b94c51d954b6467216f224bc better handling of incomplete TSTP proofs diff -r 2aea51a14200 -r 96c9b8381909 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed May 23 21:19:48 2012 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed May 23 21:19:48 2012 +0200 @@ -481,6 +481,15 @@ | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time |> Time.toMilliseconds val msg = message (preplay ()) ^ message_tail + val (outcome, used_facts) = + (* Repair incomplete or missing proofs. Better do it here and not in + Sledgehammer, so that actual Sledgehammer users get a chance to report + the issue. FIXME: This is a temporary hack. *) + if outcome = SOME ATP_Proof.ProofIncomplete orelse + outcome = SOME ATP_Proof.ProofMissing then + (NONE, []) + else + (outcome, used_facts) in case outcome of NONE => (msg, SH_OK (time_isa, time_prover, used_facts)) diff -r 2aea51a14200 -r 96c9b8381909 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed May 23 21:19:48 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed May 23 21:19:48 2012 +0200 @@ -541,7 +541,7 @@ | atp_proof_from_tstplike_proof problem output tstp = tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof problem (extract_spass_name_vector output) - |> sort (step_name_ord o pairself step_name) + |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) fun clean_up_dependencies _ [] = [] | clean_up_dependencies seen diff -r 2aea51a14200 -r 96c9b8381909 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 23 21:19:48 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed May 23 21:19:48 2012 +0200 @@ -305,9 +305,9 @@ "--cpu-limit=" ^ string_of_int (to_secs 2 timeout), proof_delims = tstp_proof_delims, known_failures = - known_szs_status_failures @ [(TimedOut, "Failure: Resource limit exceeded (time)"), - (TimedOut, "time limit exceeded")], + (TimedOut, "time limit exceeded")] @ + known_szs_status_failures, prem_kind = Conjecture, best_slices = fn ctxt => let val heuristic = effective_e_selection_heuristic ctxt in @@ -337,9 +337,13 @@ "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout), proof_delims = tstp_proof_delims, known_failures = - known_szs_status_failures @ - [(TimedOut, "CPU time limit exceeded, terminating"), - (GaveUp, "No.of.Axioms")], + [(* LEO 1.3.3 does not record definitions properly, leading to missing + dependencies in the TSTP proof. Remove the next line once this is + fixed. *) + (ProofIncomplete, "_def,definition,"), + (TimedOut, "CPU time limit exceeded, terminating"), + (GaveUp, "No.of.Axioms")] @ + known_szs_status_failures, prem_kind = Hypothesis, best_slices = (* FUDGE *) @@ -390,7 +394,6 @@ |> sos = sosN ? prefix "-SOS=1 ", proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = - known_perl_failures @ [(OldSPASS, "SPASS V 3.5"), (OldSPASS, "SPASS V 3.7"), (GaveUp, "SPASS beiseite: Completion found"), @@ -399,7 +402,8 @@ (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), (Unprovable, "No formulae and clauses found in input file"), - (InternalError, "Please report this error")], + (InternalError, "Please report this error")] @ + known_perl_failures, prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *) @@ -467,12 +471,12 @@ ("% SZS output start Refutation", "% SZS output end Refutation"), ("% SZS output start Proof", "% SZS output end Proof")], known_failures = - known_szs_status_failures @ [(GaveUp, "UNPROVABLE"), (GaveUp, "CANNOT PROVE"), (Unprovable, "Satisfiability detected"), (Unprovable, "Termination reason: Satisfiable"), - (Interrupted, "Aborted by signal SIGINT")], + (Interrupted, "Aborted by signal SIGINT")] @ + known_szs_status_failures, prem_kind = Conjecture, best_slices = fn ctxt => (* FUDGE *)