--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 09 17:33:17 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 09 17:33:17 2011 +0200
@@ -13,8 +13,7 @@
val slicingK = "slicing"
val lambda_translationK = "lambda_translation"
val e_weight_methodK = "e_weight_method"
-val spass_force_sosK = "spass_force_sos"
-val vampire_force_sosK = "vampire_force_sos"
+val force_sosK = "force_sos"
val max_relevantK = "max_relevant"
val minimizeK = "minimize"
val minimize_timeoutK = "minimize_timeout"
@@ -354,8 +353,8 @@
SH_ERROR
fun run_sh prover_name prover type_enc sound max_relevant slicing
- lambda_translation e_weight_method spass_force_sos vampire_force_sos
- hard_timeout timeout dir pos st =
+ lambda_translation e_weight_method force_sos hard_timeout timeout dir
+ pos st =
let
val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
val i = 1
@@ -375,10 +374,8 @@
lambda_translation |> the_default I)
#> (Option.map (Config.put ATP_Systems.e_weight_method)
e_weight_method |> the_default I)
- #> (Option.map (Config.put ATP_Systems.spass_force_sos)
- spass_force_sos |> the_default I)
- #> (Option.map (Config.put ATP_Systems.vampire_force_sos)
- vampire_force_sos |> the_default I)
+ #> (Option.map (Config.put ATP_Systems.force_sos)
+ force_sos |> the_default I)
#> Config.put Sledgehammer_Provers.measure_run_time true)
val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
@@ -466,9 +463,7 @@
val slicing = AList.lookup (op =) args slicingK |> the_default "true"
val lambda_translation = AList.lookup (op =) args lambda_translationK
val e_weight_method = AList.lookup (op =) args e_weight_methodK
- val spass_force_sos = AList.lookup (op =) args spass_force_sosK
- |> Option.map (curry (op <>) "false")
- val vampire_force_sos = AList.lookup (op =) args vampire_force_sosK
+ val force_sos = AList.lookup (op =) args force_sosK
|> Option.map (curry (op <>) "false")
val dir = AList.lookup (op =) args keepK
val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
@@ -477,8 +472,8 @@
val hard_timeout = SOME (2 * timeout)
val (msg, result) =
run_sh prover_name prover type_enc sound max_relevant slicing
- lambda_translation e_weight_method spass_force_sos vampire_force_sos
- hard_timeout timeout dir pos st
+ lambda_translation e_weight_method force_sos hard_timeout timeout dir
+ pos st
in
case result of
SH_OK (time_isa, time_prover, names) =>
--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 09 17:33:17 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 09 17:33:17 2011 +0200
@@ -25,6 +25,7 @@
best_slices :
Proof.context -> (real * (bool * (int * string * string))) list}
+ val force_sos : bool Config.T
val e_smartN : string
val e_autoN : string
val e_fun_weightN : string
@@ -36,8 +37,6 @@
val e_default_sym_offs_weight : real Config.T
val e_sym_offs_weight_base : real Config.T
val e_sym_offs_weight_span : real Config.T
- val spass_force_sos : bool Config.T
- val vampire_force_sos : bool Config.T
val eN : string
val spassN : string
val vampireN : string
@@ -103,11 +102,11 @@
(* named ATPs *)
val eN = "e"
+val leo2N = "leo2"
+val satallaxN = "satallax"
val spassN = "spass"
val vampireN = "vampire"
val z3_atpN = "z3_atp"
-val leo2N = "leo2"
-val satallaxN = "satallax"
val e_sineN = "e_sine"
val snarkN = "snark"
val e_tofofN = "e_tofof"
@@ -128,6 +127,8 @@
val sosN = "sos"
val no_sosN = "no_sos"
+val force_sos = Attrib.setup_config_bool @{binding atp_force_sos} (K false)
+
(* E *)
@@ -228,10 +229,49 @@
val e = (eN, e_config)
-(* SPASS *)
+(* LEO-II *)
+
+val leo2_config : atp_config =
+ {exec = ("LEO2_HOME", "leo"),
+ required_execs = [],
+ arguments =
+ fn _ => fn _ => fn sos => fn timeout => fn _ =>
+ "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
+ |> sos = sosN ? prefix "--sos ",
+ proof_delims = tstp_proof_delims,
+ known_failures = [],
+ conj_sym_kind = Axiom,
+ prem_kind = Hypothesis,
+ formats = [THF, FOF],
+ best_slices = fn ctxt =>
+ (* FUDGE *)
+ [(0.667, (false, (150, "simple_higher", sosN))),
+ (0.333, (true, (50, "simple_higher", no_sosN)))]
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
+ else I)}
-val spass_force_sos =
- Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false)
+val leo2 = (leo2N, leo2_config)
+
+
+(* Satallax *)
+
+val satallax_config : atp_config =
+ {exec = ("SATALLAX_HOME", "satallax"),
+ required_execs = [],
+ arguments =
+ fn _ => fn _ => fn _ => fn timeout => fn _ =>
+ "-t " ^ string_of_int (to_secs 1 timeout),
+ proof_delims = tstp_proof_delims,
+ known_failures = [(ProofMissing, "SZS status Theorem")],
+ conj_sym_kind = Axiom,
+ prem_kind = Hypothesis,
+ formats = [THF],
+ best_slices = K [(1.0, (true, (100, "simple_higher", "")))] (* FUDGE *)}
+
+val satallax = (satallaxN, satallax_config)
+
+
+(* SPASS *)
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
@@ -260,7 +300,7 @@
[(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
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val spass = (spassN, spass_config)
@@ -268,9 +308,6 @@
(* Vampire *)
-val vampire_force_sos =
- Attrib.setup_config_bool @{binding atp_vampire_force_sos} (K false)
-
val vampire_config : atp_config =
{exec = ("VAMPIRE_HOME", "vampire"),
required_execs = [],
@@ -301,7 +338,7 @@
[(0.333, (false, (150, "poly_guards", sosN))),
(0.334, (true, (50, "mangled_guards?", no_sosN))),
(0.333, (false, (500, "mangled_tags?", sosN)))]
- |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
+ |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val vampire = (vampireN, vampire_config)
@@ -411,17 +448,17 @@
val remote_e =
remotify_atp e "EP" ["1.0", "1.1", "1.2"]
(K (750, "mangled_tags?") (* FUDGE *))
+val remote_leo2 =
+ remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
+ (K (100, "simple_higher") (* FUDGE *))
+val remote_satallax =
+ remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
+ (K (100, "simple_higher") (* FUDGE *))
val remote_vampire =
remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"]
(K (200, "mangled_guards?") (* FUDGE *))
val remote_z3_atp =
remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_guards?") (* FUDGE *))
-val remote_leo2 =
- remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF, FOF]
- (K (100, "simple_higher") (* FUDGE *))
-val remote_satallax =
- remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
- (K (64, "simple_higher") (* FUDGE *))
val remote_e_sine =
remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
Conjecture [FOF] (K (500, "mangled_guards?") (* FUDGE *))
@@ -461,9 +498,9 @@
Synchronized.change systems (fn _ => get_systems ())
val atps =
- [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp,
- remote_leo2, remote_satallax, remote_e_sine, remote_snark, remote_e_tofof,
- remote_waldmeister]
+ [e, leo2, satallax, spass, vampire, z3_atp, remote_e, remote_leo2,
+ remote_satallax, remote_vampire, remote_z3_atp, remote_e_sine, remote_snark,
+ remote_e_tofof, remote_waldmeister]
val setup = fold add_atp atps
end;