--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 14:48:20 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 14:48:20 2014 +0100
@@ -154,14 +154,14 @@
val birth = Timer.checkRealTimer timer
val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
- val {outcome, used_fact_infos, z3_proof} =
- SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout
+ val filter_result as {outcome, ...} =
+ SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout
handle exn =>
if Exn.is_interrupt exn orelse debug then
reraise exn
else
{outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
- used_fact_infos = [], z3_proof = []}
+ conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []}
val death = Timer.checkRealTimer timer
val outcome0 = if is_none outcome0 then SOME outcome else outcome0
@@ -206,9 +206,8 @@
do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
end
else
- {outcome = if is_none outcome then NONE else the outcome0,
- used_fact_infos = used_fact_infos, used_from = map (apsnd snd) weighted_facts,
- z3_proof = z3_proof, run_time = time_so_far}
+ {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
+ used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
end
in
do_slice timeout 1 NONE Time.zeroTime
@@ -227,9 +226,9 @@
end
val weighted_factss = map (apsnd weight_facts) factss
- val {outcome, used_fact_infos, used_from, z3_proof, run_time} =
- smt2_filter_loop name params state goal subgoal weighted_factss
- val used_named_facts = map snd used_fact_infos
+ val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...},
+ used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss
+ val used_named_facts = map snd fact_ids
val used_facts = map fst used_named_facts
val outcome = Option.map failure_of_smt2_failure outcome
@@ -241,8 +240,10 @@
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
- val fact_ids = map (fn (id, ((name, _), _)) => (id, name)) used_fact_infos
- val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_proof fact_ids
+ val fact_ids =
+ map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
+ map (fn (id, ((name, _), _)) => (id, name)) fact_ids
+ val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof
val isar_params =
K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
minimize <> SOME false, atp_proof, goal)