fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
--- a/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:25 2011 +0200
@@ -12,10 +12,24 @@
type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
datatype failure =
- Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
- CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
- NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
- Interrupted | Crashed | InternalError | UnknownError of string
+ Unprovable |
+ IncompleteUnprovable |
+ ProofMissing |
+ UnsoundProof of bool |
+ CantConnect |
+ TimedOut |
+ OutOfResources |
+ SpassTooOld |
+ VampireTooOld |
+ NoPerl |
+ NoLibwwwPerl |
+ NoRealZ3 |
+ MalformedInput |
+ MalformedOutput |
+ Interrupted |
+ Crashed |
+ InternalError |
+ UnknownError of string
type step_name = string * string option
@@ -47,10 +61,24 @@
open ATP_Problem
datatype failure =
- Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
- CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
- NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
- Interrupted | Crashed | InternalError | UnknownError of string
+ Unprovable |
+ IncompleteUnprovable |
+ ProofMissing |
+ UnsoundProof of bool |
+ CantConnect |
+ TimedOut |
+ OutOfResources |
+ SpassTooOld |
+ VampireTooOld |
+ NoPerl |
+ NoLibwwwPerl |
+ NoRealZ3 |
+ MalformedInput |
+ MalformedOutput |
+ Interrupted |
+ Crashed |
+ InternalError |
+ UnknownError of string
fun strip_spaces_in_list _ [] = []
| strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -95,9 +123,14 @@
"The prover gave up."
| string_for_failure ProofMissing =
"The prover claims the conjecture is a theorem but did not provide a proof."
- | string_for_failure UnsoundProof =
- "The prover found a type-unsound proof. (Or, very unlikely, your axioms \
- \are inconsistent.)"
+ | string_for_failure (UnsoundProof false) =
+ "The prover found a type-unsound proof (or, very unlikely, your axioms \
+ \are inconsistent). Try passing the \"full_types\" option to Sledgehammer \
+ \to avoid such spurious proofs."
+ | string_for_failure (UnsoundProof true) =
+ "The prover found a type-unsound proof even though a supposedly type-sound \
+ \encoding was used (or, very unlikely, your axioms are inconsistent). You \
+ \might want to report this to the Isabelle developers."
| string_for_failure CantConnect = "Cannot connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The prover ran out of resources."
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:25 2011 +0200
@@ -20,8 +20,8 @@
type text_result = string * (string * locality) list
val repair_conjecture_shape_and_fact_names :
- string -> int list list -> (string * locality) list vector
- -> int list list * (string * locality) list vector
+ string -> int list list -> int -> (string * locality) list vector
+ -> int list list * int * (string * locality) list vector
val used_facts_in_atp_proof :
int -> (string * locality) list vector -> string proof
-> (string * locality) list
@@ -78,8 +78,7 @@
fun extract_clause_sequence output =
let
val tokens_of = String.tokens (not o Char.isAlphaNum)
- fun extract_num ("clause" :: (ss as _ :: _)) =
- Int.fromString (List.last ss)
+ fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss)
| extract_num _ = NONE
in output |> split_lines |> map_filter (extract_num o tokens_of) end
@@ -98,7 +97,8 @@
val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
-fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
+fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_offset
+ fact_names =
if String.isSubstring set_ClauseFormulaRelationN output then
let
val j0 = hd (hd conjecture_shape)
@@ -117,11 +117,11 @@
handle Option.Option =>
error ("No such fact: " ^ quote name ^ "."))
in
- (conjecture_shape |> map (maps renumber_conjecture),
+ (conjecture_shape |> map (maps renumber_conjecture), 0,
seq |> map names_for_number |> Vector.fromList)
end
else
- (conjecture_shape, fact_names)
+ (conjecture_shape, fact_offset, fact_names)
val vampire_step_prefix = "f" (* grrr... *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 01 18:37:25 2011 +0200
@@ -495,20 +495,21 @@
extract_tstplike_proof_and_outcome debug verbose complete
res_code proof_delims known_failures output
|>> atp_proof_from_tstplike_proof
- val (conjecture_shape, fact_names) =
+ val (conjecture_shape, facts_offset, fact_names) =
if is_none outcome then
repair_conjecture_shape_and_fact_names output
- conjecture_shape fact_names
+ conjecture_shape facts_offset fact_names
else
- (conjecture_shape, fact_names) (* don't bother repairing *)
+ (* don't bother repairing *)
+ (conjecture_shape, facts_offset, fact_names)
val outcome =
case outcome of
- NONE => if level_of_type_sys type_sys <> Sound andalso
- is_unsound_proof conjecture_shape facts_offset
- fact_names atp_proof then
- SOME UnsoundProof
- else
- NONE
+ NONE =>
+ if is_unsound_proof conjecture_shape facts_offset fact_names
+ atp_proof then
+ SOME (UnsoundProof (level_of_type_sys type_sys = Sound))
+ else
+ NONE
| SOME Unprovable =>
if null blacklist then outcome
else SOME IncompleteUnprovable
@@ -534,7 +535,7 @@
| maybe_run_slice _ _ result = result
fun maybe_blacklist_facts_and_retry iter blacklist
(result as ((_, _, facts_offset, fact_names),
- (_, _, atp_proof, SOME UnsoundProof))) =
+ (_, _, atp_proof, SOME (UnsoundProof false)))) =
(case used_facts_in_atp_proof facts_offset fact_names
atp_proof of
[] => result