1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 03 18:00:55 2012 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 03 18:00:55 2012 +0100
1.3 @@ -23,7 +23,8 @@
1.4 prem_kind : formula_kind,
1.5 best_slices :
1.6 Proof.context
1.7 - -> (real * (bool * (int * atp_format * string * string * string))) list}
1.8 + -> (real * (bool * ((int * atp_format * string * string) * string)))
1.9 + list}
1.10
1.11 val force_sos : bool Config.T
1.12 val e_smartN : string
1.13 @@ -88,10 +89,10 @@
1.14 prem_kind : formula_kind,
1.15 best_slices :
1.16 Proof.context
1.17 - -> (real * (bool * (int * atp_format * string * string * string))) list}
1.18 + -> (real * (bool * ((int * atp_format * string * string) * string))) list}
1.19
1.20 (* "best_slices" must be found empirically, taking a wholistic approach since
1.21 - the ATPs are run in parallel. The "real" components give the faction of the
1.22 + the ATPs are run in parallel. The "real" component gives the faction of the
1.23 time available given to the slice and should add up to 1.0. The "bool"
1.24 component indicates whether the slice's strategy is complete; the "int", the
1.25 preferred number of facts to pass; the first "string", the preferred type
1.26 @@ -150,7 +151,8 @@
1.27 type T = (atp_config * stamp) Symtab.table
1.28 val empty = Symtab.empty
1.29 val extend = I
1.30 - fun merge data : T = Symtab.merge (eq_snd op =) data
1.31 + fun merge data : T =
1.32 + Symtab.merge (eq_snd (op =)) data
1.33 handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
1.34 )
1.35
1.36 @@ -246,14 +248,12 @@
1.37 let val method = effective_e_weight_method ctxt in
1.38 (* FUDGE *)
1.39 if method = e_smartN then
1.40 - [(0.333, (true, (500, FOF, "mono_tags??", combsN,
1.41 - e_fun_weightN))),
1.42 - (0.334, (true, (50, FOF, "mono_guards??", combsN,
1.43 - e_fun_weightN))),
1.44 - (0.333, (true, (1000, FOF, "mono_tags??", combsN,
1.45 + [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))),
1.46 + (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))),
1.47 + (0.333, (true, ((1000, FOF, "mono_tags??", combsN),
1.48 e_sym_offset_weightN)))]
1.49 else
1.50 - [(1.0, (true, (500, FOF, "mono_tags??", combsN, method)))]
1.51 + [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))]
1.52 end}
1.53
1.54 val e = (eN, e_config)
1.55 @@ -278,9 +278,9 @@
1.56 prem_kind = Hypothesis,
1.57 best_slices = fn ctxt =>
1.58 (* FUDGE *)
1.59 - [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", liftingN,
1.60 + [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN),
1.61 sosN))),
1.62 - (0.333, (true, (50, leo2_thf0, "mono_simple_higher", liftingN,
1.63 + (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN),
1.64 no_sosN)))]
1.65 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.66 else I)}
1.67 @@ -305,7 +305,7 @@
1.68 prem_kind = Hypothesis,
1.69 best_slices =
1.70 (* FUDGE *)
1.71 - K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN,
1.72 + K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN),
1.73 "")))]}
1.74
1.75 val satallax = (satallaxN, satallax_config)
1.76 @@ -338,17 +338,21 @@
1.77 prem_kind = Conjecture,
1.78 best_slices = fn ctxt =>
1.79 (* FUDGE *)
1.80 - [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", liftingN,
1.81 + [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN),
1.82 sosN))),
1.83 - (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", liftingN,
1.84 + (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN),
1.85 sosN))),
1.86 - (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", liftingN,
1.87 + (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN),
1.88 no_sosN)))]
1.89 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.90 else I)}
1.91
1.92 val spass = (spassN, spass_config)
1.93
1.94 +val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN)
1.95 +val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN)
1.96 +val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN)
1.97 +
1.98 (* Experimental *)
1.99 val spass_new_config : atp_config =
1.100 {exec = ("ISABELLE_ATP", "scripts/spass_new"),
1.101 @@ -364,10 +368,9 @@
1.102 prem_kind = #prem_kind spass_config,
1.103 best_slices = fn _ =>
1.104 (* FUDGE *)
1.105 - [(0.334, (true, (300, DFG DFG_Sorted, "mono_simple", combsN,
1.106 - "" (* spass_incompleteN *)))),
1.107 - (0.333, (true, (50, DFG DFG_Sorted, "mono_simple", combsN, ""))),
1.108 - (0.333, (true, (150, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
1.109 + [(0.300, (true, (spass_new_macro_slice_1, ""))),
1.110 + (0.333, (true, (spass_new_macro_slice_2, ""))),
1.111 + (0.333, (true, (spass_new_macro_slice_3, "")))]}
1.112
1.113 val spass_new = (spass_newN, spass_new_config)
1.114
1.115 @@ -407,15 +410,17 @@
1.116 best_slices = fn ctxt =>
1.117 (* FUDGE *)
1.118 (if is_old_vampire_version () then
1.119 - [(0.333, (false, (150, FOF, "poly_guards??", combs_or_liftingN, sosN))),
1.120 - (0.333, (false, (500, FOF, "mono_tags??", combs_or_liftingN, sosN))),
1.121 - (0.334, (true, (50, FOF, "mono_guards??", combs_or_liftingN, no_sosN)))]
1.122 + [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN),
1.123 + sosN))),
1.124 + (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))),
1.125 + (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN),
1.126 + no_sosN)))]
1.127 else
1.128 - [(0.333, (false, (150, vampire_tff0, "poly_guards??", combs_or_liftingN,
1.129 + [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
1.130 + combs_or_liftingN), sosN))),
1.131 + (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN),
1.132 sosN))),
1.133 - (0.333, (false, (500, vampire_tff0, "mono_simple", combs_or_liftingN,
1.134 - sosN))),
1.135 - (0.334, (true, (50, vampire_tff0, "mono_simple", combs_or_liftingN,
1.136 + (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN),
1.137 no_sosN)))])
1.138 |> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
1.139 else I)}
1.140 @@ -438,10 +443,10 @@
1.141 prem_kind = Hypothesis,
1.142 best_slices =
1.143 (* FUDGE *)
1.144 - K [(0.5, (false, (250, z3_tff0, "mono_simple", combsN, ""))),
1.145 - (0.25, (false, (125, z3_tff0, "mono_simple", combsN, ""))),
1.146 - (0.125, (false, (62, z3_tff0, "mono_simple", combsN, ""))),
1.147 - (0.125, (false, (31, z3_tff0, "mono_simple", combsN, "")))]}
1.148 + K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))),
1.149 + (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))),
1.150 + (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))),
1.151 + (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]}
1.152
1.153 val z3_tptp = (z3_tptpN, z3_tptp_config)
1.154
1.155 @@ -457,9 +462,9 @@
1.156 conj_sym_kind = Hypothesis,
1.157 prem_kind = Hypothesis,
1.158 best_slices =
1.159 - K [(1.0, (false, (200, format, type_enc,
1.160 - if is_format_higher_order format then keep_lamsN
1.161 - else combsN, "")))]}
1.162 + K [(1.0, (false, ((200, format, type_enc,
1.163 + if is_format_higher_order format then keep_lamsN
1.164 + else combsN), "")))]}
1.165
1.166 val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
1.167 val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
1.168 @@ -518,7 +523,7 @@
1.169 prem_kind = prem_kind,
1.170 best_slices = fn ctxt =>
1.171 let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
1.172 - [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))]
1.173 + [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))]
1.174 end}
1.175
1.176 fun remotify_config system_name system_versions best_slice