--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 27 16:35:02 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 27 17:34:33 2012 +0200
@@ -644,12 +644,11 @@
fact_override
in
if !reconstructor = "sledgehammer_tac" then
- sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
- ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
- ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
- ORELSE' Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN
- ctxt thms
+ sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
+ ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
+ ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
+ ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
+ ORELSE' SMT_Solver.smt_tac ctxt thms
else if !reconstructor = "smt" then
SMT_Solver.smt_tac ctxt thms
else if full then
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jul 27 16:35:02 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Jul 27 17:34:33 2012 +0200
@@ -2659,7 +2659,7 @@
? append (map fst cs)))
(Datatype.get_all thy) []
-val app_op_and_predicator_threshold = 50
+val app_op_and_predicator_threshold = 45
fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
uncurried_aliases readable_names preproc hyp_ts concl_t
--- a/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 27 16:35:02 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 27 17:34:33 2012 +0200
@@ -420,7 +420,7 @@
(0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))),
(0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))),
(0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))),
- (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))],
+ (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), "")))],
best_max_mono_iters = default_max_mono_iters,
best_max_new_mono_instances = default_max_new_mono_instances}