1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
     1.3 @@ -11,15 +11,23 @@
     1.4    type formula_kind = ATP_Problem.formula_kind
     1.5    type failure = ATP_Proof.failure
     1.6  
     1.7 +  datatype type_level = Level_All | Level_Some | Level_None
     1.8 +  datatype type_system =
     1.9 +    Many_Typed |
    1.10 +    Mangled of type_level |
    1.11 +    Args of bool * type_level |
    1.12 +    Tags of bool * type_level
    1.13 +
    1.14    type atp_config =
    1.15 -    {exec: string * string,
    1.16 -     required_execs: (string * string) list,
    1.17 -     arguments: int -> Time.time -> (unit -> (string * real) list) -> string,
    1.18 -     slices: unit -> (real * (bool * int)) list,
    1.19 -     proof_delims: (string * string) list,
    1.20 -     known_failures: (failure * string) list,
    1.21 -     hypothesis_kind: formula_kind,
    1.22 -     formats: format list}
    1.23 +    {exec : string * string,
    1.24 +     required_execs : (string * string) list,
    1.25 +     arguments : int -> Time.time -> (unit -> (string * real) list) -> string,
    1.26 +     proof_delims : (string * string) list,
    1.27 +     known_failures : (failure * string) list,
    1.28 +     hypothesis_kind : formula_kind,
    1.29 +     formats : format list,
    1.30 +     best_slices : unit -> (real * (bool * int)) list,
    1.31 +     best_type_systems : type_system list}
    1.32  
    1.33    datatype e_weight_method =
    1.34      E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
    1.35 @@ -43,8 +51,8 @@
    1.36    val remote_prefix : string
    1.37    val remote_atp :
    1.38      string -> string -> string list -> (string * string) list
    1.39 -    -> (failure * string) list -> (unit -> int) -> formula_kind -> format list
    1.40 -    -> string * atp_config
    1.41 +    -> (failure * string) list -> formula_kind -> format list -> (unit -> int)
    1.42 +    -> type_system list -> string * atp_config
    1.43    val add_atp : string * atp_config -> theory -> theory
    1.44    val get_atp : theory -> string -> atp_config
    1.45    val supported_atps : theory -> string list
    1.46 @@ -61,15 +69,23 @@
    1.47  
    1.48  (* ATP configuration *)
    1.49  
    1.50 +datatype type_level = Level_All | Level_Some | Level_None
    1.51 +datatype type_system =
    1.52 +  Many_Typed |
    1.53 +  Mangled of type_level |
    1.54 +  Args of bool * type_level |
    1.55 +  Tags of bool * type_level
    1.56 +
    1.57  type atp_config =
    1.58 -  {exec: string * string,
    1.59 -   required_execs: (string * string) list,
    1.60 -   arguments: int -> Time.time -> (unit -> (string * real) list) -> string,
    1.61 -   slices: unit -> (real * (bool * int)) list,
    1.62 -   proof_delims: (string * string) list,
    1.63 -   known_failures: (failure * string) list,
    1.64 -   hypothesis_kind: formula_kind,
    1.65 -   formats: format list}
    1.66 +  {exec : string * string,
    1.67 +   required_execs : (string * string) list,
    1.68 +   arguments : int -> Time.time -> (unit -> (string * real) list) -> string,
    1.69 +   proof_delims : (string * string) list,
    1.70 +   known_failures : (failure * string) list,
    1.71 +   hypothesis_kind : formula_kind,
    1.72 +   formats : format list,
    1.73 +   best_slices : unit -> (real * (bool * int)) list,
    1.74 +   best_type_systems : type_system list}
    1.75  
    1.76  val known_perl_failures =
    1.77    [(CantConnect, "HTTP error"),
    1.78 @@ -177,13 +193,6 @@
    1.79       e_weight_arguments (method_for_slice slice) weights ^
    1.80       " -tAutoDev --silent --cpu-limit=" ^
    1.81       string_of_int (to_secs (e_bonus ()) timeout),
    1.82 -   slices = fn () =>
    1.83 -     if effective_e_weight_method () = E_Slices then
    1.84 -       [(0.33333, (true, 100 (* FUDGE *))) (* E_Sym_Offset_Weight *),
    1.85 -        (0.33333, (true, 1000 (* FUDGE *))) (* E_Auto *),
    1.86 -        (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
    1.87 -     else
    1.88 -       [(1.0, (true, 250 (* FUDGE *)))],
    1.89     proof_delims = [tstp_proof_delims],
    1.90     known_failures =
    1.91       [(Unprovable, "SZS status: CounterSatisfiable"),
    1.92 @@ -195,7 +204,15 @@
    1.93        (OutOfResources, "SZS status: ResourceOut"),
    1.94        (OutOfResources, "SZS status ResourceOut")],
    1.95     hypothesis_kind = Conjecture,
    1.96 -   formats = [Fof]}
    1.97 +   formats = [Fof],
    1.98 +   best_slices = fn () =>
    1.99 +     if effective_e_weight_method () = E_Slices then
   1.100 +       [(0.33333, (true, 100 (* FUDGE *))) (* E_Sym_Offset_Weight *),
   1.101 +        (0.33333, (true, 1000 (* FUDGE *))) (* E_Auto *),
   1.102 +        (0.33334, (true, 200 (* FUDGE *))) (* E_Fun_Weight *)]
   1.103 +     else
   1.104 +       [(1.0, (true, 250 (* FUDGE *)))],
   1.105 +   best_type_systems = []}
   1.106  
   1.107  val e = (eN, e_config)
   1.108  
   1.109 @@ -211,8 +228,6 @@
   1.110       ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
   1.111        \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
   1.112       |> slice = 0 ? prefix "-SOS=1 ",
   1.113 -   slices = K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
   1.114 -               (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
   1.115     proof_delims = [("Here is a proof", "Formulae used in the proof")],
   1.116     known_failures =
   1.117       known_perl_failures @
   1.118 @@ -224,7 +239,11 @@
   1.119        (SpassTooOld, "tptp2dfg"),
   1.120        (InternalError, "Please report this error")],
   1.121     hypothesis_kind = Conjecture,
   1.122 -   formats = [Fof]}
   1.123 +   formats = [Fof],
   1.124 +   best_slices =
   1.125 +     K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
   1.126 +        (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
   1.127 +   best_type_systems = []}
   1.128  
   1.129  val spass = (spassN, spass_config)
   1.130  
   1.131 @@ -239,8 +258,6 @@
   1.132       "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
   1.133       " --thanks \"Andrei and Krystof\" --input_file"
   1.134       |> slice = 0 ? prefix "--sos on ",
   1.135 -   slices = K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
   1.136 -               (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
   1.137     proof_delims =
   1.138       [("=========== Refutation ==========",
   1.139         "======= End of refutation ======="),
   1.140 @@ -258,7 +275,11 @@
   1.141        (VampireTooOld, "not a valid option"),
   1.142        (Interrupted, "Aborted by signal SIGINT")],
   1.143     hypothesis_kind = Conjecture,
   1.144 -   formats = [Fof]}
   1.145 +   formats = [Fof],
   1.146 +   best_slices =
   1.147 +     K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
   1.148 +        (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
   1.149 +   best_type_systems = []}
   1.150  
   1.151  val vampire = (vampireN, vampire_config)
   1.152  
   1.153 @@ -270,7 +291,6 @@
   1.154     required_execs = [],
   1.155     arguments = fn _ => fn timeout => fn _ =>
   1.156       "MBQI=true -p -t:" ^ string_of_int (to_secs 0 timeout),
   1.157 -   slices = K [(1.0, (false, 250 (* FUDGE *)))],
   1.158     proof_delims = [],
   1.159     known_failures =
   1.160       [(Unprovable, "\nsat"),
   1.161 @@ -279,7 +299,9 @@
   1.162        (ProofMissing, "\nunsat"),
   1.163        (ProofMissing, "SZS status Unsatisfiable")],
   1.164     hypothesis_kind = Hypothesis,
   1.165 -   formats = [Fof]}
   1.166 +   formats = [Fof],
   1.167 +   best_slices = K [(1.0, (false, 250 (* FUDGE *)))],
   1.168 +   best_type_systems = []}
   1.169  
   1.170  val z3_atp = (z3_atpN, z3_atp_config)
   1.171  
   1.172 @@ -317,34 +339,38 @@
   1.173  val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   1.174  
   1.175  fun remote_config system_name system_versions proof_delims known_failures
   1.176 -                  default_max_relevant hypothesis_kind formats : atp_config =
   1.177 +                  hypothesis_kind formats best_max_relevant best_type_systems
   1.178 +                  : atp_config =
   1.179    {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   1.180     required_execs = [],
   1.181     arguments = fn _ => fn timeout => fn _ =>
   1.182       " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
   1.183       ^ " -s " ^ the_system system_name system_versions,
   1.184 -   slices = fn () => [(1.0, (false, default_max_relevant ()))],
   1.185     proof_delims = insert (op =) tstp_proof_delims proof_delims,
   1.186     known_failures =
   1.187       known_failures @ known_perl_failures @
   1.188       [(IncompleteUnprovable, "says Unknown"),
   1.189        (TimedOut, "says Timeout")],
   1.190     hypothesis_kind = hypothesis_kind,
   1.191 -   formats = formats}
   1.192 +   formats = formats,
   1.193 +   best_slices = fn () => [(1.0, (false, best_max_relevant ()))],
   1.194 +   best_type_systems = best_type_systems}
   1.195  
   1.196  fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
   1.197  
   1.198  fun remotify_config system_name system_versions
   1.199 -                    ({proof_delims, slices, known_failures, hypothesis_kind,
   1.200 -                      formats, ...} : atp_config) : atp_config =
   1.201 +                    ({proof_delims, known_failures, hypothesis_kind, formats,
   1.202 +                      best_slices, best_type_systems, ...} : atp_config)
   1.203 +                    : atp_config =
   1.204    remote_config system_name system_versions proof_delims known_failures
   1.205 -                (int_average (snd o snd) o slices) hypothesis_kind formats
   1.206 +                hypothesis_kind formats
   1.207 +                (int_average (snd o snd) o best_slices) best_type_systems
   1.208  
   1.209  fun remote_atp name system_name system_versions proof_delims known_failures
   1.210 -               default_max_relevant hypothesis_kind formats =
   1.211 +               hypothesis_kind formats best_max_relevant best_type_systems =
   1.212    (remote_prefix ^ name,
   1.213     remote_config system_name system_versions proof_delims known_failures
   1.214 -                 default_max_relevant hypothesis_kind formats)
   1.215 +                 hypothesis_kind formats best_max_relevant best_type_systems)
   1.216  fun remotify_atp (name, config) system_name system_versions =
   1.217    (remote_prefix ^ name, remotify_config system_name system_versions config)
   1.218  
   1.219 @@ -353,13 +379,14 @@
   1.220  val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
   1.221  val remote_tofof_e =
   1.222    remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
   1.223 -             (K 200 (* FUDGE *)) Conjecture [Tff]
   1.224 +             Conjecture [Tff] (K 200 (* FUDGE *)) []
   1.225  val remote_sine_e =
   1.226 -  remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) Conjecture [Fof]
   1.227 +  remote_atp sine_eN "SInE" ["0.4"] [] [] Conjecture [Fof] (K 500 (* FUDGE *))
   1.228 +                     []
   1.229  val remote_snark =
   1.230    remote_atp snarkN "SNARK" ["20080805r024"]
   1.231 -             [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *))
   1.232 -             Conjecture [Tff, Fof]
   1.233 +             [("refutation.", "end_refutation.")] [] Conjecture [Tff, Fof]
   1.234 +             (K 250 (* FUDGE *)) []
   1.235  
   1.236  (* Setup *)
   1.237  

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
     2.3 @@ -138,7 +138,7 @@
     2.4        SMT_Solver.default_max_relevant ctxt name
     2.5      else
     2.6        fold (Integer.max o snd o snd o snd)
     2.7 -           (get_slices slicing (#slices (get_atp thy name) ())) 0
     2.8 +           (get_slices slicing (#best_slices (get_atp thy name) ())) 0
     2.9    end
    2.10  
    2.11  (* These are either simplified away by "Meson.presimplify" (most of the time) or
    2.12 @@ -339,8 +339,8 @@
    2.13    | must_monomorphize _ = false
    2.14  
    2.15  fun run_atp auto name
    2.16 -        ({exec, required_execs, arguments, slices, proof_delims, known_failures,
    2.17 -          hypothesis_kind, ...} : atp_config)
    2.18 +        ({exec, required_execs, arguments, proof_delims, known_failures,
    2.19 +          hypothesis_kind, best_slices, ...} : atp_config)
    2.20          ({debug, verbose, overlord, type_sys, max_relevant, monomorphize,
    2.21            monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor,
    2.22            slicing, timeout, ...} : params)
    2.23 @@ -385,7 +385,7 @@
    2.24            let
    2.25              (* If slicing is disabled, we expand the last slice to fill the
    2.26                 entire time available. *)
    2.27 -            val actual_slices = get_slices slicing (slices ())
    2.28 +            val actual_slices = get_slices slicing (best_slices ())
    2.29              val num_actual_slices = length actual_slices
    2.30              fun monomorphize_facts facts =
    2.31                let