remove useless value in solver.ml, add solver.mli

src/symbolic/solver.ml

@@ -8,8 +8,6 @@ type solver = S : ('a solver_module * 'a) -> solver [@@unboxed]
 
 module Z3Batch = Smtml.Solver.Batch (Smtml.Z3_mappings)
 
-let solver_mod : Z3Batch.t solver_module = (module Z3Batch)
-
 let fresh_solver () =
   let module Mapping = Smtml.Z3_mappings.Fresh.Make () in
   let module Batch = Smtml.Solver.Batch (Mapping) in

src/symbolic/solver.mli

@@ -0,0 +1,19 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+type 'a solver_module = (module Smtml.Solver_intf.S with type t = 'a)
+
+module Z3Batch : sig
+  type t
+
+  val create : ?params:Smtml.Params.t -> ?logic:Smtml.Ty.logic -> unit -> t
+
+  val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability
+
+  val model : ?symbols:Smtml.Symbol.t list -> t -> Smtml.Model.t option
+end
+
+type solver = S : ('a solver_module * 'a) -> solver [@@unboxed]
+
+val fresh_solver : unit -> solver