--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 22 14:51:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sun May 22 14:51:42 2011 +0200
@@ -189,7 +189,9 @@
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
val _ = print "Sledgehammering..."
- val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
+ val (smts, (ueq_atps, full_atps)) =
+ provers |> List.partition (is_smt_prover ctxt)
+ ||> List.partition (is_unit_equational_atp ctxt)
fun launch_provers state get_facts translate maybe_smt_filter provers =
let
val facts = get_facts ()
@@ -212,7 +214,7 @@
|> (if blocking then smart_par_list_map else map) (launch problem)
|> exists fst |> rpair state
end
- fun get_facts label relevance_fudge provers =
+ fun get_facts label is_good_prop relevance_fudge provers =
let
val max_max_relevant =
case max_relevant of
@@ -225,7 +227,7 @@
val is_built_in_const =
is_built_in_const_for_prover ctxt (hd provers)
in
- relevant_facts ctxt relevance_thresholds max_max_relevant
+ relevant_facts ctxt relevance_thresholds max_max_relevant is_good_prop
is_built_in_const relevance_fudge relevance_override
chained_ths hyp_ts concl_t
|> tap (fn facts =>
@@ -241,18 +243,19 @@
else
())
end
- fun launch_atps accum =
- if null atps then
+ fun launch_atps label is_good_prop atps accum =
+ if null atps orelse not (is_good_prop concl_t) then
accum
else
- launch_provers state (get_facts "ATP" atp_relevance_fudge o K atps)
- (K (Untranslated_Fact o fst)) (K (K NONE)) atps
+ launch_provers state
+ (get_facts label is_good_prop atp_relevance_fudge o K atps)
+ (K (Untranslated_Fact o fst)) (K (K NONE)) atps
fun launch_smts accum =
if null smts then
accum
else
let
- val facts = get_facts "SMT solver" smt_relevance_fudge smts
+ val facts = get_facts "SMT solver" (K true) smt_relevance_fudge smts
val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
fun smt_filter facts =
(if debug then curry (op o) SOME
@@ -264,14 +267,19 @@
|> map (launch_provers state (K facts) weight smt_filter o snd)
|> exists fst |> rpair state
end
+ val launch_full_atps = launch_atps "ATP" (K true) full_atps
+ val launch_ueq_atps =
+ launch_atps "Unit equational provers" is_unit_equality ueq_atps
fun launch_atps_and_smt_solvers () =
- [launch_atps, launch_smts]
+ [launch_full_atps, launch_ueq_atps, launch_smts]
|> smart_par_list_map (fn f => f (false, state) |> K ())
handle ERROR msg => (print ("Error: " ^ msg); error msg)
in
(false, state)
- |> (if blocking then launch_atps #> not auto ? launch_smts
- else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
+ |> (if blocking then
+ launch_full_atps #> not auto ? (launch_ueq_atps #> launch_smts)
+ else
+ (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
handle TimeLimit.TimeOut =>
(print "Sledgehammer ran out of time."; (false, state))
end