added one slice with configurable simplification turned off
authorblanchet
Tue May 22 16:59:27 2012 +0200 (2012-05-22)
changeset 47955a2a821abab83
parent 47954 aada9fd08b58
child 47956 2a420750248b
added one slice with configurable simplification turned off
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 22 16:59:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 22 16:59:27 2012 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4       |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single else I)}
     1.5  
     1.6  val spass_new_H1SOS = "-Heuristic=1 -SOS"
     1.7 -val spass_new_H2 = "-Heuristic=2"
     1.8 +val spass_new_H2LR0LT0 = "-Heuristic=2 -LR=0 -LT=0"
     1.9  val spass_new_H2SOS = "-Heuristic=2 -SOS"
    1.10  val spass_new_H2NuVS0 = "-Heuristic=2 -RNuV=1 -Sorts=0"
    1.11  val spass_new_H2NuVS0Red2 =
    1.12 @@ -411,7 +411,7 @@
    1.13       (* FUDGE *)
    1.14       [(0.1667, (false, ((150, DFG DFG_Sorted, "mono_native", combsN, true), ""))),
    1.15        (0.1667, (false, ((500, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H2SOS))),
    1.16 -      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2))),
    1.17 +      (0.1666, (false, ((50, DFG DFG_Sorted,  "mono_native", liftingN, true), spass_new_H2LR0LT0))),
    1.18        (0.1000, (false, ((250, DFG DFG_Sorted, "mono_native", combsN, true), spass_new_H2NuVS0))),
    1.19        (0.1000, (false, ((1000, DFG DFG_Sorted, "mono_native", liftingN, true), spass_new_H1SOS))),
    1.20        (0.1000, (false, ((150, DFG DFG_Sorted, "poly_guards??", liftingN, false), spass_new_H2NuVS0Red2))),