--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sun May 22 14:51:42 2011 +0200
@@ -383,6 +383,8 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover_name
+ val is_good_prop =
+ Sledgehammer_Provers.is_good_prop_for_prover ctxt prover_name
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
val relevance_fudge =
@@ -399,8 +401,9 @@
let
val facts =
Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ (the_default default_max_relevant max_relevant) is_good_prop
+ is_built_in_const relevance_fudge relevance_override chained_ths
+ hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Sun May 22 14:51:42 2011 +0200
@@ -118,6 +118,8 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover
+ val is_good_prop =
+ Sledgehammer_Provers.is_good_prop_for_prover ctxt default_prover
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
@@ -128,8 +130,9 @@
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override facts hyp_ts concl_t
+ (the_default default_max_relevant max_relevant) is_good_prop
+ is_built_in_const relevance_fudge relevance_override facts hyp_ts
+ concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
flat proofs |> sort_distinct string_ord
--- a/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 22 14:51:42 2011 +0200
@@ -35,6 +35,7 @@
val mk_aconn :
connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
-> ('a, 'b, 'c) formula
+ val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
val timestamp : unit -> string
val hashw : word * word -> word
val hashw_string : string * word -> word
@@ -82,6 +83,10 @@
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
+fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
+ | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
+ | formula_map f (AAtom tm) = AAtom (f tm)
+
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
(* This hash function is recommended in Compilers: Principles, Techniques, and
@@ -172,19 +177,22 @@
(Formula (_, _, AAtom (ATerm (("equal", _), _)), _, _)) = true
| is_problem_line_cnf_ueq _ = false
-fun open_formula (AQuant (AForall, _, phi)) = open_formula phi
- | open_formula phi = phi
-fun open_non_conjecture_line (line as Formula (_, Conjecture, _, _, _)) = line
- | open_non_conjecture_line (Formula (ident, kind, phi, source, info)) =
- Formula (ident, kind, open_formula phi, source, info)
- | open_non_conjecture_line line = line
+fun open_conjecture_term (ATerm ((s, s'), tms)) =
+ ATerm (s |> is_atp_variable s ? Name.desymbolize false |> `I,
+ tms |> map open_conjecture_term)
+fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi
+ | open_formula true (AAtom t) = AAtom (open_conjecture_term t)
+ | open_formula _ phi = phi
+fun open_formula_line (Formula (ident, kind, phi, source, info)) =
+ Formula (ident, kind, open_formula (kind = Conjecture) phi, source, info)
+ | open_formula_line line = line
fun negate_conjecture_line (Formula (ident, Conjecture, phi, source, info)) =
Formula (ident, Hypothesis, mk_anot phi, source, info)
| negate_conjecture_line line = line
val filter_cnf_ueq_problem =
- map (apsnd (map open_non_conjecture_line
+ map (apsnd (map open_formula_line
#> filter is_problem_line_cnf_ueq
#> map negate_conjecture_line))
#> (fn problem =>
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 22 14:51:42 2011 +0200
@@ -419,8 +419,9 @@
[TFF, FOF] (K (250, ["simple"]) (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
- [("#START OF PROOF", "Proved Goals:")] [] Hypothesis Hypothesis
- [CNF_UEQ] (K (500, ["poly_args"]) (* FUDGE *))
+ [("#START OF PROOF", "Proved Goals:")]
+ [(OutOfResources, "Too many function symbols")] Hypothesis
+ Hypothesis [CNF_UEQ] (K (100, ["poly_args"]) (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun May 22 14:51:42 2011 +0200
@@ -38,7 +38,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
- the conclusion variable to False. (Cf. "transform_elim_term" in
+ the conclusion variable to False. (Cf. "transform_elim_prop" in
"Sledgehammer_Util".) *)
fun transform_elim_theorem th =
case concl_of th of (*conclusion variable*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 22 14:51:42 2011 +0200
@@ -176,10 +176,6 @@
is_type_level_virtually_sound level orelse level = Finite_Types
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
-fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
- | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
- | formula_map f (AAtom tm) = AAtom (f tm)
-
fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
| aconn_fold pos f (AImplies, [phi1, phi2]) =
f (Option.map not pos) phi1 #> f pos phi2
@@ -452,7 +448,7 @@
let
val thy = Proof_Context.theory_of ctxt
val t = t |> Envir.beta_eta_contract
- |> transform_elim_term
+ |> transform_elim_prop
|> Object_Logic.atomize_term thy
val need_trueprop = (fastype_of t = @{typ bool})
val t = t |> need_trueprop ? HOLogic.mk_Trueprop
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 22 14:51:42 2011 +0200
@@ -44,13 +44,13 @@
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
val all_facts :
- Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list
- -> (((unit -> string) * locality) * (bool * thm)) list
+ Proof.context -> 'a Symtab.table -> bool -> (term -> bool) -> thm list
+ -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
val const_names_in_fact :
theory -> (string * typ -> term list -> bool * term list) -> term
-> string list
val relevant_facts :
- Proof.context -> real * real -> int
+ Proof.context -> real * real -> int -> (term -> bool)
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
-> relevance_override -> thm list -> term list -> term
-> ((string * locality) * thm) list
@@ -785,11 +785,12 @@
(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
-fun is_theorem_bad_for_atps thm =
+fun is_theorem_bad_for_atps is_good_prop thm =
let val t = prop_of thm in
- is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
- exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
- is_metastrange_theorem thm orelse is_that_fact thm
+ not (is_good_prop t) orelse is_formula_too_complex t orelse
+ exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
+ exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
+ is_that_fact thm
end
fun meta_equify (@{const Trueprop}
@@ -814,7 +815,7 @@
mk_fact_table normalize_simp_prop snd simps)
end
-fun all_facts ctxt reserved really_all add_ths chained_ths =
+fun all_facts ctxt reserved really_all is_good_prop add_ths chained_ths =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -868,7 +869,7 @@
pair 1
#> fold (fn th => fn (j, rest) =>
(j + 1,
- if is_theorem_bad_for_atps th andalso
+ if is_theorem_bad_for_atps is_good_prop th andalso
not (member Thm.eq_thm add_ths th) then
rest
else
@@ -902,9 +903,9 @@
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
-fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
- fudge (override as {add, only, ...}) chained_ths hyp_ts
- concl_t =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_good_prop
+ is_built_in_const fudge (override as {add, only, ...})
+ chained_ths hyp_ts concl_t =
let
val thy = Proof_Context.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -920,7 +921,7 @@
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o fact_from_ref ctxt reserved chained_ths) add
else
- all_facts ctxt reserved false add_ths chained_ths)
+ all_facts ctxt reserved false is_good_prop add_ths chained_ths)
|> Config.get ctxt instantiate_inducts
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
|> rearrange_facts ctxt only
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun May 22 14:51:42 2011 +0200
@@ -183,7 +183,7 @@
(* 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 =
- [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
+ [spassN, eN, vampireN, sine_eN, waldmeisterN, SMT_Solver.solver_name_of ctxt]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
|> implode_param
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Sun May 22 14:51:42 2011 +0200
@@ -71,9 +71,12 @@
val das_Tool : string
val select_smt_solver : string -> Proof.context -> Proof.context
val is_smt_prover : Proof.context -> string -> bool
+ val is_unit_equational_atp : Proof.context -> string -> bool
val is_prover_supported : Proof.context -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
val default_max_relevant_for_prover : Proof.context -> bool -> string -> int
+ val is_unit_equality : term -> bool
+ val is_good_prop_for_prover : Proof.context -> string -> term -> bool
val is_built_in_const_for_prover :
Proof.context -> string -> string * typ -> term list -> bool * term list
val atp_relevance_fudge : relevance_fudge
@@ -120,6 +123,13 @@
fun is_smt_prover ctxt name =
member (op =) (SMT_Solver.available_solvers_of ctxt) name
+fun is_unit_equational_atp ctxt name =
+ let val thy = Proof_Context.theory_of ctxt in
+ case try (get_atp thy) name of
+ SOME {formats, ...} => member (op =) formats CNF_UEQ
+ | NONE => false
+ end
+
fun is_prover_supported ctxt name =
let val thy = Proof_Context.theory_of ctxt in
is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
@@ -147,6 +157,20 @@
@{const_name conj}, @{const_name disj}, @{const_name implies},
@{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
+fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
+ | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
+ is_unit_equality t
+ | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
+ is_unit_equality t
+ | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ _ $ _) =
+ T <> @{typ bool}
+ | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ _ $ _) =
+ T <> @{typ bool}
+ | is_unit_equality _ = false
+
+fun is_good_prop_for_prover ctxt name =
+ if is_unit_equational_atp ctxt name then is_unit_equality else K true
+
fun is_built_in_const_for_prover ctxt name =
if is_smt_prover ctxt name then
let val ctxt = ctxt |> select_smt_solver name in
@@ -390,8 +414,8 @@
(* Facts containing variables of type "unit" or "bool" or of the form
"ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
are omitted. *)
-fun is_dangerous_term ctxt =
- transform_elim_term
+fun is_dangerous_prop ctxt =
+ transform_elim_prop
#> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf
is_exhaustive_finite)
@@ -413,13 +437,13 @@
(* We could return (TFF, type_sys) in all cases but this would require the
TFF provers to accept problems in which constants are implicitly
declared. Today neither SNARK nor ToFoF-E satisfy this criterion. *)
- if member (op =) formats FOF then
- (FOF, type_sys)
- else if member (op =) formats CNF_UEQ then
+ if member (op =) formats CNF_UEQ then
(CNF_UEQ, case type_sys of
Tags _ => type_sys
| _ => Preds (polymorphism_of_type_sys type_sys,
Const_Arg_Types, Light))
+ else if member (op =) formats FOF then
+ (FOF, type_sys)
else
(TFF, Simple_Types All_Types)
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
@@ -514,7 +538,7 @@
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> not fairly_sound
- ? filter_out (is_dangerous_term ctxt o prop_of o snd
+ ? filter_out (is_dangerous_prop ctxt o prop_of o snd
o untranslated_fact)
|> take num_facts
|> not (null blacklist)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 22 14:51:42 2011 +0200
@@ -189,7 +189,9 @@
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
val _ = print "Sledgehammering..."
- val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
+ val (smts, (ueq_atps, full_atps)) =
+ provers |> List.partition (is_smt_prover ctxt)
+ ||> List.partition (is_unit_equational_atp ctxt)
fun launch_provers state get_facts translate maybe_smt_filter provers =
let
val facts = get_facts ()
@@ -212,7 +214,7 @@
|> (if blocking then smart_par_list_map else map) (launch problem)
|> exists fst |> rpair state
end
- fun get_facts label relevance_fudge provers =
+ fun get_facts label is_good_prop relevance_fudge provers =
let
val max_max_relevant =
case max_relevant of
@@ -225,7 +227,7 @@
val is_built_in_const =
is_built_in_const_for_prover ctxt (hd provers)
in
- relevant_facts ctxt relevance_thresholds max_max_relevant
+ relevant_facts ctxt relevance_thresholds max_max_relevant is_good_prop
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
|> tap (fn facts =>
@@ -241,18 +243,19 @@
else
())
end
- fun launch_atps accum =
- if null atps then
+ fun launch_atps label is_good_prop atps accum =
+ if null atps orelse not (is_good_prop concl_t) then
accum
else
- launch_provers state (get_facts "ATP" atp_relevance_fudge o K atps)
- (K (Untranslated_Fact o fst)) (K (K NONE)) atps
+ launch_provers state
+ (get_facts label is_good_prop atp_relevance_fudge o K atps)
+ (K (Untranslated_Fact o fst)) (K (K NONE)) atps
fun launch_smts accum =
if null smts then
accum
else
let
- val facts = get_facts "SMT solver" smt_relevance_fudge smts
+ val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
fun smt_filter facts =
(if debug then curry (op o) SOME
@@ -264,14 +267,19 @@
|> map (launch_provers state (K facts) weight smt_filter o snd)
|> exists fst |> rpair state
end
+ val launch_full_atps = launch_atps "ATP" (K true) full_atps
+ val launch_ueq_atps =
+ launch_atps "Unit equational provers" is_unit_equality ueq_atps
fun launch_atps_and_smt_solvers () =
- [launch_atps, launch_smts]
+ [launch_full_atps, launch_ueq_atps, launch_smts]
|> smart_par_list_map (fn f => f (false, state) |> K ())
handle ERROR msg => (print ("Error: " ^ msg); error msg)
in
(false, state)
- |> (if blocking then launch_atps #> not auto ? launch_smts
- else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
+ |> (if blocking then
+ launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
+ else
+ (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
handle TimeLimit.TimeOut =>
(print "Sledgehammer ran out of time."; (false, state))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun May 22 14:51:42 2011 +0200
@@ -25,7 +25,7 @@
val is_type_surely_infinite : Proof.context -> typ list -> typ -> bool
val monomorphic_term : Type.tyenv -> term -> term
val eta_expand : typ list -> term -> int -> term
- val transform_elim_term : term -> term
+ val transform_elim_prop : term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
@@ -210,7 +210,7 @@
predicate variable. Leaves other theorems unchanged. We simply instantiate
the conclusion variable to False. (Cf. "transform_elim_theorem" in
"Meson_Clausify".) *)
-fun transform_elim_term t =
+fun transform_elim_prop t =
case Logic.strip_imp_concl t of
@{const Trueprop} $ Var (z, @{typ bool}) =>
subst_Vars [(z, @{const False})] t
--- a/src/HOL/ex/sledgehammer_tactics.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Sun May 22 14:51:42 2011 +0200
@@ -34,8 +34,9 @@
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val facts =
Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_built_in_const
- relevance_fudge relevance_override chained_ths hyp_ts concl_t
+ (the_default default_max_relevant max_relevant) (K true)
+ is_built_in_const relevance_fudge relevance_override chained_ths
+ hyp_ts concl_t
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
facts = map Sledgehammer_Provers.Untranslated_Fact facts,
--- a/src/HOL/ex/tptp_export.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Sun May 22 14:51:42 2011 +0200
@@ -23,7 +23,7 @@
fun facts_of thy =
Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
- true [] []
+ true (K true) [] []
fun fold_body_thms f =
let