# HG changeset patch # User blanchet # Date 1283514879 -7200 # Node ID 91ba394cc5258625506cbcf6fe0a7301f2df5b82 # Parent 3b9e020c3908026d5c746fc24f04998cc1a4fc9f# Parent 611e41ef07c31e4f552491c99e77f8d3ad53f0d7 merged diff -r 3b9e020c3908 -r 91ba394cc525 Admin/isatest/settings/cygwin-poly-e --- 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" diff -r 3b9e020c3908 -r 91ba394cc525 src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r 3b9e020c3908 -r 91ba394cc525 src/HOL/Tools/Sledgehammer/clausifier.ML --- 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 diff -r 3b9e020c3908 -r 91ba394cc525 src/HOL/Tools/Sledgehammer/metis_tactics.ML --- 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 diff -r 3b9e020c3908 -r 91ba394cc525 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 diff -r 3b9e020c3908 -r 91ba394cc525 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 *)