--- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/cvc4_proof_parse.ML Tue Mar 29 17:12:44 2022 +0200
@@ -37,7 +37,7 @@
val fact_ids' =
map_filter (fn j =>
- let val (i, _) = nth assms j in
+ let val ((i, _), _) = nth assms j in
try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
end) used_assm_js
in
--- a/src/HOL/Tools/SMT/lethe_proof_parse.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_proof_parse.ML Tue Mar 29 17:12:44 2022 +0200
@@ -32,13 +32,16 @@
val id_of_index = Integer.add num_ll_defs
val index_of_id = Integer.add (~ num_ll_defs)
- fun step_of_assume j (_, th) =
- Lethe_Proof.Lethe_Step {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j),
+ fun step_of_assume j ((_, role), th) =
+ Lethe_Proof.Lethe_Step
+ {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j),
rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
val (actual_steps, _) = Lethe_Proof.parse typs terms output ctxt
val used_assert_ids =
- map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output
+ actual_steps
+ |> map_filter (fn (Lethe_Step { id, ...}) =>
+ try (snd o SMTLIB_Interface.role_and_index_of_assert_name) id)
val used_assm_js =
map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
used_assert_ids
@@ -57,10 +60,11 @@
val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
val fact_ids' =
map_filter (fn j =>
- let val (i, _) = nth assms j in
+ let val ((i, _), _) = nth assms j in
try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
end) used_assm_js
- val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms
+ val helper_ids' =
+ map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms
val fact_helper_ts =
map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @
--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Tue Mar 29 17:12:44 2022 +0200
@@ -32,7 +32,7 @@
terms: term Symtab.table,
ll_defs: term list,
rewrite_rules: thm list,
- assms: (int * thm) list }
+ assms: ((int * SMT_Util.role) * thm) list }
(*translation*)
val add_config: SMT_Util.class * (Proof.context -> config) -> Context.generic -> Context.generic
@@ -79,7 +79,7 @@
terms: term Symtab.table,
ll_defs: term list,
rewrite_rules: thm list,
- assms: (int * thm) list }
+ assms: ((int * SMT_Util.role) * thm) list }
(* translation context *)
@@ -133,7 +133,7 @@
val terms' = Termtab.fold add_fun terms Symtab.empty
in
{context = ctxt, typs = typs', terms = terms', ll_defs = ll_defs, rewrite_rules = rules,
- assms = map (apfst fst) assms}
+ assms = assms}
end
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Tue Mar 29 17:12:44 2022 +0200
@@ -148,8 +148,8 @@
fun unprefix_axiom s =
try (pair SMT_Util.Conjecture o unprefix conjecture_prefix) s
- |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix hypothesis_prefix) s)
- |> curry merge_options (try (pair SMT_Util.Conjecture o unprefix axiom_prefix) s)
+ |> curry merge_options (try (pair SMT_Util.Hypothesis o unprefix hypothesis_prefix) s)
+ |> curry merge_options (try (pair SMT_Util.Axiom o unprefix axiom_prefix) s)
|> the
fun role_and_index_of_assert_name s =
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Mar 29 17:12:44 2022 +0200
@@ -35,9 +35,9 @@
val id_of_index = Integer.add num_ll_defs
val index_of_id = Integer.add (~ num_ll_defs)
- fun step_of_assume j (_, th) =
+ fun step_of_assume j ((_, role), th) =
Verit_Proof.VeriT_Step
- {id = SMTLIB_Interface.assert_name_of_role_and_index SMT_Util.Axiom (id_of_index j),
+ {id = SMTLIB_Interface.assert_name_of_role_and_index role (id_of_index j),
rule = input_rule, prems = [], proof_ctxt = [], concl = Thm.prop_of th, fixes = []}
val (actual_steps, _) = Verit_Proof.parse typs terms output ctxt
@@ -60,10 +60,11 @@
val prem_ids = map id_of_index (prems_i upto prems_i + num_prems - 1)
val fact_ids' =
map_filter (fn j =>
- let val (i, _) = nth assms j in
+ let val ((i, _), _) = nth assms j in
try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
end) used_assm_js
- val helper_ids' = filter (fn (i, _) => i >= helpers_i) used_assms
+ val helper_ids' =
+ map_filter (fn ((i, _), thm) => if i >= helpers_i then SOME (i, thm) else NONE) used_assms
val fact_helper_ts =
map (fn (_, th) => (ATP_Util.short_thm_name ctxt th, Thm.prop_of th)) helper_ids' @
--- a/src/HOL/Tools/SMT/verit_replay.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_replay.ML Tue Mar 29 17:12:44 2022 +0200
@@ -272,7 +272,7 @@
fun cond rule = rule = Verit_Proof.input_rule
val add_asssert = SMT_Replay.add_asserted Symtab.update Symtab.empty extract cond
val ((_, _), (ctxt3, assumed)) =
- add_asssert outer_ctxt rewrite_rules assms
+ add_asssert outer_ctxt rewrite_rules (map (apfst fst) assms)
(map_filter (remove_rewrite_rules_from_rules num_ll_defs) assm_steps) ctxt2
val used_rew_js =
--- a/src/HOL/Tools/SMT/z3_replay.ML Tue Mar 29 15:44:27 2022 +0200
+++ b/src/HOL/Tools/SMT/z3_replay.ML Tue Mar 29 17:12:44 2022 +0200
@@ -123,7 +123,7 @@
xfacts prems concl output =
let
val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt
- val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+ val ((iidths, _), _) = add_asserted outer_ctxt rewrite_rules (map (apfst fst) assms) steps ctxt2
fun id_of_index i = the_default ~1 (Option.map fst (AList.lookup (op =) iidths i))
@@ -153,7 +153,7 @@
let
val (steps, ctxt2) = Z3_Proof.parse typs terms output ctxt
val ((_, rules), (ctxt3, assumed)) =
- add_asserted outer_ctxt rewrite_rules assms steps ctxt2
+ add_asserted outer_ctxt rewrite_rules (map (apfst fst) assms) steps ctxt2
val ctxt4 =
ctxt3
|> put_simpset (SMT_Replay.make_simpset ctxt3 [])