From c699bc338b63ea5486b6326a51ab584db4c6586e Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Fri, 22 Sep 2023 16:39:50 +0200
Subject: [PATCH] Restoring dump-models option

The dump-models option have been broken by the refactoring in OptimAE.
I restore this feature.
---
 src/lib/frontend/frontend.ml | 17 +++----
 src/lib/frontend/models.ml   | 90 ++++++++++++++++++------------------
 2 files changed, 52 insertions(+), 55 deletions(-)

diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml
index c0276295b0..250642876c 100644
--- a/src/lib/frontend/frontend.ml
+++ b/src/lib/frontend/frontend.ml
@@ -162,24 +162,21 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     | Some SAT.ModelGen -> "ModelGen"
 
   let print_model env timeout =
-    let get_m = Options.get_interpretation () in
-    let s = timeout_reason_to_string timeout in
-    match SAT.get_model env with
-    | None ->
-      if get_m then
+    if Options.(get_interpretation () && get_dump_models ()) then begin
+      let s = timeout_reason_to_string timeout in
+      match SAT.get_model env with
+      | None ->
         Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
           "@[<v 0>It seems that no model has been computed so \
            far. You may need to change your model generation strategy \
            or to increase your timeouts. Returned timeout reason = %s@]" s
 
-    | Some m ->
-      assert (get_m);
-      if get_m then
+      | Some (lazy model) ->
         Printer.print_fmt
           (Options.Output.get_fmt_diagnostic ())
           "@[<v 0>; Returned timeout reason = %s@]" s;
-      let m = Lazy.force m in
-      Models.output_concrete_model (Options.Output.get_fmt_regular ()) m
+        Models.output_concrete_model (Options.Output.get_fmt_regular ()) model
+    end
 
   let process_decl print_status used_context consistent_dep_stack
       ((env, consistent, dep) as acc) d =
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index d601f9e581..8d5e315fdc 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -497,50 +497,50 @@ let output_concrete_model fmt m =
     Format.fprintf fmt "; This model is a best-effort. It includes symbols
         for which model generation is known to be incomplete. @.";
 
-    Format.fprintf fmt "@[<v 2>(";
-    if Options.get_model_type_constraints () then begin
-      Why3CounterExample.output_constraints fmt m.propositional
-    end;
-
-    let values = Hashtbl.create 17 in
-    (* Add the constants *)
-    ModelMap.iter (fun (f, xs_ty, _) st ->
-        assert (Lists.is_empty xs_ty);
-        ModelMap.V.iter (fun (keys, (value_r, value_s)) ->
-            assert (Lists.is_empty keys);
-            Hashtbl.add values f (value (value_r, value_s))
-          ) st
-      ) m.constants;
-
-    (* Add the arrays values, when applicable *)
-    ModelMap.iter (fun (f, xs_ty, ty) st ->
-        let root =
-          try Hashtbl.find values f
-          with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty))
-        in
-        Hashtbl.replace values f @@
-        ModelMap.V.fold (fun (keys, rs) acc ->
-            Store (acc, value (snd (List.hd keys)), value rs)) st root
-      ) m.arrays;
-
-    let pp_value =
-      pp_value (fun ppf (sy, _) ->
-          pp_value pp_constant ppf (Hashtbl.find values sy))
-    in
-
-    let pp_x ppf xs = pp_value ppf (value xs) in
-
-    (* Functions *)
-    let records =
-      SmtlibCounterExample.output_functions_counterexample
-        pp_x fmt MS.empty m.functions
-    in
-
-    (* Constants *)
-    SmtlibCounterExample.output_constants_counterexample
-      pp_x fmt records m.constants;
-
-    (* Arrays *)
-    (*     SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *)
+  Format.fprintf fmt "@[<v 2>(";
+  if Options.get_model_type_constraints () then begin
+    Why3CounterExample.output_constraints fmt m.propositional
+  end;
+
+  let values = Hashtbl.create 17 in
+  (* Add the constants *)
+  ModelMap.iter (fun (f, xs_ty, _) st ->
+      assert (Lists.is_empty xs_ty);
+      ModelMap.V.iter (fun (keys, (value_r, value_s)) ->
+          assert (Lists.is_empty keys);
+          Hashtbl.add values f (value (value_r, value_s))
+        ) st
+    ) m.constants;
+
+  (* Add the arrays values, when applicable *)
+  ModelMap.iter (fun (f, xs_ty, ty) st ->
+      let root =
+        try Hashtbl.find values f
+        with Not_found -> Constant (f, Tfarray (List.hd xs_ty, ty))
+      in
+      Hashtbl.replace values f @@
+      ModelMap.V.fold (fun (keys, rs) acc ->
+          Store (acc, value (snd (List.hd keys)), value rs)) st root
+    ) m.arrays;
+
+  let pp_value =
+    pp_value (fun ppf (sy, _) ->
+        pp_value pp_constant ppf (Hashtbl.find values sy))
+  in
+
+  let pp_x ppf xs = pp_value ppf (value xs) in
+
+  (* Functions *)
+  let records =
+    SmtlibCounterExample.output_functions_counterexample
+      pp_x fmt MS.empty m.functions
+  in
+
+  (* Constants *)
+  SmtlibCounterExample.output_constants_counterexample
+    pp_x fmt records m.constants;
+
+  (* Arrays *)
+  (*     SmtlibCounterExample.output_arrays_counterexample fmt m.arrays; *)
 
   Printer.print_fmt fmt "@]@,)";