--- 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
--- 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"
--- 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 \
--- 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
--- 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 ())
--- 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
--- 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
--- 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
--- 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,
--- 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"
--- 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
--- 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;
--- /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;