# HG changeset patch # User blanchet # Date 1287999725 -7200 # Node ID be8acf6e63bb247a688912fd56e31deb0e693c1f # Parent 80b7f456600ff8244a8274b31b3f2d5ac526985a# Parent ea388cb9bc57d9310ae4411b7a0b4f4e5a237f7e merged diff -r 80b7f456600f -r be8acf6e63bb NEWS --- a/NEWS Mon Oct 25 10:45:22 2010 +0200 +++ b/NEWS Mon Oct 25 11:42:05 2010 +0200 @@ -278,6 +278,9 @@ meson_disj_FalseD2 ~> Meson.disj_FalseD2 INCOMPATIBILITY. +* Auto Solve: Renamed "Auto Solve Direct". The tool is now available manually as + "solve_direct". + * Sledgehammer: - Renamed lemmas: COMBI_def ~> Meson.COMBI_def diff -r 80b7f456600f -r be8acf6e63bb etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Oct 25 10:45:22 2010 +0200 +++ b/etc/isar-keywords.el Mon Oct 25 11:42:05 2010 +0200 @@ -220,6 +220,7 @@ "sledgehammer" "sledgehammer_params" "smt_status" + "solve_direct" "sorry" "specification" "statespace" @@ -392,6 +393,7 @@ "refute" "sledgehammer" "smt_status" + "solve_direct" "term" "thm" "thm_deps" diff -r 80b7f456600f -r be8acf6e63bb src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Oct 25 11:42:05 2010 +0200 @@ -122,7 +122,6 @@ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ $(SRC)/Tools/IsaPlanner/zipper.ML \ $(SRC)/Tools/atomize_elim.ML \ - $(SRC)/Tools/auto_solve.ML \ $(SRC)/Tools/auto_tools.ML \ $(SRC)/Tools/coherent.ML \ $(SRC)/Tools/cong_tac.ML \ @@ -134,6 +133,7 @@ $(SRC)/Tools/nbe.ML \ $(SRC)/Tools/project_rule.ML \ $(SRC)/Tools/quickcheck.ML \ + $(SRC)/Tools/solve_direct.ML \ $(SRC)/Tools/value.ML \ HOL.thy \ Tools/hologic.ML \ diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Oct 25 11:42:05 2010 +0200 @@ -364,7 +364,7 @@ val problem = {state = st', goal = goal, subgoal = i, subgoal_count = Sledgehammer_Util.subgoal_count st, - axioms = axioms |> map Sledgehammer.Unprepared, only = true} + axioms = axioms |> map Sledgehammer.Untranslated, only = true} val time_limit = (case hard_timeout of NONE => I diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Oct 25 11:42:05 2010 +0200 @@ -12,7 +12,7 @@ type locality = Sledgehammer_Filter.locality type relevance_fudge = Sledgehammer_Filter.relevance_fudge type relevance_override = Sledgehammer_Filter.relevance_override - type prepared_formula = Sledgehammer_ATP_Translate.prepared_formula + type translated_formula = Sledgehammer_ATP_Translate.translated_formula type minimize_command = Sledgehammer_ATP_Reconstruct.minimize_command type params = @@ -31,8 +31,8 @@ expect: string} datatype axiom = - Unprepared of (string * locality) * thm | - Prepared of term * ((string * locality) * prepared_formula) option + Untranslated of (string * locality) * thm | + Translated of term * ((string * locality) * translated_formula) option type prover_problem = {state: Proof.state, @@ -195,8 +195,8 @@ expect: string} datatype axiom = - Unprepared of (string * locality) * thm | - Prepared of term * ((string * locality) * prepared_formula) option + Untranslated of (string * locality) * thm | + Translated of term * ((string * locality) * translated_formula) option type prover_problem = {state: Proof.state, @@ -250,10 +250,10 @@ (* generic TPTP-based ATPs *) -fun dest_Unprepared (Unprepared p) = p - | dest_Unprepared (Prepared _) = raise Fail "dest_Unprepared" -fun prepared_axiom ctxt (Unprepared p) = prepare_axiom ctxt p - | prepared_axiom _ (Prepared p) = p +fun dest_Untranslated (Untranslated p) = p + | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated" +fun translated_axiom ctxt (Untranslated p) = translate_axiom ctxt p + | translated_axiom _ (Translated p) = p fun int_option_add (SOME m) (SOME n) = SOME (m + n) | int_option_add _ _ = NONE @@ -275,7 +275,7 @@ val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal val axioms = axioms |> not only ? take (the_default default_max_relevant max_relevant) - |> map (prepared_axiom ctxt) + |> map (translated_axiom ctxt) val dest_dir = if overlord then getenv "ISABELLE_HOME_USER" else Config.get ctxt dest_dir val problem_prefix = Config.get ctxt problem_prefix @@ -418,7 +418,7 @@ let val {outcome, used_axioms, run_time_in_msecs} = saschas_run_smt_solver remote timeout state - (map_filter (try dest_Unprepared) axioms) subgoal + (map_filter (try dest_Untranslated) axioms) subgoal val message = if outcome = NONE then try_command_line (proof_banner false) @@ -507,8 +507,8 @@ val _ = () |> not blocking ? kill_provers val _ = if auto then () else priority "Sledgehammering..." val (smts, atps) = provers |> List.partition is_smt_prover - fun run_provers full_types irrelevant_consts relevance_fudge maybe_prepare - provers (res as (success, state)) = + fun run_provers full_types irrelevant_consts relevance_fudge + maybe_translate provers (res as (success, state)) = if success orelse null provers then res else @@ -524,7 +524,7 @@ relevant_facts ctxt full_types relevance_thresholds max_max_relevant irrelevant_consts relevance_fudge relevance_override chained_ths hyp_ts concl_t - |> map maybe_prepare + |> map maybe_translate val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, axioms = axioms, only = only} @@ -541,9 +541,9 @@ end val run_atps = run_provers full_types atp_irrelevant_consts atp_relevance_fudge - (Prepared o prepare_axiom ctxt) atps + (Translated o translate_axiom ctxt) atps val run_smts = - run_provers true smt_irrelevant_consts smt_relevance_fudge Unprepared + run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated smts fun run_atps_and_smt_solvers () = [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ()) diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon Oct 25 11:42:05 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Oct 25 11:42:05 2010 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/Sledgehammer/sledgehammer_translate.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen @@ -9,16 +9,16 @@ signature SLEDGEHAMMER_ATP_TRANSLATE = sig type 'a problem = 'a ATP_Problem.problem - type prepared_formula + type translated_formula val axiom_prefix : string val conjecture_prefix : string - val prepare_axiom : + val translate_axiom : Proof.context -> (string * 'a) * thm - -> term * ((string * 'a) * prepared_formula) option + -> term * ((string * 'a) * translated_formula) option val prepare_atp_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term - -> (term * ((string * 'a) * prepared_formula) option) list + -> (term * ((string * 'a) * translated_formula) option) list -> string problem * string Symtab.table * int * (string * 'a) list vector end; @@ -39,7 +39,7 @@ (* Freshness almost guaranteed! *) val sledgehammer_weak_prefix = "Sledgehammer:" -type prepared_formula = +type translated_formula = {name: string, kind: kind, combformula: (name, combterm) formula, @@ -214,7 +214,7 @@ fun count_combformula (AQuant (_, _, phi)) = count_combformula phi | count_combformula (AConn (_, phis)) = fold count_combformula phis | count_combformula (AAtom tm) = count_combterm tm -fun count_prepared_formula ({combformula, ...} : prepared_formula) = +fun count_translated_formula ({combformula, ...} : translated_formula) = count_combformula combformula val optional_helpers = @@ -235,7 +235,7 @@ fun get_helper_facts ctxt is_FO full_types conjectures axioms = let val ct = - fold (fold count_prepared_formula) [conjectures, axioms] init_counters + fold (fold count_translated_formula) [conjectures, axioms] init_counters fun is_needed c = the (Symtab.lookup ct c) > 0 fun baptize th = ((Thm.get_name_hint th, false), th) in @@ -247,12 +247,12 @@ |> map_filter (Option.map snd o make_axiom ctxt false) end -fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax) +fun translate_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax) -fun prepare_formulas ctxt full_types hyp_ts concl_t axioms = +fun translate_formulas ctxt full_types hyp_ts concl_t axioms = let val thy = ProofContext.theory_of ctxt - val (axiom_ts, prepared_axioms) = ListPair.unzip axioms + val (axiom_ts, translated_axioms) = ListPair.unzip axioms (* Remove existing axioms from the conjecture, as this can dramatically boost an ATP's performance (for some reason). *) val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts) @@ -263,7 +263,7 @@ val tycons = type_consts_of_terms thy (goal_t :: axiom_ts) (* TFrees in the conjecture; TVars in the axioms *) val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) - val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms) + val (axiom_names, axioms) = ListPair.unzip (map_filter I translated_axioms) val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' @@ -323,7 +323,7 @@ in aux end fun formula_for_axiom full_types - ({combformula, ctypes_sorts, ...} : prepared_formula) = + ({combformula, ctypes_sorts, ...} : translated_formula) = mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) (type_literals_for_types ctypes_sorts)) (formula_for_combformula full_types combformula) @@ -353,11 +353,12 @@ (fo_literal_for_arity_literal conclLit))) fun problem_line_for_conjecture full_types - ({name, kind, combformula, ...} : prepared_formula) = + ({name, kind, combformula, ...} : translated_formula) = Fof (conjecture_prefix ^ name, kind, formula_for_combformula full_types combformula) -fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : prepared_formula) = +fun free_type_literals_for_conjecture + ({ctypes_sorts, ...} : translated_formula) = map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts) fun problem_line_for_free_type j lit = @@ -501,7 +502,7 @@ val thy = ProofContext.theory_of ctxt val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) = - prepare_formulas ctxt full_types hyp_ts concl_t axioms + translate_formulas ctxt full_types hyp_ts concl_t axioms val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms val helper_lines = map (problem_line_for_fact helper_prefix full_types) helper_facts diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Oct 25 11:42:05 2010 +0200 @@ -157,13 +157,15 @@ prover :: avoid_too_many_local_threads thy n provers end +val num_processors = try Thread.numProcessors #> the_default 1 + (* The first ATP of the list is used by Auto Sledgehammer. Because of the low timeout, it makes sense to put SPASS first. *) fun default_provers_param_value ctxt = let val thy = ProofContext.theory_of ctxt in [spassN, eN, vampireN, sine_eN (* FIXME: , smtN *)] |> map_filter (remotify_prover_if_not_installed ctxt) - |> avoid_too_many_local_threads thy (Thread.numProcessors ()) + |> avoid_too_many_local_threads thy (num_processors ()) |> space_implode " " end diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Oct 25 11:42:05 2010 +0200 @@ -55,7 +55,7 @@ max_relevant = NONE, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""} val axioms = - axioms |> maps (fn (n, ths) => ths |> map (Unprepared o pair n)) + axioms |> maps (fn (n, ths) => ths |> map (Untranslated o pair n)) val {goal, ...} = Proof.goal state val problem = {state = state, goal = goal, subgoal = i, subgoal_count = n, diff -r 80b7f456600f -r be8acf6e63bb src/HOL/Tools/try.ML --- a/src/HOL/Tools/try.ML Mon Oct 25 10:45:22 2010 +0200 +++ b/src/HOL/Tools/try.ML Mon Oct 25 11:42:05 2010 +0200 @@ -40,6 +40,7 @@ SOME (x, _) => nprems_of (post x) < nprems_of goal | NONE => false end + handle TimeLimit.TimeOut => false fun do_generic timeout_opt command pre post apply st = let val timer = Timer.startRealTimer () in @@ -52,15 +53,6 @@ fun named_method thy name = Method.method thy (Args.src ((name, []), Position.none)) -fun apply_named_method name ctxt = - let val thy = ProofContext.theory_of ctxt in - Method.apply (named_method thy name) ctxt [] - end - -fun do_named_method name timeout_opt st = - do_generic timeout_opt name (#goal o Proof.goal) snd - (apply_named_method name (Proof.context_of st)) st - fun apply_named_method_on_first_goal name ctxt = let val thy = ProofContext.theory_of ctxt in Proof.refine (Method.SelectGoals (1, Method.Basic (named_method thy name))) @@ -77,7 +69,8 @@ val named_methods = [("simp", false), ("auto", true), ("fast", false), ("fastsimp", false), - ("force", false), ("blast", false), ("arith", false)] + ("force", false), ("blast", false), ("metis", false), ("linarith", false), + ("presburger", false)] val do_methods = map do_named_method named_methods fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms" diff -r 80b7f456600f -r be8acf6e63bb src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Mon Oct 25 10:45:22 2010 +0200 +++ b/src/Tools/Code_Generator.thy Mon Oct 25 11:42:05 2010 +0200 @@ -9,7 +9,7 @@ uses "~~/src/Tools/cache_io.ML" "~~/src/Tools/auto_tools.ML" - "~~/src/Tools/auto_solve.ML" + "~~/src/Tools/solve_direct.ML" "~~/src/Tools/quickcheck.ML" "~~/src/Tools/value.ML" "~~/src/Tools/Code/code_preproc.ML" @@ -26,7 +26,7 @@ begin setup {* - Auto_Solve.setup + Solve_Direct.setup #> Code_Preproc.setup #> Code_Simp.setup #> Code_ML.setup diff -r 80b7f456600f -r be8acf6e63bb src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Mon Oct 25 10:45:22 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -(* Title: Tools/auto_solve.ML - Author: Timothy Bourke and Gerwin Klein, NICTA - -Check whether a newly stated theorem can be solved directly by an -existing theorem. Duplicate lemmas can be detected in this way. - -The implementation relies critically on the Find_Theorems solves -feature. -*) - -signature AUTO_SOLVE = -sig - val auto : bool Unsynchronized.ref - val max_solutions : int Unsynchronized.ref - val setup : theory -> theory -end; - -structure Auto_Solve : AUTO_SOLVE = -struct - -(* preferences *) - -val auto = Unsynchronized.ref false; -val max_solutions = Unsynchronized.ref 5; - -val _ = - ProofGeneralPgip.add_preference Preferences.category_tracing - (Unsynchronized.setmp auto true (fn () => - Preferences.bool_pref auto - "auto-solve" "Try to solve conjectures with existing theorems.") ()); - - -(* hook *) - -fun auto_solve state = - let - val ctxt = Proof.context_of state; - - val crits = [(true, Find_Theorems.Solves)]; - fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits); - - fun prt_result (goal, results) = - let - val msg = - (case goal of - NONE => "The current goal" - | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); - in - Pretty.big_list - (msg ^ " could be solved directly with:") - (map (Find_Theorems.pretty_thm ctxt) results) - end; - - fun seek_against_goal () = - (case try Proof.simple_goal state of - NONE => NONE - | SOME {goal = st, ...} => - let - val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); - val rs = - if length subgoals = 1 - then [(NONE, find st)] - else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; - val results = filter_out (null o snd) rs; - in if null results then NONE else SOME results end); - - fun go () = - (case try seek_against_goal () of - SOME (SOME results) => - (true, state |> Proof.goal_message - (fn () => Pretty.chunks - [Pretty.str "", - Pretty.markup Markup.hilite - (separate (Pretty.brk 0) (map prt_result results))])) - | _ => (false, state)); - in if not (!auto) then (false, state) else go () end; - -val setup = Auto_Tools.register_tool ("solve", auto_solve) - -end; diff -r 80b7f456600f -r be8acf6e63bb src/Tools/solve_direct.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/solve_direct.ML Mon Oct 25 11:42:05 2010 +0200 @@ -0,0 +1,97 @@ +(* Title: Tools/solve_direct.ML + Author: Timothy Bourke and Gerwin Klein, NICTA + +Check whether a newly stated theorem can be solved directly by an +existing theorem. Duplicate lemmas can be detected in this way. + +The implementation relies critically on the Find_Theorems solves +feature. +*) + +signature SOLVE_DIRECT = +sig + val auto : bool Unsynchronized.ref + val max_solutions : int Unsynchronized.ref + val setup : theory -> theory +end; + +structure Solve_Direct : SOLVE_DIRECT = +struct + +val solve_directN = "solve_direct" + +(* preferences *) + +val auto = Unsynchronized.ref false; +val max_solutions = Unsynchronized.ref 5; + +val _ = + ProofGeneralPgip.add_preference Preferences.category_tracing + (Unsynchronized.setmp auto true (fn () => + Preferences.bool_pref auto + ("Auto " ^ solve_directN) + ("Run " ^ quote solve_directN ^ " automatically.")) ()); + +fun solve_direct auto state = + let + val ctxt = Proof.context_of state; + + val crits = [(true, Find_Theorems.Solves)]; + fun find g = snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits); + + fun prt_result (goal, results) = + let + val msg = + (if auto then "Auto " else "") ^ solve_directN ^ ": " ^ + (case goal of + NONE => "The current goal" + | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg)); + in + Pretty.big_list + (msg ^ " can be solved directly with") + (map (Find_Theorems.pretty_thm ctxt) results) + end; + + fun seek_against_goal () = + (case try Proof.simple_goal state of + NONE => NONE + | SOME {goal = st, ...} => + let + val subgoals = Drule.strip_imp_prems (Thm.cprop_of st); + val rs = + if length subgoals = 1 + then [(NONE, find st)] + else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals; + val results = filter_out (null o snd) rs; + in if null results then NONE else SOME results end); + fun message results = separate (Pretty.brk 0) (map prt_result results) + in + (case try seek_against_goal () of + SOME (SOME results) => + (true, state |> (if auto then + Proof.goal_message + (fn () => Pretty.chunks + [Pretty.str "", + Pretty.markup Markup.hilite (message results)]) + else + tap (fn _ => priority (Pretty.string_of + (Pretty.chunks (message results)))))) + | _ => (false, state)) + end; + +val invoke_solve_direct = fst o solve_direct false + +val _ = + Outer_Syntax.improper_command solve_directN + "try to solve conjectures directly with existing theorems" Keyword.diag + (Scan.succeed (Toplevel.keep (K () o invoke_solve_direct + o Toplevel.proof_of))) + +(* hook *) + +fun auto_solve_direct state = + if not (!auto) then (false, state) else solve_direct true state + +val setup = Auto_Tools.register_tool (solve_directN, auto_solve_direct) + +end;