1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Nov 16 16:35:19 2011 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Nov 16 17:06:14 2011 +0100
1.3 @@ -23,7 +23,7 @@
1.4 prem_kind : formula_kind,
1.5 best_slices :
1.6 Proof.context
1.7 - -> (real * (bool * (int * atp_format * string * string))) list}
1.8 + -> (real * (bool * (int * atp_format * string * string * string))) list}
1.9
1.10 val force_sos : bool Config.T
1.11 val e_smartN : string
1.12 @@ -56,7 +56,8 @@
1.13 val remote_atp :
1.14 string -> string -> string list -> (string * string) list
1.15 -> (failure * string) list -> formula_kind -> formula_kind
1.16 - -> (Proof.context -> int * atp_format * string) -> string * atp_config
1.17 + -> (Proof.context -> int * atp_format * string * string)
1.18 + -> 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 @@ -70,6 +71,7 @@
1.23
1.24 open ATP_Problem
1.25 open ATP_Proof
1.26 +open ATP_Translate
1.27
1.28 (* ATP configuration *)
1.29
1.30 @@ -85,15 +87,16 @@
1.31 prem_kind : formula_kind,
1.32 best_slices :
1.33 Proof.context
1.34 - -> (real * (bool * (int * atp_format * string * string))) list}
1.35 + -> (real * (bool * (int * atp_format * string * string * string))) list}
1.36
1.37 (* "best_slices" must be found empirically, taking a wholistic approach since
1.38 the ATPs are run in parallel. The "real" components give the faction of the
1.39 time available given to the slice and should add up to 1.0. The "bool"
1.40 component indicates whether the slice's strategy is complete; the "int", the
1.41 preferred number of facts to pass; the first "string", the preferred type
1.42 - system (which should be sound or quasi-sound); the second "string", extra
1.43 - information to the prover (e.g., SOS or no SOS).
1.44 + system (which should be sound or quasi-sound); the second "string", the
1.45 + preferred lambda translation scheme; the third "string", extra information to
1.46 + the prover (e.g., SOS or no SOS).
1.47
1.48 The last slice should be the most "normal" one, because it will get all the
1.49 time available if the other slices fail early and also because it is used if
1.50 @@ -242,11 +245,14 @@
1.51 let val method = effective_e_weight_method ctxt in
1.52 (* FUDGE *)
1.53 if method = e_smartN then
1.54 - [(0.333, (true, (500, FOF, "mono_tags??", e_fun_weightN))),
1.55 - (0.334, (true, (50, FOF, "mono_guards??", e_fun_weightN))),
1.56 - (0.333, (true, (1000, FOF, "mono_tags??", e_sym_offset_weightN)))]
1.57 + [(0.333, (true, (500, FOF, "mono_tags??", combinatorsN,
1.58 + e_fun_weightN))),
1.59 + (0.334, (true, (50, FOF, "mono_guards??", combinatorsN,
1.60 + e_fun_weightN))),
1.61 + (0.333, (true, (1000, FOF, "mono_tags??", combinatorsN,
1.62 + e_sym_offset_weightN)))]
1.63 else
1.64 - [(1.0, (true, (500, FOF, "mono_tags??", method)))]
1.65 + [(1.0, (true, (500, FOF, "mono_tags??", combinatorsN, method)))]
1.66 end}
1.67
1.68 val e = (eN, e_config)
1.69 @@ -271,8 +277,10 @@
1.70 prem_kind = Hypothesis,
1.71 best_slices = fn ctxt =>
1.72 (* FUDGE *)
1.73 - [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", sosN))),
1.74 - (0.333, (true, (50, leo2_thf0, "mono_simple_higher", no_sosN)))]
1.75 + [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", lam_liftingN,
1.76 + sosN))),
1.77 + (0.333, (true, (50, leo2_thf0, "mono_simple_higher", lam_liftingN,
1.78 + no_sosN)))]
1.79 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.80 else I)}
1.81
1.82 @@ -296,7 +304,8 @@
1.83 prem_kind = Hypothesis,
1.84 best_slices =
1.85 (* FUDGE *)
1.86 - K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", "")))]}
1.87 + K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN,
1.88 + "")))]}
1.89
1.90 val satallax = (satallaxN, satallax_config)
1.91
1.92 @@ -326,9 +335,12 @@
1.93 prem_kind = Conjecture,
1.94 best_slices = fn ctxt =>
1.95 (* FUDGE *)
1.96 - [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", sosN))),
1.97 - (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", sosN))),
1.98 - (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", no_sosN)))]
1.99 + [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
1.100 + sosN))),
1.101 + (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", lam_liftingN,
1.102 + sosN))),
1.103 + (0.334, (true, (50, DFG DFG_Unsorted, "mono_tags??", lam_liftingN,
1.104 + no_sosN)))]
1.105 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.106 else I)}
1.107
1.108 @@ -345,9 +357,12 @@
1.109 prem_kind = #prem_kind spass_config,
1.110 best_slices = fn ctxt =>
1.111 (* FUDGE *)
1.112 - [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", sosN))) (*,
1.113 - (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", sosN))),
1.114 - (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", no_sosN)))*)]
1.115 + [(0.333, (false, (150, DFG DFG_Sorted, "mono_simple", lam_liftingN,
1.116 + sosN))) (*,
1.117 + (0.333, (false, (300, DFG DFG_Sorted, "poly_tags??", lam_liftingN,
1.118 + sosN))),
1.119 + (0.334, (true, (50, DFG DFG_Sorted, "mono_simple", lam_liftingN,
1.120 + no_sosN)))*)]
1.121 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.122 else I)}
1.123
1.124 @@ -389,13 +404,16 @@
1.125 best_slices = fn ctxt =>
1.126 (* FUDGE *)
1.127 (if is_old_vampire_version () then
1.128 - [(0.333, (false, (150, FOF, "poly_guards??", sosN))),
1.129 - (0.333, (false, (500, FOF, "mono_tags??", sosN))),
1.130 - (0.334, (true, (50, FOF, "mono_guards??", no_sosN)))]
1.131 + [(0.333, (false, (150, FOF, "poly_guards??", hybrid_lamsN, sosN))),
1.132 + (0.333, (false, (500, FOF, "mono_tags??", hybrid_lamsN, sosN))),
1.133 + (0.334, (true, (50, FOF, "mono_guards??", hybrid_lamsN, no_sosN)))]
1.134 else
1.135 - [(0.333, (false, (150, vampire_tff0, "poly_guards??", sosN))),
1.136 - (0.333, (false, (500, vampire_tff0, "mono_simple", sosN))),
1.137 - (0.334, (true, (50, vampire_tff0, "mono_simple", no_sosN)))])
1.138 + [(0.333, (false, (150, vampire_tff0, "poly_guards??", hybrid_lamsN,
1.139 + sosN))),
1.140 + (0.333, (false, (500, vampire_tff0, "mono_simple", hybrid_lamsN,
1.141 + sosN))),
1.142 + (0.334, (true, (50, vampire_tff0, "mono_simple", hybrid_lamsN,
1.143 + no_sosN)))])
1.144 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.145 else I)}
1.146
1.147 @@ -417,10 +435,10 @@
1.148 prem_kind = Hypothesis,
1.149 best_slices =
1.150 (* FUDGE *)
1.151 - K [(0.5, (false, (250, z3_tff0, "mono_simple", ""))),
1.152 - (0.25, (false, (125, z3_tff0, "mono_simple", ""))),
1.153 - (0.125, (false, (62, z3_tff0, "mono_simple", ""))),
1.154 - (0.125, (false, (31, z3_tff0, "mono_simple", "")))]}
1.155 + K [(0.5, (false, (250, z3_tff0, "mono_simple", combinatorsN, ""))),
1.156 + (0.25, (false, (125, z3_tff0, "mono_simple", combinatorsN, ""))),
1.157 + (0.125, (false, (62, z3_tff0, "mono_simple", combinatorsN, ""))),
1.158 + (0.125, (false, (31, z3_tff0, "mono_simple", combinatorsN, "")))]}
1.159
1.160 val z3_tptp = (z3_tptpN, z3_tptp_config)
1.161
1.162 @@ -435,7 +453,10 @@
1.163 known_failures = known_szs_status_failures,
1.164 conj_sym_kind = Hypothesis,
1.165 prem_kind = Hypothesis,
1.166 - best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
1.167 + best_slices =
1.168 + K [(1.0, (false, (200, format, type_enc,
1.169 + if is_format_higher_order format then keep_lamsN
1.170 + else combinatorsN, "")))]}
1.171
1.172 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
1.173 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
1.174 @@ -493,8 +514,8 @@
1.175 conj_sym_kind = conj_sym_kind,
1.176 prem_kind = prem_kind,
1.177 best_slices = fn ctxt =>
1.178 - let val (max_relevant, format, type_enc) = best_slice ctxt in
1.179 - [(1.0, (false, (max_relevant, format, type_enc, "")))]
1.180 + let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
1.181 + [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))]
1.182 end}
1.183
1.184 fun remotify_config system_name system_versions best_slice
1.185 @@ -516,42 +537,43 @@
1.186
1.187 val remote_e =
1.188 remotify_atp e "EP" ["1.0", "1.1", "1.2"]
1.189 - (K (750, FOF, "mono_tags??") (* FUDGE *))
1.190 + (K (750, FOF, "mono_tags??", combinatorsN) (* FUDGE *))
1.191 val remote_leo2 =
1.192 remotify_atp leo2 "LEO-II" ["1.2.8", "1.2.6"]
1.193 - (K (100, leo2_thf0, "mono_simple_higher") (* FUDGE *))
1.194 + (K (100, leo2_thf0, "mono_simple_higher", lam_liftingN) (* FUDGE *))
1.195 val remote_satallax =
1.196 remotify_atp satallax "Satallax" ["2.1", "2.0", "2"]
1.197 - (K (100, satallax_thf0, "mono_simple_higher") (* FUDGE *))
1.198 + (K (100, satallax_thf0, "mono_simple_higher", keep_lamsN) (* FUDGE *))
1.199 val remote_vampire =
1.200 remotify_atp vampire "Vampire" ["1.8"]
1.201 - (K (250, FOF, "mono_guards??") (* FUDGE *))
1.202 + (K (250, FOF, "mono_guards??", hybrid_lamsN) (* FUDGE *))
1.203 val remote_z3_tptp =
1.204 remotify_atp z3_tptp "Z3" ["3.0"]
1.205 - (K (250, z3_tff0, "mono_simple") (* FUDGE *))
1.206 + (K (250, z3_tff0, "mono_simple", combinatorsN) (* FUDGE *))
1.207 val remote_e_sine =
1.208 remote_atp e_sineN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
1.209 - Conjecture (K (500, FOF, "mono_guards??") (* FUDGE *))
1.210 + Conjecture (K (500, FOF, "mono_guards??", combinatorsN) (* FUDGE *))
1.211 val remote_iprover =
1.212 remote_atp iproverN "iProver" [] [] [] Axiom Conjecture
1.213 - (K (150, FOF, "mono_guards??") (* FUDGE *))
1.214 + (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
1.215 val remote_iprover_eq =
1.216 remote_atp iprover_eqN "iProver-Eq" [] [] [] Axiom Conjecture
1.217 - (K (150, FOF, "mono_guards??") (* FUDGE *))
1.218 + (K (150, FOF, "mono_guards??", lam_liftingN) (* FUDGE *))
1.219 val remote_snark =
1.220 remote_atp snarkN "SNARK" ["20080805r029", "20080805r024"]
1.221 - [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
1.222 - (K (100, explicit_tff0, "mono_simple") (* FUDGE *))
1.223 + [("refutation.", "end_refutation.")] [] Hypothesis Hypothesis
1.224 + (K (100, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
1.225 val remote_e_tofof =
1.226 remote_atp e_tofofN "ToFoF" ["0.1"] [] (#known_failures e_config) Axiom
1.227 - Hypothesis (K (150, explicit_tff0, "mono_simple") (* FUDGE *))
1.228 + Hypothesis
1.229 + (K (150, explicit_tff0, "mono_simple", lam_liftingN) (* FUDGE *))
1.230 val remote_waldmeister =
1.231 remote_atp waldmeisterN "Waldmeister" ["710"]
1.232 - [("#START OF PROOF", "Proved Goals:")]
1.233 - [(OutOfResources, "Too many function symbols"),
1.234 - (Crashed, "Unrecoverable Segmentation Fault")]
1.235 - Hypothesis Hypothesis
1.236 - (K (50, CNF_UEQ, "mono_tags??") (* FUDGE *))
1.237 + [("#START OF PROOF", "Proved Goals:")]
1.238 + [(OutOfResources, "Too many function symbols"),
1.239 + (Crashed, "Unrecoverable Segmentation Fault")]
1.240 + Hypothesis Hypothesis
1.241 + (K (50, CNF_UEQ, "mono_tags??", combinatorsN) (* FUDGE *))
1.242
1.243 (* Setup *)
1.244