# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1690365865 -7200
# Node ID 71713dd09c35d3055c30e71e524922d78fbf84b6
# Parent  0bd81d52859822f920d785a67286282d18c6ef19
support for let in Alethe name bindings;

diff -r 0bd81d528598 -r 71713dd09c35 src/HOL/Tools/SMT/smt_solver.ML
--- 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 =
diff -r 0bd81d528598 -r 71713dd09c35 src/HOL/Tools/SMT/smtlib_proof.ML
--- 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)