--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Aug 04 15:02:02 2014 +0200
@@ -91,7 +91,7 @@
("max_mono_iters", "smart"),
("max_new_mono_instances", "smart"),
("isar_proofs", "smart"),
- ("compress", "10"),
+ ("compress", "smart"),
("try0", "true"),
("smt_proofs", "smart"),
("slice", "true"),
@@ -101,7 +101,7 @@
val alias_params =
[("prover", ("provers", [])), (* undocumented *)
("dont_preplay", ("preplay_timeout", ["0"])),
- ("dont_compress", ("compress", ["0"])),
+ ("dont_compress", ("compress", ["1"])),
("isar_proof", ("isar_proofs", [])) (* legacy *)]
val negated_alias_params =
[("no_debug", "debug"),
@@ -291,7 +291,7 @@
val max_new_mono_instances =
lookup_option lookup_int "max_new_mono_instances"
val isar_proofs = lookup_option lookup_bool "isar_proofs"
- val compress = Real.max (1.0, lookup_real "compress")
+ val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
val try0 = lookup_bool "try0"
val smt_proofs = lookup_option lookup_bool "smt_proofs"
val slice = mode <> Auto_Try andalso lookup_bool "slice"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 04 15:02:02 2014 +0200
@@ -16,7 +16,7 @@
val trace : bool Config.T
type isar_params =
- bool * (string option * string option) * Time.time * real * bool * bool
+ bool * (string option * string option) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
@@ -124,7 +124,7 @@
end
type isar_params =
- bool * (string option * string option) * Time.time * real * bool * bool
+ bool * (string option * string option) * Time.time * real option * bool * bool
* (term, string) atp_step list * thm
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
@@ -161,7 +161,10 @@
val ctxt = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
val do_preplay = preplay_timeout <> Time.zeroTime
- val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress
+ val compress =
+ (case compress of
+ NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0
+ | SOME n => n)
fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem
fun skolems_of ctxt t = Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Aug 04 14:19:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Aug 04 15:02:02 2014 +0200
@@ -35,7 +35,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
- compress : real,
+ compress : real option,
try0 : bool,
smt_proofs : bool option,
slice : bool,
@@ -126,7 +126,7 @@
max_mono_iters : int option,
max_new_mono_instances : int option,
isar_proofs : bool option,
- compress : real,
+ compress : real option,
try0 : bool,
smt_proofs : bool option,
slice : bool,