# HG changeset patch # User blanchet # Date 1578404411 -3600 # Node ID 475b2260b9c4ab01cd259984787bee5c6351c333 # Parent 41f3ca717da5b79bf54edc0f6624062406a965f6 removed experimental option to SPASS diff -r 41f3ca717da5 -r 475b2260b9c4 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jan 07 12:37:12 2020 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jan 07 14:40:11 2020 +0100 @@ -45,7 +45,6 @@ val spass_H2NuVS0 : string val spass_H2NuVS0Red2 : string val spass_H2SOS : string - val spass_extra_options : string Config.T val is_vampire_noncommercial_license_accepted : unit -> bool option val remote_atp : string -> string -> string list -> (string * string) list -> (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) -> @@ -437,9 +436,6 @@ val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2" val spass_H2SOS = "-Heuristic=2 -SOS" -val spass_extra_options = - Attrib.setup_config_string \<^binding>\atp_spass_extra_options\ (K "") - val spass_config : atp_config = {exec = K (["SPASS_HOME"], ["SPASS"]), arguments = fn _ => fn full_proofs => fn extra_options => fn timeout => fn file_name => fn _ => @@ -466,10 +462,7 @@ (0.1000, (((1000, mepoN), DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)), (0.1000, (((150, meshN), DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)), (0.1000, (((300, meshN), DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)), - (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))] - |> (case Config.get ctxt spass_extra_options of - "" => I - | opts => map (apsnd (apsnd (K opts)))), + (0.1000, (((100, meshN), DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances}