# HG changeset patch # User blanchet # Date 1394713094 -3600 # Node ID bc036c1cf1112bb22e6d5857e5d249560edebf9d # Parent d530cc905c2f30c4de21c1d1af7b49bf0e5369f5 thread through step IDs from Z3 to Sledgehammer diff -r d530cc905c2f -r bc036c1cf111 src/HOL/Tools/SMT2/smt2_solver.ML --- a/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:14 2014 +0100 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML Thu Mar 13 13:18:14 2014 +0100 @@ -20,20 +20,20 @@ cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> term list * term list) option, replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> - (int list * Z3_New_Proof.z3_step list) * thm) option } + ((int * int) list * Z3_New_Proof.z3_step list) * thm) option } (*registry*) val add_solver: solver_config -> theory -> theory val solver_name_of: Proof.context -> string val available_solvers_of: Proof.context -> string list val apply_solver: Proof.context -> (int * (int option * thm)) list -> - (int list * Z3_New_Proof.z3_step list) * thm + ((int * int) list * Z3_New_Proof.z3_step list) * thm val default_max_relevant: Proof.context -> string -> int (*filter*) val smt2_filter: Proof.context -> thm list -> thm -> ('a * (int option * thm)) list -> int -> - Time.time -> {outcome: SMT2_Failure.failure option, used_facts: ('a * thm) list, - z3_steps: Z3_New_Proof.z3_step list} + Time.time -> {outcome: SMT2_Failure.failure option, used_fact_infos: (int * ('a * thm)) list, + z3_proof: Z3_New_Proof.z3_step list} (*tactic*) val smt2_tac: Proof.context -> thm list -> int -> tactic @@ -152,7 +152,7 @@ cex_parser: (Proof.context -> SMT2_Translate.replay_data -> string list -> term list * term list) option, replay: (Proof.context -> SMT2_Translate.replay_data -> string list -> - (int list * Z3_New_Proof.z3_step list) * thm) option } + ((int * int) list * Z3_New_Proof.z3_step list) * thm) option } (* registry *) @@ -162,7 +162,7 @@ default_max_relevant: int, supports_filter: bool, replay: Proof.context -> string list * SMT2_Translate.replay_data -> - (int list * Z3_New_Proof.z3_step list) * thm } + ((int * int) list * Z3_New_Proof.z3_step list) * thm } structure Solvers = Generic_Data ( @@ -275,7 +275,9 @@ val xthms = map (apsnd snd) xwthms - val filter_thms = if supports_filter ctxt then map_filter (try (nth xthms)) else K xthms + val used_fact_infos_of = + if supports_filter ctxt then map_filter (try (apsnd (nth xthms))) + else K (map (pair ~1) xthms) in map snd xwthms |> map_index I @@ -283,23 +285,24 @@ |> check_topsorts ctxt |> apply_solver ctxt |> fst - |> (fn (is, z3_steps) => {outcome = NONE, used_facts = filter_thms is, z3_steps = z3_steps}) + |> (fn (idis, z3_proof) => + {outcome = NONE, used_fact_infos = used_fact_infos_of idis, z3_proof = z3_proof}) end - handle SMT2_Failure.SMT fail => {outcome = SOME fail, used_facts = [], z3_steps = []} + handle SMT2_Failure.SMT fail => {outcome = SOME fail, used_fact_infos = [], z3_proof = []} (* SMT tactic *) local - fun trace_assumptions ctxt iwthms idxs = + fun trace_assumptions ctxt iwthms idis = let val wthms = - idxs + idis + |> map snd |> filter (fn i => i >= 0) |> map_filter (AList.lookup (op =) iwthms) in - if Config.get ctxt SMT2_Config.trace_used_facts andalso length wthms > 0 - then + if Config.get ctxt SMT2_Config.trace_used_facts andalso length wthms > 0 then tracing (Pretty.string_of (Pretty.big_list "SMT used facts:" (map (Display.pretty_thm ctxt o snd) wthms))) else () diff -r d530cc905c2f -r bc036c1cf111 src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 13:18:14 2014 +0100 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Thu Mar 13 13:18:14 2014 +0100 @@ -8,7 +8,8 @@ sig type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (term, string) atp_step list + val atp_proof_of_z3_proof: theory -> Z3_New_Proof.z3_step list -> (int * string) list -> + (term, string) atp_step list end; structure Z3_New_Isar: Z3_NEW_ISAR = @@ -73,29 +74,24 @@ fun simplify_line (name, role, t, rule, deps) = (name, role, simplify_prop t, rule, deps) -fun atp_proof_of_z3_proof thy proof = +fun atp_proof_of_z3_proof thy proof fact_ids = let - fun step_name_of id = (string_of_int id, []) - - (* FIXME: find actual conjecture *) - val id_of_conjecture = - proof - |> find_first (fn Z3_New_Proof.Z3_Step {rule, ...} => rule = Z3_New_Proof.Asserted) - |> Option.map (fn Z3_New_Proof.Z3_Step {id, ...} => id) - fun step_of (Z3_New_Proof.Z3_Step {id, rule, prems, concl, ...}) = let + fun step_name_of id = (string_of_int id, the_list (AList.lookup (op =) fact_ids id)) + + val name as (_, ss) = step_name_of id val role = (case rule of Z3_New_Proof.Asserted => - if id_of_conjecture = SOME id then Negated_Conjecture else Hypothesis + if null ss then Negated_Conjecture (* FIXME: or hypothesis! *) else Axiom | Z3_New_Proof.Rewrite => Lemma | Z3_New_Proof.Rewrite_Star => Lemma | Z3_New_Proof.Skolemize => Lemma | Z3_New_Proof.Th_Lemma _ => Lemma | _ => Plain) in - (step_name_of id, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl), + (name, role, HOLogic.mk_Trueprop (Object_Logic.atomize_term thy concl), Z3_New_Proof.string_of_rule rule, map step_name_of prems) end in diff -r d530cc905c2f -r bc036c1cf111 src/HOL/Tools/SMT2/z3_new_replay.ML --- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:14 2014 +0100 +++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Mar 13 13:18:14 2014 +0100 @@ -8,7 +8,7 @@ signature Z3_NEW_REPLAY = sig val replay: Proof.context -> SMT2_Translate.replay_data -> string list -> - (int list * Z3_New_Proof.z3_step list) * thm + ((int * int) list * Z3_New_Proof.z3_step list) * thm end structure Z3_New_Replay: Z3_NEW_REPLAY = @@ -106,26 +106,24 @@ val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt in (thm' RS thm, ctxt') end - fun add1 id fixes thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) = + fun add1 id fixes thm1 ((i, th), exact) ((idis, thms), (ctxt, ptab)) = let val (thm, ctxt') = if exact then (Thm.implies_elim thm1 th, ctxt) else assume thm1 ctxt val thms' = if exact then thms else th :: thms - in ((insert (op =) i is, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end + in (((id, i) :: idis, thms'), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end fun add (Z3_New_Proof.Z3_Step {id, rule, concl, fixes, ...}) - (cx as ((is, thms), (ctxt, ptab))) = + (cx as ((idis, thms), (ctxt, ptab))) = if Z3_New_Replay_Methods.is_assumption rule andalso rule <> Z3_New_Proof.Hypothesis then let val ct = SMT2_Util.certify ctxt concl - val thm1 = - Thm.trivial ct - |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) + val thm1 = Thm.trivial ct |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt)) val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1 in (case lookup_assm assms_net (Thm.cprem_of thm2 1) of [] => let val (thm, ctxt') = assume thm1 ctxt - in ((is, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end + in ((idis, thms), (ctxt', Inttab.update (id, (fixes, thm)) ptab)) end | ithms => fold (add1 id fixes thm1) ithms cx) end else @@ -178,10 +176,10 @@ ({context=ctxt, typs, terms, rewrite_rules, assms} : SMT2_Translate.replay_data) output = let val (steps, ctxt2) = Z3_New_Proof.parse typs terms output ctxt - val ((is, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 + val ((idis, rules), (ctxt3, assumed)) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2 in if Config.get ctxt3 SMT2_Config.filter_only_facts then - ((is, steps), TrueI) + ((idis, steps), TrueI) else let val ctxt4 = put_simpset (Z3_New_Replay_Util.make_simpset ctxt3 []) ctxt3 diff -r d530cc905c2f -r bc036c1cf111 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:14 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu Mar 13 13:18:14 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_facts, z3_steps} = + val {outcome, used_fact_infos, z3_proof} = 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_facts = [], z3_steps = []} + used_fact_infos = [], z3_proof = []} val death = Timer.checkRealTimer timer val outcome0 = if is_none outcome0 then SOME outcome else outcome0 @@ -206,8 +206,9 @@ do_slice timeout (slice + 1) outcome0 time_so_far weighted_factss end else - {outcome = if is_none outcome then NONE else the outcome0, used_facts = used_facts, - used_from = map (apsnd snd) weighted_facts, z3_steps = z3_steps, run_time = time_so_far} + {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} end in do_slice timeout 1 NONE Time.zeroTime @@ -225,21 +226,23 @@ map (weight_smt2_fact ctxt num_facts) (facts ~~ (0 upto num_facts - 1)) end - val weighted_factss = factss |> map (apsnd weight_facts) - val {outcome, used_facts = used_pairs, used_from, z3_steps, run_time} = + 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_facts = used_pairs |> map fst - val outcome = outcome |> Option.map failure_of_smt2_failure + val used_named_facts = map snd used_fact_infos + val used_facts = map fst used_named_facts + val outcome = Option.map failure_of_smt2_failure outcome val (preplay, message, message_tail) = (case outcome of NONE => (Lazy.lazy (fn () => - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + play_one_line_proof mode debug verbose preplay_timeout used_named_facts state subgoal SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)), fn preplay => let - val atp_proof = Z3_New_Isar.atp_proof_of_z3_proof thy z3_steps + 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 isar_params = K (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, minimize <> SOME false, atp_proof, goal)