From 0d4d98edbe118079ccaf8202b755820cd4337bd6 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Mon, 18 Mar 2024 14:50:30 +0100
Subject: [PATCH] New exception for wrong model

We raise a new exception `Wrong_model` in `get_value` in order to
clarify the API.
---
 src/bin/common/solving_loop.ml        |  4 +--
 src/lib/reasoners/sat_solver_util.ml  | 48 +++++++++++++++------------
 src/lib/reasoners/sat_solver_util.mli |  5 ++-
 3 files changed, 32 insertions(+), 25 deletions(-)

diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
index 076170e9d1..9cf8714bee 100644
--- a/src/bin/common/solving_loop.ml
+++ b/src/bin/common/solving_loop.ml
@@ -103,7 +103,7 @@ let cmd_on_modes st modes cmd =
 let verify_model ~get_value () =
   match get_value [Expr.vrai] with
   | Some [e] when Expr.equal e Expr.vrai -> ()
-  | Some [_] | None | exception Sat_solver_sig.Unsat _ ->
+  | Some [_] | None | exception Sat_solver_util.Wrong_model _ ->
     recoverable_error "The model is wrong"
   | Some _ ->
     (* The length of the output list is the same as the length of the
@@ -831,7 +831,7 @@ let main () =
         (l, values)
     | None ->
       recoverable_error "No model produced, cannot execute get-value."
-    | exception Sat_solver_sig.Unsat _ ->
+    | exception Sat_solver_util.Wrong_model _ ->
       recoverable_error "The model is wrong, cannot execute get-value."
   in
 
diff --git a/src/lib/reasoners/sat_solver_util.ml b/src/lib/reasoners/sat_solver_util.ml
index 62f9f2b816..5c5cf7376a 100644
--- a/src/lib/reasoners/sat_solver_util.ml
+++ b/src/lib/reasoners/sat_solver_util.ml
@@ -81,6 +81,8 @@ let check (type a) (module SAT : S with type t = a) env =
   with
   | I_dont_know | Sat -> ()
 
+exception Wrong_model of Explanation.t
+
 (* Assert the last computed model in the environment [env].
 
    @raise Unsat if the solver found a contradiction, which means the model
@@ -179,28 +181,30 @@ let get_value (type a) (module SAT : S with type t = a) env l =
   (* We have to check the satisfability of the new environment [env] in order
      to produce a new model. If this call raise [Unsat], the model is wrong
      and we cannot produce model terms for the expressions of [l]. *)
-  check (module SAT) env;
-  let* mdl = SAT.get_model env in
-  let values =
-    List.map
-      (fun (v, name) ->
-         match v, name with
-         | Some v, None -> v
-         | None, Some name ->
-           begin match get_value_in_model (module SAT) env mdl name with
-             | Some v -> v
-             | None ->
-               (* The model generation has to produce a value for each
-                  declared names. If some declared names are missing in the
-                  model, it's a bug. *)
-               assert false
-           end
-         | _ ->
-           (* This case is excluded by the construction of the list [res]. *)
-           assert false
-      ) res
-  in
-  Some values
+  try
+    check (module SAT) env;
+    let* mdl = SAT.get_model env in
+    let values =
+      List.map
+        (fun (v, name) ->
+           match v, name with
+           | Some v, None -> v
+           | None, Some name ->
+             begin match get_value_in_model (module SAT) env mdl name with
+               | Some v -> v
+               | None ->
+                 (* The model generation has to produce a value for each
+                    declared names. If some declared names are missing in the
+                    model, it's a bug. *)
+                 assert false
+             end
+           | _ ->
+             (* This case is excluded by the construction of the list [res]. *)
+             assert false
+        ) res
+    in
+    Some values
+  with Unsat ex -> raise_notrace (Wrong_model ex)
 
 let get_assignment (type a) (module SAT : S with type t = a) env =
   List.map
diff --git a/src/lib/reasoners/sat_solver_util.mli b/src/lib/reasoners/sat_solver_util.mli
index 61493d93be..28cf313f8d 100644
--- a/src/lib/reasoners/sat_solver_util.mli
+++ b/src/lib/reasoners/sat_solver_util.mli
@@ -36,13 +36,16 @@ type lbool = False | True | Unknown
 
 val pp_lbool : lbool Fmt.t
 
+exception Wrong_model of Explanation.t
+
 val get_value : 'a sat_module -> 'a -> Expr.t list -> Expr.t list option
 (** [get_value (module SAT) env l] returns the model values of the expressions
     of [l] in the current generated model of [env].
 
     @return [None] if the model generation is not enabled or the
             environment is already unsatisfiable before calling this function.
-    @raise Unsat if the solver found a contradiction. *)
+    @raise Wrong_model if the solver found a contradiction in the current
+           model. *)
 
 val get_assignment : 'a sat_module -> 'a -> Expr.t list -> lbool list
 (** [get_assignment (module SAT) env l] returns the status of the literals [l]