make SPASS more configurable, for experiments
authorblanchet
Thu Jan 17 17:55:02 2013 +0100 (2013-01-17)
changeset 50950a145ee10371b
parent 50949 a5689bb4ed7e
child 50951 e1cbaa7d5536
make SPASS more configurable, for experiments
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Jan 15 20:26:38 2013 -0800
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jan 17 17:55:02 2013 +0100
     1.3 @@ -41,6 +41,13 @@
     1.4    val e_default_sym_offs_weight : real Config.T
     1.5    val e_sym_offs_weight_base : real Config.T
     1.6    val e_sym_offs_weight_span : real Config.T
     1.7 +  val spass_H1SOS : string
     1.8 +  val spass_H2 : string
     1.9 +  val spass_H2LR0LT0 : string
    1.10 +  val spass_H2NuVS0 : string
    1.11 +  val spass_H2NuVS0Red2 : string
    1.12 +  val spass_H2SOS : string
    1.13 +  val spass_extra_options : string Config.T
    1.14    val alt_ergoN : string
    1.15    val dummy_thfN : string
    1.16    val eN : string
    1.17 @@ -465,6 +472,9 @@
    1.18  val spass_H2NuVS0Red2 = "-Heuristic=2 -RNuV=1 -Sorts=0 -RFRew=2 -RBRew=2 -RTaut=2"
    1.19  val spass_H2SOS = "-Heuristic=2 -SOS"
    1.20  
    1.21 +val spass_extra_options =
    1.22 +  Attrib.setup_config_string @{binding atp_spass_extra_options} (K "")
    1.23 +
    1.24  (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
    1.25  val spass_config : atp_config =
    1.26    {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
    1.27 @@ -485,7 +495,7 @@
    1.28        (InternalError, "Please report this error")] @
    1.29        known_perl_failures,
    1.30     prem_role = Conjecture,
    1.31 -   best_slices = fn _ =>
    1.32 +   best_slices = fn ctxt =>
    1.33       (* FUDGE *)
    1.34       [(0.1667, ((150, DFG Monomorphic, "mono_native", combsN, true), "")),
    1.35        (0.1667, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS)),
    1.36 @@ -494,7 +504,10 @@
    1.37        (0.1000, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS)),
    1.38        (0.1000, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2)),
    1.39        (0.1000, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS)),
    1.40 -      (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))],
    1.41 +      (0.1000, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2))]
    1.42 +     |> (case Config.get ctxt spass_extra_options of
    1.43 +           "" => I
    1.44 +         | opts => map (apsnd (apsnd (K opts)))),
    1.45     best_max_mono_iters = default_max_mono_iters,
    1.46     best_max_new_mono_instances = default_max_new_mono_instances}
    1.47