# HG changeset patch # User blanchet # Date 1305206958 -7200 # Node ID 64dea91bbe0eb72d6dd637a5ecad4b9510273aae # Parent 4d6bcf846759b6f1dba94106f4ee318f1d8d8759 added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options diff -r 4d6bcf846759 -r 64dea91bbe0e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu May 12 15:29:18 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu May 12 15:29:18 2011 +0200 @@ -10,6 +10,10 @@ val keepK = "keep" val full_typesK = "full_types" val type_sysK = "type_sys" +val slicingK = "slicing" +val e_weight_methodK = "e_weight_method" +val spass_force_sosK = "spass_force_sos" +val vampire_force_sosK = "vampire_force_sos" val max_relevantK = "max_relevant" val minimizeK = "minimize" val minimize_timeoutK = "minimize_timeout" @@ -348,7 +352,8 @@ SH_FAIL of int * int | SH_ERROR -fun run_sh prover_name prover type_sys max_relevant hard_timeout timeout dir st = +fun run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos + vampire_force_sos hard_timeout timeout dir st = let val {context = ctxt, facts = chained_ths, goal} = Proof.goal st val i = 1 @@ -361,12 +366,19 @@ val st' = st |> Proof.map_context (change_dir dir + #> (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) #> Config.put Sledgehammer_Provers.measure_run_time true) val params as {relevance_thresholds, max_relevant, slicing, ...} = Sledgehammer_Isar.default_params ctxt [("verbose", "true"), ("type_sys", type_sys), ("max_relevant", max_relevant), + ("slicing", slicing), ("timeout", string_of_int timeout)] val default_max_relevant = Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing @@ -429,13 +441,20 @@ val (prover_name, prover) = get_prover (Proof.context_of st) args val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart" val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart" + val slicing = AList.lookup (op =) args slicingK |> the_default "true" + 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 + |> Option.map (curry (op <>) "false") val dir = AList.lookup (op =) args keepK val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30) (* always use a hard timeout, but give some slack so that the automatic minimizer has a chance to do its magic *) val hard_timeout = SOME (2 * timeout) val (msg, result) = - run_sh prover_name prover type_sys max_relevant hard_timeout timeout dir st + run_sh prover_name prover type_sys max_relevant slicing e_weight_method spass_force_sos + vampire_force_sos hard_timeout timeout dir st in case result of SH_OK (time_isa, time_prover, names) => diff -r 4d6bcf846759 -r 64dea91bbe0e src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Thu May 12 15:29:18 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu May 12 15:29:18 2011 +0200 @@ -31,6 +31,8 @@ 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 @@ -230,15 +232,18 @@ (* SPASS *) +val spass_force_sos = + Attrib.setup_config_bool @{binding atp_spass_force_sos} (K false) + (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) val spass_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass"), required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], - arguments = fn _ => fn slice => fn timeout => fn _ => + arguments = fn ctxt => fn slice => fn timeout => fn _ => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout)) - |> slice = 0 ? prefix "-SOS=1 ", + |> (slice = 0 orelse Config.get ctxt spass_force_sos) ? prefix "-SOS=1 ", proof_delims = [("Here is a proof", "Formulae used in the proof")], known_failures = known_perl_failures @ @@ -252,24 +257,30 @@ conj_sym_kind = Axiom, (* FIXME: try out Hypothesis *) prem_kind = Conjecture, formats = [Fof], - best_slices = + best_slices = fn ctxt => (* FUDGE *) - K [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *), - (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]} + [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *), + (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)] + |> (if Config.get ctxt spass_force_sos then hd #> apfst (K 1.0) #> single + else I)} val spass = (spassN, spass_config) (* 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 = [], - arguments = fn _ => fn slice => fn timeout => fn _ => + arguments = fn ctxt => fn slice => fn timeout => fn _ => (* This would work too but it's less tested: "--proof tptp " ^ *) "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ " --thanks \"Andrei and Krystof\" --input_file" - |> slice = 0 ? prefix "--sos on ", + |> (slice = 0 orelse Config.get ctxt vampire_force_sos) + ? prefix "--sos on ", proof_delims = [("=========== Refutation ==========", "======= End of refutation ======="), @@ -289,10 +300,12 @@ conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *) prem_kind = Conjecture, formats = [Fof], - best_slices = + best_slices = fn ctxt => (* FUDGE *) - K [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *), - (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]} + [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *), + (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)] + |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single + else I)} val vampire = (vampireN, vampire_config)