--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Aug 18 12:05:44 2010 +0200
@@ -8,9 +8,9 @@
signature ATP_SYSTEMS =
sig
datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
+ MalformedInput | MalformedOutput | UnknownError
type prover_config =
{exec: string * string,
@@ -40,7 +40,7 @@
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+ SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
MalformedOutput | UnknownError
type prover_config =
@@ -63,7 +63,7 @@
| string_for_failure CantConnect = "Can't connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
- | string_for_failure OldSpass =
+ | string_for_failure SpassTooOld =
"Isabelle requires a more recent version of SPASS with support for the \
\TPTP syntax. To install it, download and extract the package \
\\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -72,7 +72,7 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
" on a line of its own."
- | string_for_failure OldVampire =
+ | string_for_failure VampireTooOld =
"Isabelle requires a more recent version of Vampire. To install it, follow \
\the instructions from the Sledgehammer manual (\"isabelle doc\
\ sledgehammer\")."
@@ -170,7 +170,7 @@
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
- (OldSpass, "tptp2dfg")],
+ (SpassTooOld, "tptp2dfg")],
max_new_relevant_facts_per_iter = 35 (* FIXME *),
prefers_theory_relevant = true,
explicit_forall = true}
@@ -197,7 +197,7 @@
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found"),
- (OldVampire, "not a valid option")],
+ (VampireTooOld, "not a valid option")],
max_new_relevant_facts_per_iter = 45 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
--- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Aug 18 12:05:44 2010 +0200
@@ -156,6 +156,7 @@
datatype outcome =
JavaNotInstalled |
+ JavaTooOld |
KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
@@ -303,6 +304,7 @@
datatype outcome =
JavaNotInstalled |
+ JavaTooOld |
KodkodiNotInstalled |
Normal of (int * raw_bound list) list * int list * string |
TimedOut of int list |
@@ -1063,19 +1065,20 @@
|> perhaps (try (unsuffix "."))
|> perhaps (try (unprefix "Solve error: "))
|> perhaps (try (unprefix "Error: "))
+ fun has_error s =
+ first_error |> Substring.full |> Substring.position s |> snd
+ |> Substring.isEmpty |> not
in
if null ps then
if code = 2 then
TimedOut js
else if code = 0 then
Normal ([], js, first_error)
- else if first_error |> Substring.full
- |> Substring.position "exec: java" |> snd
- |> Substring.isEmpty |> not then
+ else if has_error "exec: java" then
JavaNotInstalled
- else if first_error |> Substring.full
- |> Substring.position "NoClassDefFoundError" |> snd
- |> Substring.isEmpty |> not then
+ else if has_error "UnsupportedClassVersionError" then
+ JavaTooOld
+ else if has_error "NoClassDefFoundError" then
KodkodiNotInstalled
else if first_error <> "" then
Error (first_error, js)
--- a/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Aug 18 12:05:44 2010 +0200
@@ -315,6 +315,7 @@
in
case solve_any_problem overlord NONE max_threads max_solutions problems of
JavaNotInstalled => "unknown"
+ | JavaTooOld => "unknown"
| KodkodiNotInstalled => "unknown"
| Normal ([], _, _) => "none"
| Normal _ => "genuine"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Aug 18 12:05:44 2010 +0200
@@ -740,6 +740,9 @@
KK.JavaNotInstalled =>
(print_m install_java_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
+ | KK.JavaTooOld =>
+ (print_m install_java_message;
+ (found_really_genuine, max_potential, max_genuine, donno + 1))
| KK.KodkodiNotInstalled =>
(print_m install_kodkodi_message;
(found_really_genuine, max_potential, max_genuine, donno + 1))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 12:05:44 2010 +0200
@@ -167,8 +167,8 @@
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
val parse_clause_formula_pair =
- $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id
- --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")"
+ $$ "(" |-- scan_integer --| $$ ","
+ -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
--| Scan.option ($$ ",")
val parse_clause_formula_relation =
Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
@@ -183,21 +183,21 @@
thm_names =
if String.isSubstring set_ClauseFormulaRelationN output then
(* This is a hack required for keeping track of axioms after they have been
- clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part
- of this hack. *)
+ clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also
+ part of this hack. *)
let
val j0 = hd (hd conjecture_shape)
val seq = extract_clause_sequence output
val name_map = extract_clause_formula_relation output
fun renumber_conjecture j =
- AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0))
+ conjecture_prefix ^ Int.toString (j - j0)
+ |> AList.find (fn (s, ss) => member (op =) ss s) name_map
|> map (fn s => find_index (curry (op =) s) seq + 1)
in
(conjecture_shape |> map (maps renumber_conjecture),
- seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the
- |> try (unprefix axiom_prefix) of
- SOME s' => undo_ascii_of s'
- | NONE => "")
+ seq |> map (AList.lookup (op =) name_map #> these
+ #> map_filter (try (unprefix axiom_prefix))
+ #> map undo_ascii_of #> space_implode " ")
|> Vector.fromList)
end
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 11:18:24 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Aug 18 12:05:44 2010 +0200
@@ -55,8 +55,10 @@
let
val do_term = combterm_from_term thy
fun do_quant bs q s T t' =
- do_formula ((s, T) :: bs) t'
- #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ let val s = Name.variant (map fst bs) s in
+ do_formula ((s, T) :: bs) t'
+ #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+ end
and do_conn bs c t1 t2 =
do_formula bs t1 ##>> do_formula bs t2
#>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))