--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 27 13:52:47 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 27 13:52:47 2011 +0200
@@ -23,7 +23,7 @@
prem_kind : formula_kind,
formats : format list,
best_slices :
- Proof.context -> (real * (bool * (int * string list * string))) list}
+ Proof.context -> (real * (bool * (int * string * string))) list}
val e_smartN : string
val e_autoN : string
@@ -52,7 +52,7 @@
val remote_atp :
string -> string -> string list -> (string * string) list
-> (failure * string) list -> formula_kind -> formula_kind -> format list
- -> (Proof.context -> int * string list) -> string * atp_config
+ -> (Proof.context -> int * string) -> string * atp_config
val add_atp : string * atp_config -> theory -> theory
val get_atp : theory -> string -> atp_config
val supported_atps : theory -> string list
@@ -81,19 +81,19 @@
prem_kind : formula_kind,
formats : format list,
best_slices :
- Proof.context -> (real * (bool * (int * string list * string))) list}
+ Proof.context -> (real * (bool * (int * string * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
the ATPs are run in parallel. The "real" components give the faction of the
- time available given to the slice; these should add up to 1.0. The "bool"
+ time available given to the slice and should add up to 1.0. The "bool"
component indicates whether the slice's strategy is complete; the "int", the
- preferred number of facts to pass; the "string list", the preferred type
- systems, which should be of the form [sound] or [unsound, sound], where
- "sound" is a sound type system and "unsound" is an unsound one.
+ preferred number of facts to pass; the first "string", the preferred type
+ system; the second "string", extra information to the prover (e.g., SOS or no
+ SOS).
The last slice should be the most "normal" one, because it will get all the
- time available if the other slices fail early and also because it is used for
- remote provers and if slicing is disabled. *)
+ time available if the other slices fail early and also because it is used if
+ slicing is disabled (e.g., by the minimizer). *)
val known_perl_failures =
[(CantConnect, "HTTP error"),
@@ -217,11 +217,11 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, ["mangled_tags?"], e_fun_weightN))),
- (0.334, (true, (50, ["mangled_preds?"], e_fun_weightN))),
- (0.333, (true, (1000, ["mangled_tags?"], e_sym_offset_weightN)))]
+ [(0.333, (true, (500, "mangled_tags?", e_fun_weightN))),
+ (0.334, (true, (50, "mangled_preds?", e_fun_weightN))),
+ (0.333, (true, (1000, "mangled_tags?", e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, ["mangled_tags?"], method)))]
+ [(1.0, (true, (500, "mangled_tags?", method)))]
end}
val e = (eN, e_config)
@@ -237,7 +237,7 @@
val spass_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
- arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs timeout))
|> sos = sosN ? prefix "-SOS=1 ",
@@ -256,9 +256,9 @@
formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, ["mangled_tags"], sosN))),
- (0.333, (false, (300, ["poly_tags?"], sosN))),
- (0.334, (true, (50, ["mangled_tags?"], no_sosN)))]
+ [(0.333, (false, (150, "mangled_tags", sosN))),
+ (0.333, (false, (300, "poly_tags?", sosN))),
+ (0.334, (true, (50, "mangled_tags?", no_sosN)))]
|> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -273,7 +273,7 @@
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
- arguments = fn ctxt => fn _ => fn sos => fn timeout => fn _ =>
+ arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
"--proof tptp --mode casc -t " ^ string_of_int (to_secs timeout) ^
" --thanks \"Andrei and Krystof\" --input_file"
|> sos = sosN ? prefix "--sos on ",
@@ -297,9 +297,9 @@
formats = [FOF],
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, ["poly_preds"], sosN))),
- (0.334, (true, (50, ["mangled_preds?"], no_sosN))),
- (0.333, (false, (500, ["mangled_tags?"], sosN)))]
+ [(0.333, (false, (150, "poly_preds", sosN))),
+ (0.334, (true, (50, "mangled_preds?", no_sosN))),
+ (0.333, (false, (500, "mangled_tags?", sosN)))]
|> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -325,7 +325,7 @@
formats = [FOF],
best_slices =
(* FUDGE (FIXME) *)
- K [(1.0, (false, (250, [], "")))]}
+ K [(1.0, (false, (250, "mangled_preds?", "")))]}
val z3_atp = (z3_atpN, z3_atp_config)
@@ -385,8 +385,8 @@
prem_kind = prem_kind,
formats = formats,
best_slices = fn ctxt =>
- let val (max_relevant, type_syss) = best_slice ctxt in
- [(1.0, (false, (max_relevant, type_syss, "")))]
+ let val (max_relevant, type_sys) = best_slice ctxt in
+ [(1.0, (false, (max_relevant, type_sys, "")))]
end}
fun remotify_config system_name system_versions best_slice
@@ -406,36 +406,35 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
- (K (750, ["mangled_tags?"]) (* FUDGE *))
+ (K (750, "mangled_tags?") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
- (K (200, ["mangled_preds?"]) (* FUDGE *))
+ (K (200, "mangled_preds?") (* FUDGE *))
val remote_z3_atp =
- remotify_atp z3_atp "Z3" ["2.18"] (K (250, ["mangled_preds?"]) (* FUDGE *))
+ remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
val remote_leo2 =
remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
- (K (100, ["simple"]) (* FUDGE *))
+ (K (100, "simple") (* FUDGE *))
val remote_satallax =
remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
- (K (64, ["simple"]) (* FUDGE *))
+ (K (64, "simple") (* FUDGE *))
val remote_sine_e =
- remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config)
- Axiom Conjecture [FOF]
- (K (500, ["mangled_preds?"]) (* FUDGE *))
+ remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
+ Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))
val remote_snark =
remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
[("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
- [TFF, FOF] (K (100, ["simple"]) (* FUDGE *))
+ [TFF, FOF] (K (100, "simple") (* FUDGE *))
val remote_tofof_e =
remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
- Axiom Hypothesis [TFF] (K (150, ["simple"]) (* FUDGE *))
+ Axiom Hypothesis [TFF] (K (150, "simple") (* FUDGE *))
val remote_waldmeister =
remote_atp waldmeisterN "Waldmeister" ["710"]
[("#START OF PROOF", "Proved Goals:")]
[(OutOfResources, "Too many function symbols"),
(Crashed, "Unrecoverable Segmentation Fault")]
Hypothesis Hypothesis [CNF_UEQ]
- (K (50, ["mangled_tags?"]) (* FUDGE *))
+ (K (50, "mangled_tags?") (* FUDGE *))
(* Setup *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 13:52:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 27 13:52:47 2011 +0200
@@ -12,7 +12,6 @@
val auto : bool Unsynchronized.ref
val provers : string Unsynchronized.ref
val timeout : int Unsynchronized.ref
- val full_types : bool Unsynchronized.ref
val default_params : Proof.context -> (string * string) list -> params
val setup : theory -> theory
end;
@@ -65,7 +64,6 @@
val provers = Unsynchronized.ref ""
val timeout = Unsynchronized.ref 30
-val full_types = Unsynchronized.ref false
val _ =
ProofGeneralPgip.add_preference Preferences.category_proof
@@ -79,11 +77,6 @@
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)")
-val _ =
- ProofGeneralPgip.add_preference Preferences.category_proof
- (Preferences.bool_pref full_types
- "Sledgehammer: Full Types" "ATPs will use full type information")
-
type raw_param = string * string list
val default_default_params =
@@ -108,16 +101,15 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("non_blocking", "blocking"),
- ("partial_types", "full_types"),
("no_isar_proof", "isar_proof"),
("no_slicing", "slicing")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters",
+ ["debug", "verbose", "overlord", "type_sys", "max_mono_iters",
"max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
"preplay_timeout"]
-val property_dependent_params = ["provers", "full_types", "timeout"]
+val property_dependent_params = ["provers", "timeout"]
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
@@ -218,7 +210,6 @@
[("provers", [case !provers of
"" => default_provers_param_value ctxt
| s => s]),
- ("full_types", [if !full_types then "true" else "false"]),
("timeout", let val timeout = !timeout in
[if timeout <= 0 then "none"
else string_of_int timeout]
@@ -272,10 +263,10 @@
|> mode = Auto_Try ? single o hd
val type_sys =
if mode = Auto_Try then
- Smart_Type_Sys true
+ NONE
else case lookup_string "type_sys" of
- "smart" => Smart_Type_Sys (mode = Try orelse lookup_bool "full_types")
- | s => Dumb_Type_Sys (type_sys_from_string s)
+ "smart" => NONE
+ | s => SOME (type_sys_from_string s)
val relevance_thresholds = lookup_real_pair "relevance_thresholds"
val max_relevant = lookup_option lookup_int "max_relevant"
val max_mono_iters = lookup_int "max_mono_iters"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 13:52:47 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Jun 27 13:52:47 2011 +0200
@@ -18,17 +18,13 @@
datatype mode = Auto_Try | Try | Normal | Minimize
- datatype rich_type_sys =
- Dumb_Type_Sys of type_sys |
- Smart_Type_Sys of bool
-
type params =
{debug: bool,
verbose: bool,
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: rich_type_sys,
+ type_sys: type_sys option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -286,17 +282,13 @@
(** problems, results, ATPs, etc. **)
-datatype rich_type_sys =
- Dumb_Type_Sys of type_sys |
- Smart_Type_Sys of bool
-
type params =
{debug: bool,
verbose: bool,
overlord: bool,
blocking: bool,
provers: string list,
- type_sys: rich_type_sys,
+ type_sys: type_sys option,
relevance_thresholds: real * real,
max_relevant: int option,
max_mono_iters: int,
@@ -510,16 +502,11 @@
them each time. *)
val atp_important_message_keep_quotient = 10
-val fallback_best_type_syss =
- [Preds (Mangled_Monomorphic, Noninf_Nonmono_Types, Lightweight)]
-
-fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
- choose_format formats type_sys
- | choose_format_and_type_sys best_type_syss formats
- (Smart_Type_Sys full_types) =
- map type_sys_from_string best_type_syss @ fallback_best_type_syss
- |> find_first (if full_types then is_type_sys_virtually_sound else K true)
- |> the |> choose_format formats
+fun choose_format_and_type_sys best_type_sys formats type_sys_opt =
+ (case type_sys_opt of
+ SOME ts => ts
+ | NONE => type_sys_from_string best_type_sys)
+ |> choose_format formats
val metis_minimize_max_time = seconds 2.0
@@ -609,14 +596,14 @@
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, best_type_syss, extra))))
+ (best_max_relevant, best_type_sys, extra))))
time_left =
let
val num_facts =
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val (format, type_sys) =
- choose_format_and_type_sys best_type_syss formats type_sys
+ choose_format_and_type_sys best_type_sys formats type_sys
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> map untranslated_fact