# HG changeset patch # User blanchet # Date 1312903997 -7200 # Node ID 5e14f591515e05a4dada3b5a6f285619c17b0337 # Parent 45078c8f5c1e58f0c1a9d51386cdb09079c62591 support local HOATPs diff -r 45078c8f5c1e -r 5e14f591515e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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) => diff -r 45078c8f5c1e -r 5e14f591515e src/HOL/Tools/ATP/atp_systems.ML --- 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;