--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Nov 04 13:37:11 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Nov 04 14:59:44 2010 +0100
@@ -352,14 +352,14 @@
[("timeout", Int.toString timeout ^ " s")]
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,
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Nov 04 13:37:11 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Nov 04 14:59:44 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 Thu Nov 04 13:37:11 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 04 14:59:44 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 =
@@ -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 "ATPs" 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" 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 Thu Nov 04 13:37:11 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Nov 04 14:59:44 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;
@@ -181,8 +181,8 @@
(* 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
+fun add_pconst_to_table is_built_in_const also_skolem (c, p) =
+ if is_built_in_const (c, dummyT)(*###*) orelse
(not also_skolem andalso String.isPrefix skolem_prefix c) then
I
else
@@ -190,14 +190,14 @@
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
+ add_pconst_to_table is_built_in_const also_skolems
(rich_pconst thy const (s, T) ts)
#> fold do_term ts
and do_term t =
@@ -206,14 +206,14 @@
| (Free x, ts) => do_const false x ts
| (Abs (_, T, t'), ts) =>
(null ts
- ? add_pconst_to_table irrelevant_consts true
+ ? add_pconst_to_table is_built_in_const true
(abs_name, 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
+ add_pconst_to_table is_built_in_const true
(gensym skolem_prefix, PType (order_of_type abs_T, []))
else
I)
@@ -376,12 +376,12 @@
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 +411,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,7 +448,7 @@
take_most_relevant max_relevant remaining_max fudge candidates
val rel_const_tab' =
rel_const_tab
- |> fold (add_pconst_to_table irrelevant_consts false)
+ |> fold (add_pconst_to_table is_built_in_const false)
(maps (snd o fst) accepts)
fun is_dirty (c, _) =
Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
@@ -509,7 +509,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 () =>
@@ -788,7 +788,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 +812,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