Add get_sat_model and improve model documentation

- Add comprehensive documentation for new `get_sat_model` function
- Improve clarity and structure of `model` documentation
- Add cross-references between `model` and `get_sat_model`
- Clarify usage for cached vs. non-cached solvers

src/smtml/solver.ml

@@ -55,6 +55,16 @@ module Base (M : Mappings_intf.S) = struct
   let model ?(symbols : Symbol.t list option) (s : M.solver) : Model.t option =
     let+ model = M.Solver.model s in
     M.values_of_model ?symbols model
+
+  let get_sat_model ?symbols s set =
+    match check_set s set with
+    | `Sat -> (
+      match model ?symbols s with
+      | Some _ as model -> model
+      | None ->
+        (* Should never happen *)
+        assert false )
+    | `Unsat | `Unknown -> None
 end
 
 module Incremental (M : Mappings_intf.S) : Solver_intf.S =
@@ -117,6 +127,16 @@ module Batch (Mappings : Mappings.S) = struct
   let model ?(symbols : Symbol.t list option) (s : t) : Model.t option =
     model ?symbols s.solver
 
+  let get_sat_model ?symbols s set =
+    match check_set s set with
+    | `Sat -> (
+      match model ?symbols s with
+      | Some _ as model -> model
+      | None ->
+        (* Should never happen *)
+        assert false )
+    | `Unsat | `Unknown -> None
+
   let interrupt { solver; _ } = interrupt solver
 end
 
@@ -181,6 +201,17 @@ module Cached (Mappings_ : Mappings.S) = struct
 
     let get_statistics (s : t) : Statistics.t = get_statistics s.solver
 
+    let get_sat_model ?symbols s set =
+      let assert_ = Expr.Set.union set s.top in
+      match check_set s.solver assert_ with
+      | `Sat -> (
+        match model ?symbols s.solver with
+        | Some _ as model -> model
+        | None ->
+          (* Should never happen *)
+          assert false )
+      | `Unsat | `Unknown -> None
+
     let check_set s es =
       let assert_ = Expr.Set.union es s.top in
       match Cache.find_opt cache assert_ with

src/smtml/solver_intf.ml

@@ -89,8 +89,25 @@ module type S = sig
   (** [model ?symbols solver] retrieves the model of the last [check] query. If
       [?symbols] is provided, only the values of the specified symbols are
       included. Returns [None] if [check] was not invoked before or its result
-      was not [`Sat]. *)
+      was not [`Sat].
+
+      @warning Not compatible with cached solver mode - use {!get_sat_model} instead
+      @see 'get_sat_model' For cached solver-compatible alternative *)
   val model : ?symbols:Symbol.t list -> t -> Model.t option
+
+  (** Compute and retrieve a model for specific constraints.
+
+      [get_sat_model ?symbols solver exprs] performs:
+        1. [check_set] with [exprs] constraints
+        2. Returns model if result is [`Sat]
+
+      Filters output using [?symbols] when provided. Designed for cached
+      solvers.
+
+      @see {!model} For non-cached solvers when you have already performed
+      your own [check]/[check_set] and want to retrieve the results *)
+  val get_sat_model :
+    ?symbols:Symbol.t list -> t -> Expr.Set.t -> Model.t option
 end
 
 (** The [Intf] module type defines the interface for creating and working with