--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Nov 05 14:10:41 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Nov 05 14:36:17 2010 +0100
@@ -349,17 +349,17 @@
#> Config.put Sledgehammer.measure_run_time true)
val params as {full_types, relevance_thresholds, max_relevant, ...} =
Sledgehammer_Isar.default_params ctxt
- [("timeout", Int.toString timeout ^ " s")]
+ [("timeout", Int.toString timeout)]
val default_max_relevant =
Sledgehammer.default_max_relevant_for_prover thy prover_name
- val irrelevant_consts =
- Sledgehammer.irrelevant_consts_for_prover prover_name
+ val is_built_in_const =
+ Sledgehammer.is_built_in_const_for_prover ctxt prover_name
val relevance_fudge = Sledgehammer.relevance_fudge_for_prover prover_name
val relevance_override = {add = [], del = [], only = false}
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
val facts =
Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
- (the_default default_max_relevant max_relevant) irrelevant_consts
+ (the_default default_max_relevant max_relevant) is_built_in_const
relevance_fudge relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
@@ -369,10 +369,11 @@
(case hard_timeout of
NONE => I
| SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
- val ({outcome, message, used_facts, run_time_in_msecs = SOME time_prover, ...}
+ val ({outcome, message, used_facts, run_time_in_msecs, ...}
: Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
(prover params (K ""))) problem
+ val time_prover = run_time_in_msecs |> the_default ~1
in
case outcome of
NONE => (message, SH_OK (time_isa, time_prover, used_facts))
@@ -446,7 +447,7 @@
|> Option.map (fst o read_int o explode)
|> the_default 5
val params = Sledgehammer_Isar.default_params ctxt
- [("provers", prover_name), ("timeout", Int.toString timeout ^ " s")]
+ [("provers", prover_name), ("timeout", Int.toString timeout)]
val minimize =
Sledgehammer_Minimize.minimize_facts params 1
(Sledgehammer_Util.subgoal_count st)
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Nov 05 14:10:41 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Nov 05 14:36:17 2010 +0100
@@ -111,8 +111,8 @@
|> the_default default_prover
val default_max_relevant =
Sledgehammer.default_max_relevant_for_prover thy prover
- val irrelevant_consts =
- Sledgehammer.irrelevant_consts_for_prover prover
+ val is_built_in_const =
+ Sledgehammer.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
extract_relevance_fudge args
(Sledgehammer.relevance_fudge_for_prover prover)
@@ -124,9 +124,8 @@
val facts =
Sledgehammer_Filter.relevant_facts ctxt full_types
relevance_thresholds
- (the_default default_max_relevant max_relevant)
- irrelevant_consts relevance_fudge relevance_override facts hyp_ts
- concl_t
+ (the_default default_max_relevant max_relevant) is_built_in_const
+ relevance_fudge relevance_override facts hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
List.concat proofs |> sort_distinct string_ord
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 05 14:10:41 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Nov 05 14:36:17 2010 +0100
@@ -54,7 +54,8 @@
val is_prover_available : theory -> string -> bool
val is_prover_installed : Proof.context -> string -> bool
val default_max_relevant_for_prover : theory -> string -> int
- val irrelevant_consts_for_prover : string -> string list
+ val is_built_in_const_for_prover :
+ Proof.context -> string -> string * typ -> bool
val relevance_fudge_for_prover : string -> relevance_fudge
val dest_dir : string Config.T
val problem_prefix : string Config.T
@@ -116,29 +117,9 @@
[@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
@{const_name HOL.eq}]
-(* FIXME: check types *)
-val smt_irrelevant_consts =
- atp_irrelevant_consts @
- [@{const_name distinct},
- (* numeral-related: *)
- @{const_name number_of}, @{const_name Int.Pls}, @{const_name Int.Min},
- @{const_name Int.Bit0}, @{const_name Int.Bit1}, @{const_name Suc},
- (* FIXME: @{const_name Numeral0}, @{const_name Numeral1}, *)
- (* int => nat *)
- @{const_name nat},
- (* nat => int *)
- (* FIXME: @{const_name int}, *)
- (* for "nat", "int", and "real": *)
- @{const_name plus}, @{const_name uminus}, @{const_name minus},
- @{const_name times}, @{const_name less}, @{const_name less_eq},
- @{const_name abs}, @{const_name min}, @{const_name max},
- (* for "nat" and "div": *)
- @{const_name div}, @{const_name mod} (* , *)
- (* for real: *)
- (* FIXME: @{const_name "op /"} *)]
-
-fun irrelevant_consts_for_prover name =
- if is_smt_prover name then smt_irrelevant_consts else atp_irrelevant_consts
+fun is_built_in_const_for_prover ctxt name (s, T) =
+ if is_smt_prover name then SMT_Builtin.is_builtin ctxt (s, T)
+ else member (op =) atp_irrelevant_consts s
(* FUDGE *)
val atp_relevance_fudge =
@@ -536,8 +517,8 @@
val _ = () |> not blocking ? kill_provers
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition is_smt_prover
- fun run_provers label full_types irrelevant_consts relevance_fudge
- maybe_translate provers (res as (success, state)) =
+ fun run_provers label full_types relevance_fudge maybe_translate provers
+ (res as (success, state)) =
if success orelse null provers then
res
else
@@ -549,9 +530,11 @@
0 |> fold (Integer.max o default_max_relevant_for_prover thy)
provers
|> auto ? (fn n => n div auto_max_relevant_divisor)
+ val is_built_in_const =
+ is_built_in_const_for_prover ctxt (hd provers)
val facts =
relevant_facts ctxt full_types relevance_thresholds
- max_max_relevant irrelevant_consts relevance_fudge
+ max_max_relevant is_built_in_const relevance_fudge
relevance_override chained_ths hyp_ts concl_t
|> map maybe_translate
val problem =
@@ -560,7 +543,7 @@
val run_prover = run_prover params auto minimize_command
in
if debug then
- Output.urgent_message (label ^ ": " ^
+ Output.urgent_message (label ^ plural_s (length provers) ^ ": " ^
(if null facts then
"Found no relevant facts."
else
@@ -580,11 +563,10 @@
|> exists fst |> rpair state
end
val run_atps =
- run_provers "ATPs" full_types atp_irrelevant_consts atp_relevance_fudge
+ run_provers "ATP" full_types atp_relevance_fudge
(Translated o translate_fact ctxt) atps
val run_smts =
- run_provers "SMT" true smt_irrelevant_consts smt_relevance_fudge
- Untranslated smts
+ run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
fun run_atps_and_smt_solvers () =
[run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Nov 05 14:10:41 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Nov 05 14:36:17 2010 +0100
@@ -38,7 +38,7 @@
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
val relevant_facts :
- Proof.context -> bool -> real * real -> int -> string list
+ Proof.context -> bool -> real * real -> int -> (string * typ -> bool)
-> relevance_fudge -> relevance_override -> thm list -> term list -> term
-> ((string * locality) * thm) list
end;
@@ -87,29 +87,37 @@
val theory_const_suffix = Long_Name.separator ^ " 1"
fun needs_quoting reserved s =
- Symtab.defined reserved s (* FIXME: orelse
- exists (not o Syntax.is_identifier) (Long_Name.explode s) *)
+ Symtab.defined reserved s orelse
+ exists (not o Syntax.is_identifier) (Long_Name.explode s)
-fun repair_name reserved multi j name =
+fun make_name reserved multi j name =
(name |> needs_quoting reserved name ? quote) ^
(if multi then "(" ^ Int.toString j ^ ")" else "")
+fun explode_interval _ (Facts.FromTo (i, j)) = i upto j
+ | explode_interval max (Facts.From i) = i upto i + max - 1
+ | explode_interval _ (Facts.Single i) = [i]
+
fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
implode (map (fn arg => "[" ^ Pretty.str_of (Args.pretty_src ctxt arg)
^ "]") args)
- val name =
+ fun nth_name j =
case xref of
Facts.Fact s => "`" ^ s ^ "`" ^ bracket
| Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
- | _ => Facts.string_of_ref xref ^ bracket
- val multi = length ths > 1
+ | Facts.Named ((name, _), NONE) =>
+ make_name reserved (length ths > 1) (j + 1) name ^ bracket
+ | Facts.Named ((name, _), SOME intervals) =>
+ make_name reserved true
+ (nth (maps (explode_interval (length ths)) intervals) j) name ^
+ bracket
in
- (ths, (1, []))
+ (ths, (0, []))
|-> fold (fn th => fn (j, rest) =>
- (j + 1, ((repair_name reserved multi j name,
+ (j + 1, ((nth_name j,
if member Thm.eq_thm chained_ths th then Chained
else General), th) :: rest))
|> snd
@@ -174,31 +182,31 @@
and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts)
and rich_ptype thy const (s, T) ts =
PType (order_of_type T, ptype thy const (s, T) ts)
-and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts)
+and rich_pconst thy const x ts = (x, rich_ptype thy const x ts)
fun string_for_hyper_pconst (s, ps) =
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
(* Add a pconstant to the table, but a [] entry means a standard
connective, which we ignore.*)
-fun add_pconst_to_table irrelevant_consts also_skolem (c, p) =
- if member (op =) irrelevant_consts c orelse
- (not also_skolem andalso String.isPrefix skolem_prefix c) then
+fun add_pconst_to_table is_built_in_const also_skolem ((s, T), p) =
+ if is_built_in_const (s, T) orelse
+ (not also_skolem andalso String.isPrefix skolem_prefix s) then
I
else
- Symtab.map_default (c, [p]) (insert (op =) p)
+ Symtab.map_default (s, [p]) (insert (op =) p)
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
-fun pconsts_in_terms thy irrelevant_consts also_skolems pos ts =
+fun pconsts_in_terms thy is_built_in_const also_skolems pos ts =
let
val flip = Option.map not
(* We include free variables, as well as constants, to handle locales. For
each quantifiers that must necessarily be skolemized by the ATP, we
introduce a fresh constant to simulate the effect of Skolemization. *)
- fun do_const const (s, T) ts =
- add_pconst_to_table irrelevant_consts also_skolems
- (rich_pconst thy const (s, T) ts)
+ fun do_const const x ts =
+ add_pconst_to_table is_built_in_const also_skolems
+ (rich_pconst thy const x ts)
#> fold do_term ts
and do_term t =
case strip_comb t of
@@ -206,15 +214,15 @@
| (Free x, ts) => do_const false x ts
| (Abs (_, T, t'), ts) =>
(null ts
- ? add_pconst_to_table irrelevant_consts true
- (abs_name, PType (order_of_type T + 1, [])))
+ ? add_pconst_to_table (K false) true
+ ((abs_name, dummyT), PType (order_of_type T + 1, [])))
#> fold do_term (t' :: ts)
| (_, ts) => fold do_term ts
fun do_quantifier will_surely_be_skolemized abs_T body_t =
do_formula pos body_t
#> (if also_skolems andalso will_surely_be_skolemized then
- add_pconst_to_table irrelevant_consts true
- (gensym skolem_prefix, PType (order_of_type abs_T, []))
+ add_pconst_to_table (K false) true
+ ((gensym skolem_prefix, dummyT), PType (order_of_type abs_T, []))
else
I)
and do_term_or_formula T =
@@ -366,22 +374,26 @@
||> filter_out (pconst_hyper_mem swap relevant_consts) of
([], _) => 0.0
| (rel, irrel) =>
- let
- val irrel = irrel |> filter_out (pconst_mem swap rel)
- val rel_weight =
- 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
- val irrel_weight =
- ~ (locality_bonus fudge loc)
- |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
- val res = rel_weight / (rel_weight + irrel_weight)
- in if Real.isFinite res then res else 0.0 end
+ if forall (forall (String.isSuffix theory_const_suffix o fst))
+ [rel, irrel] then
+ 0.0
+ else
+ let
+ val irrel = irrel |> filter_out (pconst_mem swap rel)
+ val rel_weight =
+ 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
+ val irrel_weight =
+ ~ (locality_bonus fudge loc)
+ |> fold (curry (op +) o irrel_pconst_weight fudge const_tab) irrel
+ val res = rel_weight / (rel_weight + irrel_weight)
+ in if Real.isFinite res then res else 0.0 end
-fun pconsts_in_fact thy irrelevant_consts t =
+fun pconsts_in_fact thy is_built_in_const t =
Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
- (pconsts_in_terms thy irrelevant_consts true (SOME true) [t]) []
-fun pair_consts_fact thy irrelevant_consts fudge fact =
+ (pconsts_in_terms thy is_built_in_const true (SOME true) [t]) []
+fun pair_consts_fact thy is_built_in_const fudge fact =
case fact |> snd |> theory_const_prop_of fudge
- |> pconsts_in_fact thy irrelevant_consts of
+ |> pconsts_in_fact thy is_built_in_const of
[] => NONE
| consts => SOME ((fact, consts), NONE)
@@ -411,23 +423,23 @@
(accepts, more_rejects @ rejects)
end
-fun if_empty_replace_with_locality thy irrelevant_consts facts loc tab =
+fun if_empty_replace_with_locality thy is_built_in_const facts loc tab =
if Symtab.is_empty tab then
- pconsts_in_terms thy irrelevant_consts false (SOME false)
+ pconsts_in_terms thy is_built_in_const false (SOME false)
(map_filter (fn ((_, loc'), th) =>
if loc' = loc then SOME (prop_of th) else NONE) facts)
else
tab
-fun relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts
+fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
(fudge as {threshold_divisor, ridiculous_threshold, ...})
({add, del, ...} : relevance_override) facts goal_ts =
let
val thy = ProofContext.theory_of ctxt
val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
val goal_const_tab =
- pconsts_in_terms thy irrelevant_consts false (SOME false) goal_ts
- |> fold (if_empty_replace_with_locality thy irrelevant_consts facts)
+ pconsts_in_terms thy is_built_in_const false (SOME false) goal_ts
+ |> fold (if_empty_replace_with_locality thy is_built_in_const facts)
[Chained, Assum, Local]
val add_ths = Attrib.eval_thms ctxt add
val del_ths = Attrib.eval_thms ctxt del
@@ -448,8 +460,8 @@
take_most_relevant max_relevant remaining_max fudge candidates
val rel_const_tab' =
rel_const_tab
- |> fold (add_pconst_to_table irrelevant_consts false)
- (maps (snd o fst) accepts)
+ |> fold (add_pconst_to_table (K false) false)
+ (maps (map (apfst (rpair dummyT)) o snd o fst) accepts)
fun is_dirty (c, _) =
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
val (hopeful_rejects, hopeless_rejects) =
@@ -509,7 +521,7 @@
o snd))
@ accepts
in
- facts |> map_filter (pair_consts_fact thy irrelevant_consts fudge)
+ facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
|> iter 0 max_relevant threshold0 goal_const_tab []
|> not (null add_ths) ? add_add_ths
|> tap (fn res => trace_msg (fn () =>
@@ -755,7 +767,7 @@
val name2 = Name_Space.extern full_space name0
in
case find_first check_thms [name1, name2, name0] of
- SOME name => repair_name reserved multi j name
+ SOME name => make_name reserved multi j name
| NONE => ""
end),
let val t = prop_of th in
@@ -788,7 +800,7 @@
(***************************************************************)
fun relevant_facts ctxt full_types (threshold0, threshold1) max_relevant
- irrelevant_consts fudge (override as {add, only, ...})
+ is_built_in_const fudge (override as {add, only, ...})
chained_ths hyp_ts concl_t =
let
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -812,7 +824,7 @@
max_relevant = 0 then
[]
else
- relevance_filter ctxt threshold0 decay max_relevant irrelevant_consts
+ relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
fudge override facts (concl_t :: hyp_ts))
|> map (apfst (apfst (fn f => f ())))
end