Add the names of SMT solvers to their mappings (and log them with SMT queries)

src/smtml/altergo_mappings.default.ml

@@ -46,6 +46,8 @@ module M = struct
     include Dolmenexpr_to_expr.DolmenIntf
 
     module Internals = struct
+      let name = "Alt-Ergo"
+
       let caches_consts = false
 
       let is_available = true

src/smtml/bitwuzla_mappings.default.ml

@@ -8,6 +8,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   open B
 
   module Internals = struct
+    let name = "Bitwuzla"
+
     let caches_consts = false
 
     let is_available = true

src/smtml/colibri2_mappings.default.ml

@@ -24,6 +24,8 @@ module M = struct
     include Dolmenexpr_to_expr.DolmenIntf
 
     module Internals = struct
+      let name = "Colibri2"
+
       let caches_consts = false
 
       let is_available = true

src/smtml/cvc5_mappings.default.ml

@@ -7,6 +7,8 @@ include Mappings_intf
 
 module Fresh_cvc5 () = struct
   module Internals = struct
+    let name = "cvc5"
+
     let caches_consts = false
 
     let is_available = true

src/smtml/mappings.ml

@@ -911,7 +911,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
               M.Solver.check s.solver ~ctx ~assumptions:encoded_assuptions
             in
             let usage_after = Mtime_clock.count usage_before in
-            Utils.write assumptions (Mtime.Span.to_uint64_ns usage_after);
+            Utils.write M.Internals.name assumptions
+              (Mtime.Span.to_uint64_ns usage_after);
             res
           | None -> M.Solver.check s.solver ~ctx ~assumptions:encoded_assuptions
           )

src/smtml/mappings.nop.ml

@@ -5,6 +5,8 @@
 module Nop = struct
   module Make () = struct
     module Internals = struct
+      let name = "Nop"
+
       let caches_consts = false
 
       let is_available = false

src/smtml/mappings_intf.ml

@@ -91,6 +91,10 @@ module type M = sig
   val exists : term list -> term -> term
 
   module Internals : sig
+    (** [name] indicates the name of the solver for query logging and debugging
+        purposes. *)
+    val name : string
+
     (** [is_available] indicates whether the module is available for use. *)
     val is_available : bool
 

src/smtml/utils.ml

@@ -28,9 +28,9 @@ let[@inline never] protect m f =
    all queries sent to the solver (with their timestamps) to the given file *)
 let write =
   match query_log_path with
-  | None -> fun _ _ -> ()
+  | None -> fun _ _ _ -> ()
   | Some path ->
-    let log_entries : (Expr.t list * int64) list ref = ref [] in
+    let log_entries : (string * Expr.t list * int64) list ref = ref [] in
     let close () =
       let entries = List.rev !log_entries in
       let bytes = Marshal.to_string entries [] in
@@ -42,6 +42,6 @@ let write =
     Sys.set_signal Sys.sigterm (Sys.Signal_handle (fun _ -> close ()));
     (* write *)
     let mutex = Mutex.create () in
-    fun assumptions time ->
-      let entry = (assumptions, time) in
+    fun solver_name assumptions time ->
+      let entry = (solver_name, assumptions, time) in
       protect mutex (fun () -> log_entries := entry :: !log_entries)

src/smtml/z3_mappings.default.ml

@@ -9,6 +9,8 @@ include Mappings_intf
 module M = struct
   module Make () = struct
     module Internals = struct
+      let name = "Z3"
+
       let caches_consts = true
 
       let is_available = true