src/HOL/Tools/SMT2/smt2_solver.ML
changeset 56981 3ef45ce002b5
parent 56132 64eeda68e693
child 57156 3546a67226ea
     1.1 --- a/src/HOL/Tools/SMT2/smt2_solver.ML	Fri May 16 17:11:56 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    (*filter*)
     1.5    val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time ->
     1.6      {outcome: SMT2_Failure.failure option, rewrite_rules: thm list, conjecture_id: int,
     1.7 -     helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list,
     1.8 +     prem_ids: int list, helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list,
     1.9       z3_proof: Z3_New_Proof.z3_step list}
    1.10  
    1.11    (*tactic*)
    1.12 @@ -260,17 +260,20 @@
    1.13      val iwthms = map_index I wthms
    1.14  
    1.15      val conjecture_i = 0
    1.16 -    val facts_i = 1 + length wprems
    1.17 +    val prems_i = 1
    1.18 +    val facts_i = prems_i + length wprems
    1.19    in
    1.20      wthms
    1.21      |> apply_solver ctxt
    1.22      |> (fn (((iidths0, z3_proof), _), {rewrite_rules, ...}) =>
    1.23 -      let val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
    1.24 +      let
    1.25 +        val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms
    1.26 +        fun id_of_index i = the_default no_id (Option.map fst (AList.lookup (op =) iidths i))
    1.27        in
    1.28          {outcome = NONE,
    1.29           rewrite_rules = rewrite_rules,
    1.30 -         conjecture_id =
    1.31 -           the_default no_id (Option.map fst (AList.lookup (op =) iidths conjecture_i)),
    1.32 +         conjecture_id = id_of_index conjecture_i,
    1.33 +         prem_ids = map id_of_index (prems_i upto facts_i - 1),
    1.34           helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths,
    1.35           fact_ids = map_filter (fn (i, (id, _)) =>
    1.36             try (apsnd (apsnd snd o nth xwfacts)) (id, i - facts_i)) iidths,
    1.37 @@ -278,7 +281,7 @@
    1.38        end)
    1.39    end
    1.40    handle SMT2_Failure.SMT fail => {outcome = SOME fail, rewrite_rules = [], conjecture_id = no_id,
    1.41 -    helper_ids = [], fact_ids = [], z3_proof = []}
    1.42 +    prem_ids = [], helper_ids = [], fact_ids = [], z3_proof = []}
    1.43  
    1.44  
    1.45  (* SMT tactic *)