--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 17:43:42 2011 +0200
@@ -251,9 +251,8 @@
(* Generalized first-order terms, which include file names, numbers, etc. *)
fun parse_annotation x =
- ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
- >> filter (is_some o Int.fromString))
- -- Scan.optional parse_annotation [] >> op @
+ ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id))
+ -- Scan.optional parse_annotation [] >> op @
|| $$ "(" |-- parse_annotations --| $$ ")"
|| $$ "[" |-- parse_annotations --| $$ "]") x
and parse_annotations x =
@@ -353,8 +352,8 @@
val parse_vampire_braced_stuff =
$$ "{" -- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) -- $$ "}"
-val parse_vampire_parenthesized_detritus =
- $$ "(" |-- parse_vampire_detritus --| $$ ")"
+fun parse_vampire_parenthesized_detritus x =
+ ($$ "(" |-- parse_vampire_detritus --| $$ ")") x
(* Syntax: <num>. <formula> <annotation> *)
fun parse_vampire_line x =
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon May 02 17:43:42 2011 +0200
@@ -11,15 +11,6 @@
type formula_kind = ATP_Problem.formula_kind
type failure = ATP_Proof.failure
- datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
- datatype type_level =
- All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-
- datatype type_system =
- Many_Typed |
- Preds of polymorphism * type_level |
- Tags of polymorphism * type_level
-
type atp_config =
{exec : string * string,
required_execs : (string * string) list,
@@ -29,15 +20,11 @@
hypothesis_kind : formula_kind,
formats : format list,
best_slices : unit -> (real * (bool * int)) list,
- best_type_systems : type_system list}
+ best_type_systems : string list}
datatype e_weight_method =
E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
- val polymorphism_of_type_sys : type_system -> polymorphism
- val level_of_type_sys : type_system -> type_level
- val is_type_sys_virtually_sound : type_system -> bool
- val is_type_sys_fairly_sound : type_system -> bool
(* for experimentation purposes -- do not use in production code *)
val e_weight_method : e_weight_method Unsynchronized.ref
val e_default_fun_weight : real Unsynchronized.ref
@@ -58,7 +45,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> format list -> (unit -> int)
- -> type_system list -> string * atp_config
+ -> string list -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -75,32 +62,6 @@
(* ATP configuration *)
-datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
-datatype type_level =
- All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
-
-datatype type_system =
- Many_Typed |
- Preds of polymorphism * type_level |
- Tags of polymorphism * type_level
-
-fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
- | polymorphism_of_type_sys (Preds (poly, _)) = poly
- | polymorphism_of_type_sys (Tags (poly, _)) = poly
-
-fun level_of_type_sys Many_Typed = All_Types
- | level_of_type_sys (Preds (_, level)) = level
- | level_of_type_sys (Tags (_, level)) = level
-
-val is_type_level_virtually_sound =
- member (op =) [All_Types, Nonmonotonic_Types]
-val is_type_sys_virtually_sound =
- is_type_level_virtually_sound o level_of_type_sys
-
-fun is_type_level_fairly_sound level =
- 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
-
type atp_config =
{exec : string * string,
required_execs : (string * string) list,
@@ -110,7 +71,7 @@
hypothesis_kind : formula_kind,
formats : format list,
best_slices : unit -> (real * (bool * int)) list,
- best_type_systems : type_system list}
+ best_type_systems : string list}
val known_perl_failures =
[(CantConnect, "HTTP error"),
@@ -237,7 +198,7 @@
(0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
else
[(1.0, (true, 250 (* FUDGE *)))],
- best_type_systems = []}
+ best_type_systems = ["const_args", "mangled_preds"]}
val e = (eN, e_config)
@@ -268,7 +229,7 @@
best_slices =
K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
(0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
- best_type_systems = []}
+ best_type_systems = ["mangled_preds"]}
val spass = (spassN, spass_config)
@@ -304,7 +265,7 @@
best_slices =
K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
(0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
- best_type_systems = []}
+ best_type_systems = ["mangled_preds"]}
val vampire = (vampireN, vampire_config)
@@ -408,7 +369,7 @@
Conjecture [Tff] (K 200 (* FUDGE *)) []
val remote_sine_e =
remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
- []
+ (#best_type_systems e_config)
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r024"]
[("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 02 17:43:42 2011 +0200
@@ -46,7 +46,6 @@
open ATP_Problem
open ATP_Proof
-open ATP_Systems
open Metis_Translate
open Sledgehammer_Util
open Sledgehammer_Filter
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 02 17:43:42 2011 +0200
@@ -10,7 +10,16 @@
sig
type 'a fo_term = 'a ATP_Problem.fo_term
type 'a problem = 'a ATP_Problem.problem
- type type_system = ATP_Systems.type_system
+
+ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+ datatype type_level =
+ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+
+ datatype type_system =
+ Many_Typed |
+ Preds of polymorphism * type_level |
+ Tags of polymorphism * type_level
+
type translated_formula
val readable_names : bool Unsynchronized.ref
@@ -20,6 +29,11 @@
val explicit_app_base : string
val type_pred_base : string
val tff_type_prefix : string
+ val type_sys_from_string : string -> type_system
+ val polymorphism_of_type_sys : type_system -> polymorphism
+ val level_of_type_sys : type_system -> type_level
+ val is_type_sys_virtually_sound : type_system -> bool
+ val is_type_sys_fairly_sound : type_system -> bool
val num_atp_type_args : theory -> type_system -> string -> int
val unmangled_const : string -> string * string fo_term list
val translate_atp_fact :
@@ -37,7 +51,6 @@
struct
open ATP_Problem
-open ATP_Systems
open Metis_Translate
open Sledgehammer_Util
@@ -72,6 +85,58 @@
(* Freshness almost guaranteed! *)
val sledgehammer_weak_prefix = "Sledgehammer:"
+datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
+datatype type_level =
+ All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types
+
+datatype type_system =
+ Many_Typed |
+ Preds of polymorphism * type_level |
+ Tags of polymorphism * type_level
+
+fun type_sys_from_string s =
+ (case try (unprefix "mangled_") s of
+ SOME s => (Mangled_Monomorphic, s)
+ | NONE =>
+ case try (unprefix "mono_") s of
+ SOME s => (Monomorphic, s)
+ | NONE => (Polymorphic, s))
+ ||> (fn s =>
+ case try (unsuffix " ?") s of
+ SOME s => (Nonmonotonic_Types, s)
+ | NONE =>
+ case try (unsuffix " !") s of
+ SOME s => (Finite_Types, s)
+ | NONE => (All_Types, s))
+ |> (fn (polymorphism, (level, core)) =>
+ case (core, (polymorphism, level)) of
+ ("many_typed", (Polymorphic (* naja *), All_Types)) =>
+ Many_Typed
+ | ("preds", extra) => Preds extra
+ | ("tags", extra) => Tags extra
+ | ("const_args", (_, All_Types (* naja *))) =>
+ Preds (polymorphism, Const_Arg_Types)
+ | ("erased", (Polymorphic, All_Types (* naja *))) =>
+ Preds (polymorphism, No_Types)
+ | _ => error ("Unknown type system: " ^ quote s ^ "."))
+
+fun polymorphism_of_type_sys Many_Typed = Mangled_Monomorphic
+ | polymorphism_of_type_sys (Preds (poly, _)) = poly
+ | polymorphism_of_type_sys (Tags (poly, _)) = poly
+
+fun level_of_type_sys Many_Typed = All_Types
+ | level_of_type_sys (Preds (_, level)) = level
+ | level_of_type_sys (Tags (_, level)) = level
+
+val is_type_level_virtually_sound =
+ member (op =) [All_Types, Nonmonotonic_Types]
+val is_type_sys_virtually_sound =
+ is_type_level_virtually_sound o level_of_type_sys
+
+fun is_type_level_fairly_sound level =
+ 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)
@@ -504,7 +569,7 @@
fun var s = ATerm (`I s, [])
fun tag tm = ATerm (`make_fixed_const type_tag_name, [var "X", tm])
in
- Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
+ Formula (helper_prefix ^ "ti_ti", Axiom,
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
|> close_formula_universally, NONE, NONE)
end
@@ -774,8 +839,7 @@
fun decl_line_for_sym_decl s (s', _, T, pred_sym, ary) =
let val (arg_Ts, res_T) = n_ary_strip_type ary T in
- Decl (sym_decl_prefix ^ ascii_of s, (s, s'),
- map mangled_type_name arg_Ts,
+ Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
end
@@ -792,7 +856,8 @@
arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
else NONE)
in
- Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
+ Formula (sym_decl_prefix ^ s ^
+ (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
CombConst ((s, s'), T, T_args)
|> fold (curry (CombApp o swap)) bound_tms
|> type_pred_combatom type_sys res_T
@@ -915,6 +980,7 @@
val hyp_weight = 0.1
val fact_min_weight = 0.2
val fact_max_weight = 1.0
+val type_info_default_weight = 0.8
fun add_term_weights weight (ATerm (s, tms)) =
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
@@ -943,10 +1009,14 @@
(* Weights are from 0.0 (most important) to 1.0 (least important). *)
fun atp_problem_weights problem =
- Symtab.empty
- |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN))
- |> add_facts_weights (these (AList.lookup (op =) problem factsN))
- |> Symtab.dest
- |> sort (prod_ord Real.compare string_ord o pairself swap)
+ let val get = these o AList.lookup (op =) problem in
+ Symtab.empty
+ |> add_conjectures_weights (get free_typesN @ get conjsN)
+ |> add_facts_weights (get factsN)
+ |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
+ [sym_declsN, class_relsN, aritiesN]
+ |> Symtab.dest
+ |> sort (prod_ord Real.compare string_ord o pairself swap)
+ end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 02 17:43:42 2011 +0200
@@ -233,33 +233,10 @@
val blocking = auto orelse debug orelse lookup_bool "blocking"
val provers = lookup_string "provers" |> space_explode " "
|> auto ? single o hd
- val type_sys = lookup_string "type_sys"
val type_sys =
- (case try (unprefix "mangled_") type_sys of
- SOME s => (Mangled_Monomorphic, s)
- | NONE =>
- case try (unprefix "mono_") type_sys of
- SOME s => (Monomorphic, s)
- | NONE => (Polymorphic, type_sys))
- ||> (fn s => case try (unsuffix " ?") s of
- SOME s => (Nonmonotonic_Types, s)
- | NONE =>
- case try (unsuffix " !") s of
- SOME s => (Finite_Types, s)
- | NONE => (All_Types, s))
- |> (fn (polymorphism, (level, core)) =>
- case (core, (polymorphism, level)) of
- ("many_typed", (Polymorphic (* naja *), All_Types)) =>
- Dumb_Type_Sys Many_Typed
- | ("preds", extra) => Dumb_Type_Sys (Preds extra)
- | ("tags", extra) => Dumb_Type_Sys (Tags extra)
- | ("const_args", (_, All_Types (* naja *))) =>
- Dumb_Type_Sys (Preds (polymorphism, Const_Arg_Types))
- | ("erased", (Polymorphic, All_Types (* naja *))) =>
- Dumb_Type_Sys (Preds (polymorphism, No_Types))
- | ("smart", (Polymorphic, All_Types) (* naja *)) =>
- Smart_Type_Sys (lookup_bool "full_types")
- | _ => error ("Unknown type system: " ^ quote type_sys ^ "."))
+ case lookup_string "type_sys" of
+ "smart" => Smart_Type_Sys (lookup_bool "full_types")
+ | s => Dumb_Type_Sys (type_sys_from_string s)
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_int_option "max_relevant"
val monomorphize_limit = lookup_int "monomorphize_limit"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 17:43:42 2011 +0200
@@ -336,7 +336,7 @@
val atp_blacklist_max_iters = 10
(* Important messages are important but not so important that users want to see
them each time. *)
-val atp_important_message_keep_factor = 0.1
+val atp_important_message_keep_quotient = 10
val fallback_best_type_systems =
[Preds (Polymorphic, Const_Arg_Types), Many_Typed]
@@ -351,7 +351,7 @@
adjust_dumb_type_sys formats type_sys
| determine_format_and_type_sys best_type_systems formats
(Smart_Type_Sys full_types) =
- best_type_systems @ fallback_best_type_systems
+ map type_sys_from_string best_type_systems @ fallback_best_type_systems
|> find_first (if full_types then is_type_sys_virtually_sound else K true)
|> the |> adjust_dumb_type_sys formats
@@ -449,8 +449,9 @@
I))
* 0.001) |> seconds
val _ =
- if verbose then
- "ATP slice " ^ string_of_int (slice + 1) ^ " with " ^
+ if debug then
+ quote name ^ " slice " ^ string_of_int (slice + 1) ^
+ " of " ^ string_of_int num_actual_slices ^ " with " ^
string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
" for " ^ string_from_time slice_timeout ^ "..."
|> Output.urgent_message
@@ -566,7 +567,8 @@
(output, msecs, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
- if not auto andalso random () <= atp_important_message_keep_factor then
+ if not auto andalso
+ random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
extract_important_message output
else
""
@@ -671,10 +673,10 @@
timeout
val num_facts = length facts
val _ =
- if verbose then
- "SMT slice with " ^ string_of_int num_facts ^ " fact" ^
- plural_s num_facts ^ " for " ^ string_from_time slice_timeout ^
- "..."
+ if debug then
+ quote name ^ " slice " ^ string_of_int slice ^ " with " ^
+ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
+ string_from_time slice_timeout ^ "..."
|> Output.urgent_message
else
()
@@ -693,14 +695,6 @@
(ML_Compiler.exn_message exn
|> SMT_Failure.Other_Failure |> SOME, [])
val death = Timer.checkRealTimer timer
- val _ =
- if verbose andalso is_some outcome then
- "SMT outcome: " ^ SMT_Failure.string_of_failure ctxt (the outcome)
- |> Output.urgent_message
- else if debug then
- Output.urgent_message "SMT solver returned."
- else
- ()
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
val time_so_far = Time.+ (time_so_far, Time.- (death, birth))
val too_many_facts_perhaps =
@@ -708,15 +702,7 @@
NONE => false
| SOME (SMT_Failure.Counterexample _) => false
| SOME SMT_Failure.Time_Out => slice_timeout <> timeout
- | SOME (SMT_Failure.Abnormal_Termination code) =>
- (if verbose then
- "The SMT solver invoked with " ^ string_of_int num_facts ^
- " fact" ^ plural_s num_facts ^ " terminated abnormally with \
- \exit code " ^ string_of_int code ^ "."
- |> warning
- else
- ();
- true (* kind of *))
+ | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
| SOME SMT_Failure.Out_Of_Memory => true
| SOME (SMT_Failure.Other_Failure _) => true
val timeout = Time.- (timeout, Timer.checkRealTimer timer)
@@ -724,9 +710,21 @@
if too_many_facts_perhaps andalso slice < max_slices andalso
num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
let
- val n = Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts)
+ val new_num_facts =
+ Real.ceil (!smt_slice_fact_frac * Real.fromInt num_facts)
+ val _ =
+ if verbose andalso is_some outcome then
+ quote name ^ " invoked with " ^ string_of_int num_facts ^
+ " fact" ^ plural_s num_facts ^ ": " ^
+ string_for_failure (failure_from_smt_failure (the outcome)) ^
+ " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
+ plural_s new_num_facts
+ |> Output.urgent_message
+ else
+ ()
in
- do_slice timeout (slice + 1) outcome0 time_so_far (take n facts)
+ facts |> take new_num_facts
+ |> do_slice timeout (slice + 1) outcome0 time_so_far
end
else
{outcome = if is_none outcome then NONE else the outcome0,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 17:43:42 2011 +0200
@@ -23,7 +23,6 @@
structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
struct
-open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_ATP_Translate
--- a/src/HOL/ex/tptp_export.ML Mon May 02 17:43:06 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Mon May 02 17:43:42 2011 +0200
@@ -98,9 +98,10 @@
Sledgehammer_ATP_Translate.translate_atp_fact ctxt true
((Thm.get_name_hint th, loc), th)))
val type_sys =
- ATP_Systems.Preds (ATP_Systems.Polymorphic,
- if full_types then ATP_Systems.All_Types
- else ATP_Systems.Const_Arg_Types)
+ Sledgehammer_ATP_Translate.Preds
+ (Sledgehammer_ATP_Translate.Polymorphic,
+ if full_types then Sledgehammer_ATP_Translate.All_Types
+ else Sledgehammer_ATP_Translate.Const_Arg_Types)
val explicit_apply = false
val (atp_problem, _, _, _, _) =
Sledgehammer_ATP_Translate.prepare_atp_problem ctxt type_sys