# HG changeset patch # User blanchet # Date 1401723267 -7200 # Node ID 24cbdebba35a2b00c90468667e0463f04f6eb97f # Parent f028d93798e685cee341a7e632aaeaaefa74df00 refactored Z3 to Isar proof construction code diff -r f028d93798e6 -r 24cbdebba35a src/HOL/SMT2.thy --- a/src/HOL/SMT2.thy Mon Jun 02 17:34:26 2014 +0200 +++ b/src/HOL/SMT2.thy Mon Jun 02 17:34:27 2014 +0200 @@ -149,8 +149,8 @@ ML_file "Tools/SMT2/smtlib2.ML" ML_file "Tools/SMT2/smtlib2_interface.ML" ML_file "Tools/SMT2/z3_new_proof.ML" +ML_file "Tools/SMT2/z3_new_isar.ML" ML_file "Tools/SMT2/smt2_solver.ML" -ML_file "Tools/SMT2/z3_new_isar.ML" ML_file "Tools/SMT2/z3_new_interface.ML" ML_file "Tools/SMT2/z3_new_replay_util.ML" ML_file "Tools/SMT2/z3_new_replay_literals.ML" diff -r f028d93798e6 -r 24cbdebba35a src/HOL/Tools/SMT2/smt2_solver.ML --- a/src/HOL/Tools/SMT2/smt2_solver.ML Mon Jun 02 17:34:26 2014 +0200 +++ b/src/HOL/Tools/SMT2/smt2_solver.ML Mon Jun 02 17:34:27 2014 +0200 @@ -26,10 +26,10 @@ val default_max_relevant: Proof.context -> string -> int (*filter*) - val smt2_filter: Proof.context -> thm -> ('a * (int option * thm)) list -> int -> Time.time -> - {outcome: SMT2_Failure.failure option, rewrite_rules: thm list, conjecture_id: int, - prem_ids: int list, helper_ids: (int * thm) list, fact_ids: (int * ('a * thm)) list, - z3_proof: Z3_New_Proof.z3_step list} + val smt2_filter: Proof.context -> thm -> ((string * 'a) * (int option * thm)) list -> int -> + Time.time -> + {outcome: SMT2_Failure.failure option, fact_ids: (int * ((string * 'a) * thm)) list, + atp_proof: unit -> (term, string) ATP_Proof.atp_step list} (*tactic*) val smt2_tac: Proof.context -> thm list -> int -> tactic @@ -273,20 +273,28 @@ |> (fn ((iidths0, z3_proof), {rewrite_rules, ...}) => let val iidths = if can_filter ctxt then iidths0 else map (apsnd (apfst (K no_id))) iwthms + fun id_of_index i = the_default no_id (Option.map fst (AList.lookup (op =) iidths i)) + + val conjecture_id = id_of_index conjecture_i + val prem_ids = map id_of_index (prems_i upto facts_i - 1) + val helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths + val fact_ids = map_filter (fn (i, (id, _)) => + try (apsnd (apsnd snd o nth xwfacts)) (id, i - facts_i)) iidths + val fact_helper_ts = + map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, prop_of th)) helper_ids @ + map (fn (_, ((s, _), th)) => (s, prop_of th)) fact_ids + val fact_helper_ids = + map (fn (id, th) => (id, ATP_Util.short_thm_name ctxt th)) helper_ids @ + map (fn (id, ((name, _), _)) => (id, name)) fact_ids in - {outcome = NONE, - rewrite_rules = rewrite_rules, - conjecture_id = id_of_index conjecture_i, - prem_ids = map id_of_index (prems_i upto facts_i - 1), - helper_ids = map_filter (try (fn (~1, idth) => idth)) iidths, - fact_ids = map_filter (fn (i, (id, _)) => - try (apsnd (apsnd snd o nth xwfacts)) (id, i - facts_i)) iidths, - z3_proof = z3_proof} + {outcome = NONE, fact_ids = fact_ids, + atp_proof = fn () => Z3_New_Isar.atp_proof_of_z3_proof ctxt rewrite_rules + (map Thm.prop_of prems) (Thm.term_of concl) fact_helper_ts prem_ids conjecture_id + fact_helper_ids z3_proof} end) end - handle SMT2_Failure.SMT fail => {outcome = SOME fail, rewrite_rules = [], conjecture_id = no_id, - prem_ids = [], helper_ids = [], fact_ids = [], z3_proof = []} + handle SMT2_Failure.SMT fail => {outcome = SOME fail, fact_ids = [], atp_proof = K []} (* SMT tactic *) diff -r f028d93798e6 -r 24cbdebba35a src/HOL/Tools/SMT2/z3_new_isar.ML --- a/src/HOL/Tools/SMT2/z3_new_isar.ML Mon Jun 02 17:34:26 2014 +0200 +++ b/src/HOL/Tools/SMT2/z3_new_isar.ML Mon Jun 02 17:34:27 2014 +0200 @@ -6,11 +6,9 @@ signature Z3_NEW_ISAR = sig - type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step - val atp_proof_of_z3_proof: Proof.context -> thm list -> term list -> term -> (string * term) list -> int list -> int -> (int * string) list -> Z3_New_Proof.z3_step list -> - (term, string) atp_step list + (term, string) ATP_Proof.atp_step list end; structure Z3_New_Isar: Z3_NEW_ISAR = diff -r f028d93798e6 -r 24cbdebba35a src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Jun 02 17:34:26 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Mon Jun 02 17:34:27 2014 +0200 @@ -158,8 +158,7 @@ reraise exn else {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)), - rewrite_rules = [], conjecture_id = ~1, prem_ids = [], helper_ids = [], - fact_ids = [], z3_proof = []} + fact_ids = [], atp_proof = K []} val death = Timer.checkRealTimer timer val outcome0 = if is_none outcome0 then SOME outcome else outcome0 @@ -226,8 +225,7 @@ end val weighted_factss = map (apsnd weight_facts) factss - val {outcome, filter_result = {rewrite_rules, conjecture_id, prem_ids, helper_ids, fact_ids, - z3_proof, ...}, used_from, run_time} = + val {outcome, filter_result = {fact_ids, atp_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 @@ -242,20 +240,8 @@ fn preplay => let fun isar_params () = - let - val fact_helper_ts = - map (fn (_, th) => (short_thm_name ctxt th, prop_of th)) helper_ids @ - map (fn ((s, _), th) => (s, prop_of th)) used_named_facts - val fact_helper_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 ctxt rewrite_rules hyp_ts - concl_t fact_helper_ts prem_ids conjecture_id fact_helper_ids z3_proof - in - (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, - minimize <> SOME false, atp_proof, goal) - end + (verbose, (NONE, NONE), preplay_timeout, compress_isar, try0_isar, + minimize <> SOME false, atp_proof (), goal) val one_line_params = (preplay, proof_banner mode name, used_facts,