src/HOL/Tools/ATP/atp_systems.ML
changeset 42723 c1909691bbf0
parent 42710 84fcce345b5d
child 42725 64dea91bbe0e
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Thu May 12 15:29:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu May 12 15:29:18 2011 +0200
     1.3 @@ -22,8 +22,7 @@
     1.4       conj_sym_kind : formula_kind,
     1.5       prem_kind : formula_kind,
     1.6       formats : format list,
     1.7 -     best_slices : Proof.context -> (real * (bool * int)) list,
     1.8 -     best_type_systems : string list}
     1.9 +     best_slices : Proof.context -> (real * (bool * (int * string list))) list}
    1.10  
    1.11    val e_weight_method : string Config.T
    1.12    val e_default_fun_weight : real Config.T
    1.13 @@ -43,7 +42,7 @@
    1.14    val remote_atp :
    1.15      string -> string -> string list -> (string * string) list
    1.16      -> (failure * string) list -> formula_kind -> formula_kind -> format list
    1.17 -    -> (Proof.context -> int) -> string list -> string * atp_config
    1.18 +    -> (Proof.context -> int * string list) -> string * atp_config
    1.19    val add_atp : string * atp_config -> theory -> theory
    1.20    val get_atp : theory -> string -> atp_config
    1.21    val supported_atps : theory -> string list
    1.22 @@ -71,13 +70,19 @@
    1.23     conj_sym_kind : formula_kind,
    1.24     prem_kind : formula_kind,
    1.25     formats : format list,
    1.26 -   best_slices : Proof.context -> (real * (bool * int)) list,
    1.27 -   best_type_systems : string list}
    1.28 +   best_slices : Proof.context -> (real * (bool * (int * string list))) list}
    1.29  
    1.30 -(* "best_slices" and "best_type_systems" must be found empirically, taking a
    1.31 -    wholistic approach since the ATPs are run in parallel. "best_type_systems"
    1.32 -    should be of the form [sound] or [unsound, sound], where "sound" is a sound
    1.33 -    type system and "unsound" is an unsound one. *)
    1.34 +(* "best_slices" must be found empirically, taking a wholistic approach since
    1.35 +   the ATPs are run in parallel. The "real" components give the faction of the
    1.36 +   time available given to the slice; these should add up to 1.0. The "bool"
    1.37 +   component indicates whether the slice's strategy is complete; the "int", the
    1.38 +   preferred number of facts to pass; the "string list", the preferred type
    1.39 +   systems, which should be of the form [sound] or [unsound, sound], where
    1.40 +   "sound" is a sound type system and "unsound" is an unsound one.
    1.41 +
    1.42 +   The last slice should be the most "normal" one, because it will get all the
    1.43 +   time available if the other slices fail early and also because it is used for
    1.44 +   remote provers and if slicing is disabled. *)
    1.45  
    1.46  val known_perl_failures =
    1.47    [(CantConnect, "HTTP error"),
    1.48 @@ -212,13 +217,13 @@
    1.49     prem_kind = Conjecture,
    1.50     formats = [Fof],
    1.51     best_slices = fn ctxt =>
    1.52 +     (* FUDGE *)
    1.53       if effective_e_weight_method ctxt = e_slicesN then
    1.54 -       [(0.33333, (true, 100 (* FUDGE *))) (* sym_offset_weight *),
    1.55 -        (0.33333, (true, 1000 (* FUDGE *))) (* auto *),
    1.56 -        (0.33334, (true, 200 (* FUDGE *))) (* fun_weight *)]
    1.57 +       [(0.333, (true, (100, ["mangled_preds?"]))) (* sym_offset_weight *),
    1.58 +        (0.333, (true, (1000, ["mangled_preds?"]))) (* auto *),
    1.59 +        (0.334, (true, (200, ["mangled_preds?"]))) (* fun_weight *)]
    1.60       else
    1.61 -       [(1.0, (true, 250 (* FUDGE *)))],
    1.62 -   best_type_systems = ["mangled_preds?"]}
    1.63 +       [(1.0, (true, (250, ["mangled_preds?"])))]}
    1.64  
    1.65  val e = (eN, e_config)
    1.66  
    1.67 @@ -248,9 +253,9 @@
    1.68     prem_kind = Conjecture,
    1.69     formats = [Fof],
    1.70     best_slices =
    1.71 -     K [(0.66667, (false, 150 (* FUDGE *))) (* with SOS *),
    1.72 -        (0.33333, (true, 150 (* FUDGE *))) (* without SOS *)],
    1.73 -   best_type_systems = ["mangled_preds"]}
    1.74 +     (* FUDGE *)
    1.75 +     K [(0.667, (false, (150, ["mangled_preds"]))) (* SOS *),
    1.76 +        (0.333, (true, (150, ["mangled_preds"]))) (* ~SOS *)]}
    1.77  
    1.78  val spass = (spassN, spass_config)
    1.79  
    1.80 @@ -285,9 +290,9 @@
    1.81     prem_kind = Conjecture,
    1.82     formats = [Fof],
    1.83     best_slices =
    1.84 -     K [(0.66667, (false, 450 (* FUDGE *))) (* with SOS *),
    1.85 -        (0.33333, (true, 450 (* FUDGE *))) (* without SOS *)],
    1.86 -   best_type_systems = ["mangled_tags!", "mangled_preds?"]}
    1.87 +     (* FUDGE *)
    1.88 +     K [(0.667, (false, (450, ["mangled_tags!", "mangled_preds?"]))) (* SOS *),
    1.89 +        (0.333, (true, (450, ["mangled_tags!", "mangled_preds?"]))) (* ~SOS *)]}
    1.90  
    1.91  val vampire = (vampireN, vampire_config)
    1.92  
    1.93 @@ -309,8 +314,9 @@
    1.94     conj_sym_kind = Hypothesis,
    1.95     prem_kind = Hypothesis,
    1.96     formats = [Fof],
    1.97 -   best_slices = K [(1.0, (false, 250 (* FUDGE *)))],
    1.98 -   best_type_systems = [] (* FIXME *)}
    1.99 +   best_slices =
   1.100 +     (* FUDGE (FIXME) *)
   1.101 +     K [(1.0, (false, (250, [])))]}
   1.102  
   1.103  val z3_atp = (z3_atpN, z3_atp_config)
   1.104  
   1.105 @@ -348,8 +354,7 @@
   1.106  val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
   1.107  
   1.108  fun remote_config system_name system_versions proof_delims known_failures
   1.109 -                  conj_sym_kind prem_kind formats best_max_relevant
   1.110 -                  best_type_systems : atp_config =
   1.111 +                  conj_sym_kind prem_kind formats best_slice : atp_config =
   1.112    {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
   1.113     required_execs = [],
   1.114     arguments = fn _ => fn _ => fn timeout => fn _ =>
   1.115 @@ -364,24 +369,20 @@
   1.116     conj_sym_kind = conj_sym_kind,
   1.117     prem_kind = prem_kind,
   1.118     formats = formats,
   1.119 -   best_slices = fn ctxt => [(1.0, (false, best_max_relevant ctxt))],
   1.120 -   best_type_systems = best_type_systems}
   1.121 -
   1.122 -fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
   1.123 +   best_slices = fn ctxt => [(1.0, (false, best_slice ctxt))]}
   1.124  
   1.125  fun remotify_config system_name system_versions
   1.126          ({proof_delims, known_failures, conj_sym_kind, prem_kind, formats,
   1.127 -          best_slices, best_type_systems, ...} : atp_config) : atp_config =
   1.128 +          best_slices, ...} : atp_config) : atp_config =
   1.129    remote_config system_name system_versions proof_delims known_failures
   1.130                  conj_sym_kind prem_kind formats
   1.131 -                (int_average (snd o snd) o best_slices) best_type_systems
   1.132 +                (best_slices #> List.last #> snd #> snd)
   1.133  
   1.134  fun remote_atp name system_name system_versions proof_delims known_failures
   1.135 -        conj_sym_kind prem_kind formats best_max_relevant best_type_systems =
   1.136 +        conj_sym_kind prem_kind formats best_slice =
   1.137    (remote_prefix ^ name,
   1.138     remote_config system_name system_versions proof_delims known_failures
   1.139 -                 conj_sym_kind prem_kind formats best_max_relevant
   1.140 -                 best_type_systems)
   1.141 +                 conj_sym_kind prem_kind formats best_slice)
   1.142  fun remotify_atp (name, config) system_name system_versions =
   1.143    (remote_prefix ^ name, remotify_config system_name system_versions config)
   1.144  
   1.145 @@ -390,14 +391,14 @@
   1.146  val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
   1.147  val remote_tofof_e =
   1.148    remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
   1.149 -             Axiom Conjecture [Tff] (K 200 (* FUDGE *)) ["simple"]
   1.150 +             Axiom Conjecture [Tff] (K (200, ["simple_types"]) (* FUDGE *))
   1.151  val remote_sine_e =
   1.152    remote_atp sine_eN "SInE" ["0.4"] [] [] Axiom Conjecture [Fof]
   1.153 -             (K 500 (* FUDGE *)) ["args", "preds", "tags"]
   1.154 +             (K (500, ["poly_args"]) (* FUDGE *))
   1.155  val remote_snark =
   1.156    remote_atp snarkN "SNARK" ["20080805r024"]
   1.157               [("refutation.", "end_refutation.")] [] Hypothesis Conjecture
   1.158 -             [Tff, Fof] (K 250 (* FUDGE *)) ["simple"]
   1.159 +             [Tff, Fof] (K (250, ["simple_types"]) (* FUDGE *))
   1.160  
   1.161  (* Setup *)
   1.162