--- 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"
--- 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 *)
--- 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 =
--- 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,