Added support for Vampire as an SMT solver. (experimental)

--- a/NEWS	Wed Sep 17 20:57:11 2025 +0200
+++ b/NEWS	Fri Sep 19 13:11:51 2025 +0200
@@ -196,6 +196,9 @@
 nat are implemented by bit operations on target-language integers. Minor
 INCOMPATIBILITY.
 
+* SMT:
+  - Added Vampire as an SMT solver (experimental).
+
 * Theory "HOL.Fun":
   - Added lemmas.
       antimonotone_on_inf_fun

--- a/src/HOL/SMT.thy	Wed Sep 17 20:57:11 2025 +0200
+++ b/src/HOL/SMT.thy	Fri Sep 19 13:11:51 2025 +0200
@@ -627,6 +627,7 @@
 ML_file \<open>Tools/SMT/z3_isar.ML\<close>
 ML_file \<open>Tools/SMT/smt_solver.ML\<close>
 ML_file \<open>Tools/SMT/cvc_interface.ML\<close>
+ML_file \<open>Tools/SMT/vampire_interface.ML\<close>
 ML_file \<open>Tools/SMT/lethe_proof.ML\<close>
 ML_file \<open>Tools/SMT/lethe_isar.ML\<close>
 ML_file \<open>Tools/SMT/lethe_proof_parse.ML\<close>

--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Sep 17 20:57:11 2025 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Fri Sep 19 13:11:51 2025 +0200
@@ -162,6 +162,42 @@
 end
 
 
+(* Vampire *)
+
+local
+  fun vampire_smt_options ctxt =
+   ["--input_syntax", "smtlib2"] @
+    (case SMT_Config.get_timeout ctxt of
+      NONE => []
+    | SOME t => ["--time_limit", string_of_int (Time.toSeconds t) ^ "s"])
+
+  (* fun vampire_smt_outcome *)
+  fun on_vampire_relevant_line test_outcome solver_name lines =
+    on_first_line test_outcome solver_name (filter (String.isPrefix "% SZS status") lines)
+
+in
+
+val vampire_smt: SMT_Solver.solver_config = {
+  name = "vampire_smt",
+  class = K Vampire_Interface.smtlib_vampireC,
+  avail = is_some o check_tool "ISABELLE_VAMPIRE",
+  command = the o check_tool "ISABELLE_VAMPIRE",
+  options = vampire_smt_options,
+  smt_options = [],
+  good_slices =
+    (* FUDGE *)
+    [((2, false, false, 1024, meshN), []),
+     ((2, false, false, 512, mashN), []),
+     ((2, false, true, 128, meshN), []),
+     ((2, false, false, 64, meshN), []),
+     ((2, false, false, 256, mepoN), []),
+     ((2, false, false, 32, meshN), [])],
+  outcome =  on_vampire_relevant_line (outcome_of "% SZS status Unsatisfiable" "% SZS status Satisfiable" "TODO: unknown" "TODO: Time limit exceeded"),
+  parse_proof = NONE,
+  replay = NONE }
+
+end
+
 (* veriT *)
 
 local
@@ -286,6 +322,7 @@
   SMT_Solver.add_solver cvc4 #>
   SMT_Solver.add_solver cvc5 #>
   SMT_Solver.add_solver cvc5_proof #>
+  SMT_Solver.add_solver vampire_smt #>
   SMT_Solver.add_solver veriT #>
   SMT_Solver.add_solver z3)
 

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Sep 17 20:57:11 2025 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Fri Sep 19 13:11:51 2025 +0200
@@ -13,6 +13,14 @@
   val realsmlibC: SMT_Util.class
   val add_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
   val del_logic: int * (string -> term list -> string option) -> Context.generic -> Context.generic
+
+  type dtype_decls = (string * (string * (string * string) list) list) list
+  type func_decl = string * (string list * string)
+  val serialize: (BNF_Util.fp_kind * dtype_decls -> Buffer.T -> Buffer.T) -> (string * string) list -> string list ->
+    {dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
+     funcs: func_decl list, logic: string, sorts: string list} ->
+    (SMT_Util.role * SMT_Translate.sterm) list -> string
+
   val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
   val assert_name_of_role_and_index: SMT_Util.role -> int -> string
   val role_and_index_of_assert_name: string -> SMT_Util.role * int
@@ -157,11 +165,16 @@
 fun role_and_index_of_assert_name s =
   apsnd (the_default ~1 o Int.fromString) (unprefix_axiom s)
 
-fun sdtyp (fp, dtyps) =
+type dtype_decls = (string * (string * (string * string) list) list) list
+
+fun sdtyp (fp, dtyps : dtype_decls) =
   Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes () (") "))\n"
     (space_implode "\n  " (map sdatatype dtyps)))
 
-fun serialize smt_options comments {logic, sorts, dtyps, funcs} ts =
+type func_decl = string * (string list * string)
+
+fun serialize (sdtyp : BNF_Util.fp_kind * dtype_decls -> Buffer.T -> Buffer.T) smt_options comments
+      {logic, sorts, dtyps, funcs} ts =
   let
     val unsat_core = member (op =) smt_options (":produce-unsat-cores", "true")
   in
@@ -187,7 +200,7 @@
   order = order,
   logic = choose_logic ctxt,
   fp_kinds = [],
-  serialize = serialize}
+  serialize = serialize sdtyp}
 
 val _ = Theory.setup (Context.theory_map
   (setup_builtins #>

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/vampire_interface.ML	Fri Sep 19 13:11:51 2025 +0200
@@ -0,0 +1,44 @@
+(*  Title:      HOL/Tools/SMT/vampire_interface.ML
+    Author:     Jasmin Blanchette, LMU Muenchen
+    Author:     Elisabeth Lempa, LMU Muenchen
+
+Interface to Vampire as an SMT prover.
+*)
+
+signature VAMPIRE_INTERFACE =
+sig
+  val smtlib_vampireC: SMT_Util.class
+end;
+
+structure Vampire_Interface : VAMPIRE_INTERFACE =
+struct
+
+val vampireC = ["vampire"]
+val smtlib_vampireC = SMTLIB_Interface.smtlibC @ vampireC
+
+fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")"
+fun sctr (name, args) = enclose "(" ")" (implode_space (name :: map sctrarg args))
+fun sdatatype (_, ctrs) = enclose "(" ")" (implode_space (map sctr ctrs))
+fun sarity (name, _) = enclose "(" ")" (name ^ " 0")
+
+fun sdtyp ((fp, dtyps : SMTLIB_Interface.dtype_decls)) =
+  Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes (" ^
+    implode_space (map sarity dtyps) ^ ") (") "))\n"
+  (space_implode"\n  " (map sdatatype dtyps)))
+
+(* interface *)
+
+local
+  fun translate_config ctxt : SMT_Translate.config =
+    {order = SMT_Util.First_Order,
+     logic = K (K ""),
+     fp_kinds = [BNF_Util.Least_FP],
+     serialize = SMTLIB_Interface.serialize sdtyp}
+in
+
+val _ = Theory.setup (Context.theory_map
+  (SMT_Translate.add_config (smtlib_vampireC, translate_config)))
+
+end
+
+end;