# HG changeset patch # User desharna # Date 1648566764 -7200 # Node ID b269a3c84b9988e2f27703b6e1aa26d70dcd7688 # Parent 366f85a104071431d387813ebdb32fb2e198b673# Parent 1bad148d894fdf71ce30992268a84439736af2ae merged diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/cvc4_proof_parse.ML --- 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 diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/lethe_proof_parse.ML --- 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' @ diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/smt_translate.ML --- 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 diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/smtlib_interface.ML --- 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 = diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/verit_proof_parse.ML --- 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' @ diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/verit_replay.ML --- 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 = diff -r 366f85a10407 -r b269a3c84b99 src/HOL/Tools/SMT/z3_replay.ML --- 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 [])