1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 04 07:40:02 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 04 12:08:18 2012 +0100
1.3 @@ -11,6 +11,7 @@
1.4 type formula_kind = ATP_Problem.formula_kind
1.5 type failure = ATP_Proof.failure
1.6
1.7 + type slice_spec = int * atp_format * string * string * bool
1.8 type atp_config =
1.9 {exec : string * string,
1.10 required_execs : (string * string) list,
1.11 @@ -22,9 +23,7 @@
1.12 conj_sym_kind : formula_kind,
1.13 prem_kind : formula_kind,
1.14 best_slices :
1.15 - Proof.context
1.16 - -> (real * (bool * ((int * atp_format * string * string) * string)))
1.17 - list}
1.18 + Proof.context -> (real * (bool * (slice_spec * string))) list}
1.19
1.20 val force_sos : bool Config.T
1.21 val e_smartN : string
1.22 @@ -58,8 +57,7 @@
1.23 val remote_atp :
1.24 string -> string -> string list -> (string * string) list
1.25 -> (failure * string) list -> formula_kind -> formula_kind
1.26 - -> (Proof.context -> int * atp_format * string * string)
1.27 - -> string * atp_config
1.28 + -> (Proof.context -> slice_spec) -> string * atp_config
1.29 val add_atp : string * atp_config -> theory -> theory
1.30 val get_atp : theory -> string -> atp_config
1.31 val supported_atps : theory -> string list
1.32 @@ -77,6 +75,8 @@
1.33
1.34 (* ATP configuration *)
1.35
1.36 +type slice_spec = int * atp_format * string * string * bool
1.37 +
1.38 type atp_config =
1.39 {exec : string * string,
1.40 required_execs : (string * string) list,
1.41 @@ -87,17 +87,16 @@
1.42 known_failures : (failure * string) list,
1.43 conj_sym_kind : formula_kind,
1.44 prem_kind : formula_kind,
1.45 - best_slices :
1.46 - Proof.context
1.47 - -> (real * (bool * ((int * atp_format * string * string) * string))) list}
1.48 + best_slices : Proof.context -> (real * (bool * (slice_spec * string))) list}
1.49
1.50 (* "best_slices" must be found empirically, taking a wholistic approach since
1.51 the ATPs are run in parallel. The "real" component gives the faction of the
1.52 - time available given to the slice and should add up to 1.0. The "bool"
1.53 + time available given to the slice and should add up to 1.0. The first "bool"
1.54 component indicates whether the slice's strategy is complete; the "int", the
1.55 preferred number of facts to pass; the first "string", the preferred type
1.56 system (which should be sound or quasi-sound); the second "string", the
1.57 - preferred lambda translation scheme; the third "string", extra information to
1.58 + preferred lambda translation scheme; the second "bool", whether uncurried
1.59 + aliased should be generated; the third "string", extra information to
1.60 the prover (e.g., SOS or no SOS).
1.61
1.62 The last slice should be the most "normal" one, because it will get all the
1.63 @@ -248,12 +247,14 @@
1.64 let val method = effective_e_weight_method ctxt in
1.65 (* FUDGE *)
1.66 if method = e_smartN then
1.67 - [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))),
1.68 - (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))),
1.69 - (0.333, (true, ((1000, FOF, "mono_tags??", combsN),
1.70 + [(0.333, (true, ((500, FOF, "mono_tags??", combsN, false),
1.71 + e_fun_weightN))),
1.72 + (0.334, (true, ((50, FOF, "mono_guards??", combsN, false),
1.73 + e_fun_weightN))),
1.74 + (0.333, (true, ((1000, FOF, "mono_tags??", combsN, false),
1.75 e_sym_offset_weightN)))]
1.76 else
1.77 - [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))]
1.78 + [(1.0, (true, ((500, FOF, "mono_tags??", combsN, false), method)))]
1.79 end}
1.80
1.81 val e = (eN, e_config)
1.82 @@ -278,9 +279,9 @@
1.83 prem_kind = Hypothesis,
1.84 best_slices = fn ctxt =>
1.85 (* FUDGE *)
1.86 - [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN),
1.87 + [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN, false),
1.88 sosN))),
1.89 - (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN),
1.90 + (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN, false),
1.91 no_sosN)))]
1.92 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.93 else I)}
1.94 @@ -305,8 +306,8 @@
1.95 prem_kind = Hypothesis,
1.96 best_slices =
1.97 (* FUDGE *)
1.98 - K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN),
1.99 - "")))]}
1.100 + K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN,
1.101 + false), "")))]}
1.102
1.103 val satallax = (satallaxN, satallax_config)
1.104
1.105 @@ -338,20 +339,20 @@
1.106 prem_kind = Conjecture,
1.107 best_slices = fn ctxt =>
1.108 (* FUDGE *)
1.109 - [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN),
1.110 + [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
1.111 sosN))),
1.112 - (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN),
1.113 + (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN, false),
1.114 sosN))),
1.115 - (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN),
1.116 + (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN, false),
1.117 no_sosN)))]
1.118 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.119 else I)}
1.120
1.121 val spass = (spassN, spass_config)
1.122
1.123 -val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN)
1.124 -val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN)
1.125 -val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN)
1.126 +val spass_new_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN, true)
1.127 +val spass_new_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN, true)
1.128 +val spass_new_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN, true)
1.129
1.130 (* Experimental *)
1.131 val spass_new_config : atp_config =
1.132 @@ -368,9 +369,9 @@
1.133 prem_kind = #prem_kind spass_config,
1.134 best_slices = fn _ =>
1.135 (* FUDGE *)
1.136 - [(0.300, (true, (spass_new_macro_slice_1, ""))),
1.137 - (0.333, (true, (spass_new_macro_slice_2, ""))),
1.138 - (0.333, (true, (spass_new_macro_slice_3, "")))]}
1.139 + [(0.300, (true, (spass_new_slice_1, ""))),
1.140 + (0.333, (true, (spass_new_slice_2, ""))),
1.141 + (0.333, (true, (spass_new_slice_3, "")))]}
1.142
1.143 val spass_new = (spass_newN, spass_new_config)
1.144
1.145 @@ -410,18 +411,19 @@
1.146 best_slices = fn ctxt =>
1.147 (* FUDGE *)
1.148 (if is_old_vampire_version () then
1.149 - [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN),
1.150 - sosN))),
1.151 - (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))),
1.152 - (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN),
1.153 + [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN, false),
1.154 + sosN))),
1.155 + (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN, false),
1.156 + sosN))),
1.157 + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN, false),
1.158 no_sosN)))]
1.159 else
1.160 [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
1.161 - combs_or_liftingN), sosN))),
1.162 - (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN),
1.163 - sosN))),
1.164 - (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN),
1.165 - no_sosN)))])
1.166 + combs_or_liftingN, false), sosN))),
1.167 + (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN,
1.168 + false), sosN))),
1.169 + (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN,
1.170 + false), no_sosN)))])
1.171 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.172 else I)}
1.173
1.174 @@ -443,10 +445,10 @@
1.175 prem_kind = Hypothesis,
1.176 best_slices =
1.177 (* FUDGE *)
1.178 - K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))),
1.179 - (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))),
1.180 - (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))),
1.181 - (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]}
1.182 + K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN, false), ""))),
1.183 + (0.25, (false, ((125, z3_tff0, "mono_simple", combsN, false), ""))),
1.184 + (0.125, (false, ((62, z3_tff0, "mono_simple", combsN, false), ""))),
1.185 + (0.125, (false, ((31, z3_tff0, "mono_simple", combsN, false), "")))]}
1.186
1.187 val z3_tptp = (z3_tptpN, z3_tptp_config)
1.188
1.189 @@ -464,7 +466,7 @@
1.190 best_slices =
1.191 K [(1.0, (false, ((200, format, type_enc,
1.192 if is_format_higher_order format then keep_lamsN
1.193 - else combsN), "")))]}
1.194 + else combsN, false), "")))]}
1.195
1.196 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
1.197 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
1.198 @@ -515,16 +517,13 @@
1.199 {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
1.200 required_execs = [],
1.201 arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
1.202 - "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
1.203 - ^ " -s " ^ the_system system_name system_versions,
1.204 + "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
1.205 + " -s " ^ the_system system_name system_versions,
1.206 proof_delims = union (op =) tstp_proof_delims proof_delims,
1.207 known_failures = known_failures @ known_perl_failures @ known_says_failures,
1.208 conj_sym_kind = conj_sym_kind,
1.209 prem_kind = prem_kind,
1.210 - best_slices = fn ctxt =>
1.211 - let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
1.212 - [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))]
1.213 - end}
1.214 + best_slices = fn ctxt => [(1.0, (false, (best_slice ctxt, "")))]}
1.215
1.216 fun remotify_config system_name system_versions best_slice
1.217 ({proof_delims, known_failures, conj_sym_kind, prem_kind, ...}
1.218 @@ -545,43 +544,44 @@
1.219
1.220 val remote_e =
1.221 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
1.222 - (K (750, FOF, "mono_tags??", combsN) (* FUDGE *))
1.223 + (K (750, FOF, "mono_tags??", combsN, false) (* FUDGE *))
1.224 val remote_leo2 =
1.225 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
1.226 - (K (100, leo2_thf0, "mono_simple_higher", liftingN) (* FUDGE *))
1.227 + (K (100, leo2_thf0, "mono_simple_higher", liftingN, false) (* FUDGE *))
1.228 val remote_satallax =
1.229 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
1.230 - (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
1.231 + (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN, false)
1.232 + (* FUDGE *))
1.233 val remote_vampire =
1.234 remotify_atp vampire "Vampire" ["1.8"]
1.235 - (K (250, FOF, "mono_guards??", combs_or_liftingN) (* FUDGE *))
1.236 + (K (250, FOF, "mono_guards??", combs_or_liftingN, false) (* FUDGE *))
1.237 val remote_z3_tptp =
1.238 remotify_atp z3_tptp "Z3" ["3.0"]
1.239 - (K (250, z3_tff0, "mono_simple", combsN) (* FUDGE *))
1.240 + (K (250, z3_tff0, "mono_simple", combsN, false) (* FUDGE *))
1.241 val remote_e_sine =
1.242 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
1.243 - Conjecture (K (500, FOF, "mono_guards??", combsN) (* FUDGE *))
1.244 + Conjecture (K (500, FOF, "mono_guards??", combsN, false) (* FUDGE *))
1.245 val remote_iprover =
1.246 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
1.247 - (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
1.248 + (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
1.249 val remote_iprover_eq =
1.250 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
1.251 - (K (150, FOF, "mono_guards??", liftingN) (* FUDGE *))
1.252 + (K (150, FOF, "mono_guards??", liftingN, false) (* FUDGE *))
1.253 val remote_snark =
1.254 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
1.255 [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
1.256 - (K (100, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
1.257 + (K (100, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
1.258 val remote_e_tofof =
1.259 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
1.260 Hypothesis
1.261 - (K (150, explicit_tff0, "mono_simple", liftingN) (* FUDGE *))
1.262 + (K (150, explicit_tff0, "mono_simple", liftingN, false) (* FUDGE *))
1.263 val remote_waldmeister =
1.264 remote_atp waldmeisterN "Waldmeister" ["710"]
1.265 [("#START OF PROOF", "Proved Goals:")]
1.266 [(OutOfResources, "Too many function symbols"),
1.267 (Crashed, "Unrecoverable Segmentation Fault")]
1.268 Hypothesis Hypothesis
1.269 - (K (50, CNF_UEQ, "mono_tags??", combsN) (* FUDGE *))
1.270 + (K (50, CNF_UEQ, "mono_tags??", combsN, false) (* FUDGE *))
1.271
1.272 (* Setup *)
1.273