--- a/Admin/isatest/settings/cygwin-poly-e Fri Sep 03 12:01:47 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e Fri Sep 03 13:54:39 2010 +0200
@@ -24,4 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
-init_component "$HOME/contrib_devel/kodkodi"
+unset KODKODI
+#init_component "$HOME/contrib_devel/kodkodi"
--- a/src/HOL/Tools/ATP/atp_problem.ML Fri Sep 03 12:01:47 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Sep 03 13:54:39 2010 +0200
@@ -111,9 +111,10 @@
fun pool_map f xs =
pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
-(* "equal" is reserved by some ATPs. "op" is also reserved, to avoid the
- unreadable "op_1", "op_2", etc., in the problem files. *)
-val reserved_nice_names = ["equal", "op"]
+(* "op" is also reserved, to avoid the unreadable "op_1", "op_2", etc., in the
+ problem files. "equal" is reserved by some ATPs. "eq" is reserved to ensure
+ that "HOL.eq" is correctly mapped to equality. *)
+val reserved_nice_names = ["op", "equal", "eq"]
fun readable_name full_name s =
if s = full_name then
s
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Sep 03 12:01:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Fri Sep 03 13:54:39 2010 +0200
@@ -241,7 +241,7 @@
let
val ctxt0 = Variable.global_thm_context th
val (nnf_th, ctxt) = to_nnf th ctxt0
- val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
+ val def_th = (* FIXME: to_definitional_cnf_with_quantifiers thy *) nnf_th
val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
in
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 03 12:01:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Sep 03 13:54:39 2010 +0200
@@ -798,6 +798,7 @@
val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
+val timer = Timer.startRealTimer () (*###*)
in
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
@@ -806,6 +807,9 @@
(maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
+|> tap (fn _ => priority (" METIS " ^
+cat_lines (map (Display.string_of_thm ctxt) ths) ^
+string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ " ms")) (*###*)
end
val metis_tac = generic_metis_tac HO
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 03 12:01:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Sep 03 13:54:39 2010 +0200
@@ -133,15 +133,29 @@
|> Exn.release
|> tap (after path)
+fun extract_delimited (begin_delim, end_delim) output =
+ output |> first_field begin_delim |> the |> snd
+ |> first_field end_delim |> the |> fst
+ |> first_field "\n" |> the |> snd
+ handle Option.Option => ""
+
+val tstp_important_message_delims =
+ ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
+
+fun extract_important_message output =
+ case extract_delimited tstp_important_message_delims output of
+ "" => ""
+ | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
+ |> map (perhaps (try (unprefix "%")))
+ |> map (perhaps (try (unprefix " ")))
+ |> space_implode "\n " |> quote
+
(* Splits by the first possible of a list of delimiters. *)
fun extract_proof delims output =
case pairself (find_first (fn s => String.isSubstring s output))
(ListPair.unzip delims) of
(SOME begin_delim, SOME end_delim) =>
- (output |> first_field begin_delim |> the |> snd
- |> first_field end_delim |> the |> fst
- |> first_field "\n" |> the |> snd
- handle Option.Option => "")
+ extract_delimited (begin_delim, end_delim) output
| _ => ""
fun extract_proof_and_outcome complete res_code proof_delims known_failures
@@ -325,6 +339,7 @@
val (conjecture_shape, axiom_names) =
repair_conjecture_shape_and_theorem_names output conjecture_shape
axiom_names
+ val important_message = extract_important_message output
val (message, used_thm_names) =
case outcome of
NONE =>
@@ -335,7 +350,12 @@
message ^ (if verbose then
"\nReal CPU time: " ^ string_of_int msecs ^ " ms."
else
- ""))
+ "") ^
+ (if important_message <> "" then
+ "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^
+ important_message
+ else
+ ""))
| SOME failure => (string_for_failure failure, [])
in
{outcome = outcome, message = message, pool = pool,
@@ -346,14 +366,23 @@
fun get_prover_fun thy name = prover_fun name (get_prover thy name)
-fun run_prover ctxt (params as {blocking, timeout, expect, ...}) i n
- relevance_override minimize_command
- (problem as {goal, ...}) (prover, atp_name) =
+fun run_prover ctxt (params as {blocking, verbose, max_relevant, timeout,
+ expect, ...})
+ i n relevance_override minimize_command
+ (problem as {goal, axioms, ...})
+ (prover as {default_max_relevant, ...}, atp_name) =
let
val birth_time = Time.now ()
val death_time = Time.+ (birth_time, timeout)
+ val max_relevant = the_default default_max_relevant max_relevant
+ val num_axioms = Int.min (length axioms, max_relevant)
val desc =
- "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":" ^
+ "ATP " ^ quote atp_name ^
+ (if verbose then
+ " with " ^ string_of_int num_axioms ^ " fact" ^ plural_s num_axioms
+ else
+ "") ^
+ " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
(if blocking then
""
else
@@ -389,15 +418,15 @@
0 => priority "No subgoal!"
| n =>
let
+ val thy = Proof.theory_of state
val timer = Timer.startRealTimer ()
val _ = () |> not blocking ? kill_atps
val _ = priority "Sledgehammering..."
+ val provers = map (`(get_prover thy)) atps
fun run () =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal state
- val thy = Proof.theory_of state
val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val provers = map (`(get_prover thy)) atps
val max_max_relevant =
case max_relevant of
SOME n => n
@@ -411,11 +440,6 @@
{ctxt = ctxt, goal = goal, subgoal = i,
axioms = map (prepare_axiom ctxt) axioms}
val num_axioms = length axioms
- val _ = if verbose then
- priority ("Selected " ^ string_of_int num_axioms ^
- " fact" ^ plural_s num_axioms ^ ".")
- else
- ()
val _ =
(if blocking then Par_List.map else map)
(run_prover ctxt params i n relevance_override
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 03 12:01:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 03 13:54:39 2010 +0200
@@ -315,8 +315,13 @@
| _ => raise FO_TERM us
else case strip_prefix_and_unascii const_prefix a of
SOME "equal" =>
- list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT),
- map (aux NONE []) us)
+ let val ts = map (aux NONE []) us in
+ if length ts = 2 andalso hd ts aconv List.last ts then
+ (* Vampire is keen on producing these. *)
+ @{const True}
+ else
+ list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+ end
| SOME b =>
let
val c = invert_const b
@@ -526,11 +531,6 @@
fun is_bad_free frees (Free x) = not (member (op =) frees x)
| is_bad_free _ _ = false
-(* Vampire is keen on producing these. *)
-fun is_trivial_formula (@{const Not} $ (Const (@{const_name HOL.eq}, _)
- $ t1 $ t2)) = (t1 aconv t2)
- | is_trivial_formula _ = false
-
fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
(j, line :: map (replace_deps_in_line (num, [])) lines)
| add_desired_line isar_shrink_factor conjecture_shape axiom_names frees
@@ -541,7 +541,6 @@
(not (is_only_type_information t) andalso
null (Term.add_tvars t []) andalso
not (exists_subterm (is_bad_free frees) t) andalso
- not (is_trivial_formula t) andalso
(null lines orelse (* last line must be kept *)
(length deps >= 2 andalso j mod isar_shrink_factor = 0))) then
Inference (num, t, deps) :: lines (* keep line *)