--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Jul 25 18:52:34 2023 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Jul 26 12:04:25 2023 +0200
@@ -40,6 +40,17 @@
(*tactic*)
val smt_tac: Proof.context -> thm list -> int -> tactic
val smt_tac': Proof.context -> thm list -> int -> tactic
+
+ (*solver information*)
+ type solver_info = {
+ command: unit -> string list,
+ smt_options: (string * string) list,
+ good_slices: ((int * bool * bool * int * string) * string list) list,
+ parse_proof: Proof.context -> SMT_Translate.replay_data ->
+ ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
+ parsed_proof,
+ replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm}
+ val name_and_info_of: Proof.context -> string * solver_info
end;
structure SMT_Solver: SMT_SOLVER =
--- a/src/HOL/Tools/SMT/smtlib_proof.ML Tue Jul 25 18:52:34 2023 +0100
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Wed Jul 26 12:04:25 2023 +0200
@@ -330,7 +330,12 @@
SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S _, body] => extract body (tab, new)
| SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S _, body] => extract body (tab, new)
| SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S _, body] => extract body (tab, new)
- | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] =>
+ | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S lets, body] => (
+ let val bindings = map (fn SMTLIB.S (var :: bindings) => bindings) lets in
+ fold (fn bdgs => fn st => fold extract bdgs st) bindings (tab, new)
+ |> extract body
+ end)
+ | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S [_, bindings], body] =>
raise (Fail "unsupported let construction in name extraction")
| SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name]) =>
extract t (tab, new)