src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 56104 fd6e132ee4fb
parent 56099 bc036c1cf111
child 56128 c106ac2ff76d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 14:48:20 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 13 14:48:20 2014 +0100
     1.3 @@ -154,14 +154,14 @@
     1.4          val birth = Timer.checkRealTimer timer
     1.5          val _ = if debug then Output.urgent_message "Invoking SMT solver..." else ()
     1.6  
     1.7 -        val {outcome, used_fact_infos, z3_proof} =
     1.8 -          SMT2_Solver.smt2_filter ctxt [] goal weighted_facts i slice_timeout
     1.9 +        val filter_result as {outcome, ...} =
    1.10 +          SMT2_Solver.smt2_filter ctxt goal weighted_facts i slice_timeout
    1.11            handle exn =>
    1.12              if Exn.is_interrupt exn orelse debug then
    1.13                reraise exn
    1.14              else
    1.15                {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
    1.16 -               used_fact_infos = [], z3_proof = []}
    1.17 +               conjecture_id = ~1, helper_ids = [], fact_ids = [], z3_proof = []}
    1.18  
    1.19          val death = Timer.checkRealTimer timer
    1.20          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    1.21 @@ -206,9 +206,8 @@
    1.22              do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss
    1.23            end
    1.24          else
    1.25 -          {outcome = if is_none outcome then NONE else the outcome0,
    1.26 -           used_fact_infos = used_fact_infos, used_from = map (apsnd snd) weighted_facts,
    1.27 -           z3_proof = z3_proof, run_time = time_so_far}
    1.28 +          {outcome = if is_none outcome then NONE else the outcome0, filter_result = filter_result,
    1.29 +           used_from = map (apsnd snd) weighted_facts, run_time = time_so_far}
    1.30        end
    1.31    in
    1.32      do_slice timeout 1 NONE Time.zeroTime
    1.33 @@ -227,9 +226,9 @@
    1.34        end
    1.35  
    1.36      val weighted_factss = map (apsnd weight_facts) factss
    1.37 -    val {outcome, used_fact_infos, used_from, z3_proof, run_time} =
    1.38 -      smt2_filter_loop name params state goal subgoal weighted_factss
    1.39 -    val used_named_facts = map snd used_fact_infos
    1.40 +    val {outcome, filter_result = {conjecture_id, helper_ids, fact_ids, z3_proof, ...},
    1.41 +         used_from, run_time} = smt2_filter_loop name params state goal subgoal weighted_factss
    1.42 +    val used_named_facts = map snd fact_ids
    1.43      val used_facts = map fst used_named_facts
    1.44      val outcome = Option.map failure_of_smt2_failure outcome
    1.45  
    1.46 @@ -241,8 +240,10 @@
    1.47               SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
    1.48           fn preplay =>
    1.49              let
    1.50 -              val fact_ids = map (fn (id, ((name, _), _)) => (id, name)) used_fact_infos
    1.51 -              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_proof fact_ids
    1.52 +              val fact_ids =
    1.53 +                map (fn (id, th) => (id, short_thm_name ctxt th)) helper_ids @
    1.54 +                map (fn (id, ((name, _), _)) => (id, name)) fact_ids
    1.55 +              val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy conjecture_id fact_ids z3_proof
    1.56                val isar_params =
    1.57                  K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar,
    1.58                     minimize <> SOME false, atp_proof, goal)