--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 03 18:00:55 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Feb 03 18:00:55 2012 +0100
@@ -23,7 +23,8 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * atp_format * string * string * string))) list}
+ -> (real * (bool * ((int * atp_format * string * string) * string)))
+ list}
val force_sos : bool Config.T
val e_smartN : string
@@ -88,10 +89,10 @@
prem_kind : formula_kind,
best_slices :
Proof.context
- -> (real * (bool * (int * atp_format * string * string * string))) list}
+ -> (real * (bool * ((int * atp_format * string * string) * string))) list}
(* "best_slices" must be found empirically, taking a wholistic approach since
- the ATPs are run in parallel. The "real" components give the faction of the
+ the ATPs are run in parallel. The "real" component gives the faction of the
time available given to the slice and should add up to 1.0. The "bool"
component indicates whether the slice's strategy is complete; the "int", the
preferred number of facts to pass; the first "string", the preferred type
@@ -150,7 +151,8 @@
type T = (atp_config * stamp) Symtab.table
val empty = Symtab.empty
val extend = I
- fun merge data : T = Symtab.merge (eq_snd op =) data
+ fun merge data : T =
+ Symtab.merge (eq_snd (op =)) data
handle Symtab.DUP name => error ("Duplicate ATP: " ^ quote name ^ ".")
)
@@ -246,14 +248,12 @@
let val method = effective_e_weight_method ctxt in
(* FUDGE *)
if method = e_smartN then
- [(0.333, (true, (500, FOF, "mono_tags??", combsN,
- e_fun_weightN))),
- (0.334, (true, (50, FOF, "mono_guards??", combsN,
- e_fun_weightN))),
- (0.333, (true, (1000, FOF, "mono_tags??", combsN,
+ [(0.333, (true, ((500, FOF, "mono_tags??", combsN), e_fun_weightN))),
+ (0.334, (true, ((50, FOF, "mono_guards??", combsN), e_fun_weightN))),
+ (0.333, (true, ((1000, FOF, "mono_tags??", combsN),
e_sym_offset_weightN)))]
else
- [(1.0, (true, (500, FOF, "mono_tags??", combsN, method)))]
+ [(1.0, (true, ((500, FOF, "mono_tags??", combsN), method)))]
end}
val e = (eN, e_config)
@@ -278,9 +278,9 @@
prem_kind = Hypothesis,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.667, (false, (150, leo2_thf0, "mono_simple_higher", liftingN,
+ [(0.667, (false, ((150, leo2_thf0, "mono_simple_higher", liftingN),
sosN))),
- (0.333, (true, (50, leo2_thf0, "mono_simple_higher", liftingN,
+ (0.333, (true, ((50, leo2_thf0, "mono_simple_higher", liftingN),
no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -305,7 +305,7 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(1.0, (true, (100, satallax_thf0, "mono_simple_higher", keep_lamsN,
+ K [(1.0, (true, ((100, satallax_thf0, "mono_simple_higher", keep_lamsN),
"")))]}
val satallax = (satallaxN, satallax_config)
@@ -338,17 +338,21 @@
prem_kind = Conjecture,
best_slices = fn ctxt =>
(* FUDGE *)
- [(0.333, (false, (150, DFG DFG_Unsorted, "mono_tags??", liftingN,
+ [(0.333, (false, ((150, DFG DFG_Unsorted, "mono_tags??", liftingN),
sosN))),
- (0.333, (false, (300, DFG DFG_Unsorted, "poly_tags??", liftingN,
+ (0.333, (false, ((300, DFG DFG_Unsorted, "poly_tags??", liftingN),
sosN))),
- (0.334, (false, (50, DFG DFG_Unsorted, "mono_tags??", liftingN,
+ (0.334, (false, ((50, DFG DFG_Unsorted, "mono_tags??", liftingN),
no_sosN)))]
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
val spass = (spassN, spass_config)
+val spass_new_macro_slice_1 = (300, DFG DFG_Sorted, "mono_simple", combsN)
+val spass_new_macro_slice_2 = (50, DFG DFG_Sorted, "mono_simple", combsN)
+val spass_new_macro_slice_3 = (150, DFG DFG_Sorted, "mono_simple", liftingN)
+
(* Experimental *)
val spass_new_config : atp_config =
{exec = ("ISABELLE_ATP", "scripts/spass_new"),
@@ -364,10 +368,9 @@
prem_kind = #prem_kind spass_config,
best_slices = fn _ =>
(* FUDGE *)
- [(0.334, (true, (300, DFG DFG_Sorted, "mono_simple", combsN,
- "" (* spass_incompleteN *)))),
- (0.333, (true, (50, DFG DFG_Sorted, "mono_simple", combsN, ""))),
- (0.333, (true, (150, DFG DFG_Sorted, "mono_simple", liftingN, "")))]}
+ [(0.300, (true, (spass_new_macro_slice_1, ""))),
+ (0.333, (true, (spass_new_macro_slice_2, ""))),
+ (0.333, (true, (spass_new_macro_slice_3, "")))]}
val spass_new = (spass_newN, spass_new_config)
@@ -407,15 +410,17 @@
best_slices = fn ctxt =>
(* FUDGE *)
(if is_old_vampire_version () then
- [(0.333, (false, (150, FOF, "poly_guards??", combs_or_liftingN, sosN))),
- (0.333, (false, (500, FOF, "mono_tags??", combs_or_liftingN, sosN))),
- (0.334, (true, (50, FOF, "mono_guards??", combs_or_liftingN, no_sosN)))]
+ [(0.333, (false, ((150, FOF, "poly_guards??", combs_or_liftingN),
+ sosN))),
+ (0.333, (false, ((500, FOF, "mono_tags??", combs_or_liftingN), sosN))),
+ (0.334, (true, ((50, FOF, "mono_guards??", combs_or_liftingN),
+ no_sosN)))]
else
- [(0.333, (false, (150, vampire_tff0, "poly_guards??", combs_or_liftingN,
+ [(0.333, (false, ((150, vampire_tff0, "poly_guards??",
+ combs_or_liftingN), sosN))),
+ (0.333, (false, ((500, vampire_tff0, "mono_simple", combs_or_liftingN),
sosN))),
- (0.333, (false, (500, vampire_tff0, "mono_simple", combs_or_liftingN,
- sosN))),
- (0.334, (true, (50, vampire_tff0, "mono_simple", combs_or_liftingN,
+ (0.334, (true, ((50, vampire_tff0, "mono_simple", combs_or_liftingN),
no_sosN)))])
|> (if Config.get ctxt force_sos then hd #> apfst (K 1.0) #> single
else I)}
@@ -438,10 +443,10 @@
prem_kind = Hypothesis,
best_slices =
(* FUDGE *)
- K [(0.5, (false, (250, z3_tff0, "mono_simple", combsN, ""))),
- (0.25, (false, (125, z3_tff0, "mono_simple", combsN, ""))),
- (0.125, (false, (62, z3_tff0, "mono_simple", combsN, ""))),
- (0.125, (false, (31, z3_tff0, "mono_simple", combsN, "")))]}
+ K [(0.5, (false, ((250, z3_tff0, "mono_simple", combsN), ""))),
+ (0.25, (false, ((125, z3_tff0, "mono_simple", combsN), ""))),
+ (0.125, (false, ((62, z3_tff0, "mono_simple", combsN), ""))),
+ (0.125, (false, ((31, z3_tff0, "mono_simple", combsN), "")))]}
val z3_tptp = (z3_tptpN, z3_tptp_config)
@@ -457,9 +462,9 @@
conj_sym_kind = Hypothesis,
prem_kind = Hypothesis,
best_slices =
- K [(1.0, (false, (200, format, type_enc,
- if is_format_higher_order format then keep_lamsN
- else combsN, "")))]}
+ K [(1.0, (false, ((200, format, type_enc,
+ if is_format_higher_order format then keep_lamsN
+ else combsN), "")))]}
val dummy_tff1_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
val dummy_tff1_config = dummy_config dummy_tff1_format "poly_simple"
@@ -518,7 +523,7 @@
prem_kind = prem_kind,
best_slices = fn ctxt =>
let val (max_relevant, format, type_enc, lam_trans) = best_slice ctxt in
- [(1.0, (false, (max_relevant, format, type_enc, lam_trans, "")))]
+ [(1.0, (false, ((max_relevant, format, type_enc, lam_trans), "")))]
end}
fun remotify_config system_name system_versions best_slice
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Feb 03 18:00:55 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Feb 03 18:00:55 2012 +0100
@@ -147,7 +147,7 @@
let val thy = Proof_Context.theory_of ctxt in
case try (get_atp thy) name of
SOME {best_slices, ...} =>
- exists (fn (_, (_, (_, format, _, _, _))) => is_format format)
+ exists (fn (_, (_, ((_, format, _, _), _))) => is_format format)
(best_slices ctxt)
| NONE => false
end
@@ -174,7 +174,7 @@
if is_reconstructor name then
reconstructor_default_max_relevant
else if is_atp thy name then
- fold (Integer.max o #1 o snd o snd o snd)
+ fold (Integer.max o #1 o fst o snd o snd o snd)
(get_slices slice (#best_slices (get_atp thy name) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
@@ -651,10 +651,10 @@
|> curry ListPair.zip (map fst facts)
|> maps (fn (name, rths) => map (pair name o snd) rths)
end
- fun run_slice (slice, (time_frac, (complete,
- (best_max_relevant, format, best_type_enc,
- best_lam_trans, extra))))
- time_left =
+ fun run_slice time_left (cache_key, cache_value)
+ (slice, (time_frac, (complete,
+ (key as (best_max_relevant, format, best_type_enc,
+ best_lam_trans), extra)))) =
let
val num_facts =
length facts |> is_none max_relevant
@@ -663,14 +663,6 @@
val type_enc =
type_enc |> choose_type_enc soundness best_type_enc format
val fairly_sound = is_type_enc_fairly_sound type_enc
- val facts =
- facts |> map untranslated_fact
- |> not fairly_sound
- ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
- |> take num_facts
- |> polymorphism_of_type_enc type_enc <> Polymorphic
- ? monomorphize_facts
- |> map (apsnd prop_of)
val real_ms = Real.fromInt o Time.toMilliseconds
val slice_timeout =
((real_ms time_left
@@ -695,20 +687,32 @@
case lam_trans of
SOME s => s
| NONE => best_lam_trans
- val (atp_problem, pool, fact_names, _, sym_tab) =
- prepare_atp_problem ctxt format conj_sym_kind prem_kind
- type_enc false lam_trans readable_names true hyp_ts
- concl_t facts
+ val value as (atp_problem, _, fact_names, _, _) =
+ if cache_key = SOME key then
+ cache_value
+ else
+ facts
+ |> map untranslated_fact
+ |> not fairly_sound
+ ? filter_out (is_dangerous_prop ctxt o prop_of o snd)
+ |> take num_facts
+ |> polymorphism_of_type_enc type_enc <> Polymorphic
+ ? monomorphize_facts
+ |> map (apsnd prop_of)
+ |> prepare_atp_problem ctxt format conj_sym_kind prem_kind
+ type_enc false lam_trans readable_names true hyp_ts
+ concl_t
fun weights () = atp_problem_weights atp_problem
val full_proof = debug orelse isar_proof
- val core =
+ val command =
File.shell_path command ^ " " ^
arguments ctxt full_proof extra slice_timeout weights ^ " " ^
File.shell_path prob_file
- val command = "TIMEFORMAT='%3R'; { time " ^ core ^ " ; } 2>&1"
- val _ = atp_problem |> lines_for_atp_problem format
- |> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
+ |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
+ val _ =
+ atp_problem |> lines_for_atp_problem format
+ |> cons ("% " ^ command ^ "\n")
+ |> File.write_list prob_file
val ((output, run_time), (atp_proof, outcome)) =
TimeLimit.timeLimit generous_slice_timeout
Isabelle_System.bash_output command
@@ -745,27 +749,24 @@
end
| NONE => NONE)
| _ => outcome
- in
- ((pool, fact_names, sym_tab),
- (output, run_time, atp_proof, outcome))
- end
+ in ((SOME key, value), (output, run_time, atp_proof, outcome)) end
val timer = Timer.startRealTimer ()
fun maybe_run_slice slice
- (result as (_, (_, run_time0, _, SOME _))) =
+ (result as (cache, (_, run_time0, _, SOME _))) =
let
val time_left = Time.- (timeout, Timer.checkRealTimer timer)
in
if Time.<= (time_left, Time.zeroTime) then
result
else
- run_slice slice time_left
- |> (fn (stuff, (output, run_time, atp_proof, outcome)) =>
- (stuff, (output, Time.+ (run_time0, run_time),
+ run_slice time_left cache slice
+ |> (fn (cache, (output, run_time, atp_proof, outcome)) =>
+ (cache, (output, Time.+ (run_time0, run_time),
atp_proof, outcome)))
end
| maybe_run_slice _ result = result
in
- ((Symtab.empty, Vector.fromList [], Symtab.empty),
+ ((NONE, ([], Symtab.empty, Vector.fromList [], [], Symtab.empty)),
("", Time.zeroTime, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
@@ -781,7 +782,8 @@
()
else
File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
- val ((pool, fact_names, sym_tab), (output, run_time, atp_proof, outcome)) =
+ val ((_, (_, pool, fact_names, _, sym_tab)),
+ (output, run_time, atp_proof, outcome)) =
with_path cleanup export run_on problem_path_name
val important_message =
if mode = Normal andalso