Update the JS worker

We have to update the JS worker to dump models as we don't print models
in the library anymore.

src/bin/common/solving_loop.ml

@@ -154,15 +154,11 @@ let main () =
     (module SatCont.Make(TH) : Sat_solver_sig.S)
   in
 
-  let pp_unknown_reason_opt ppf = function
-    | None -> Fmt.pf ppf "Decided"
-    | Some ur -> Sat_solver_sig.pp_unknown_reason ppf ur
-  in
-
   let print_model ppf (Model ((module SAT), env)) =
     let ur = SAT.get_unknown_reason env in
     Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
-      "@[<v 0>; Returned unknown reason = %a@]" pp_unknown_reason_opt ur;
+      "@[<v 0>; Returned unknown reason = %a@]"
+      Sat_solver_sig.pp_unknown_reason_opt ur;
     match SAT.get_model env with
     | None ->
       Printer.print_fmt (Options.Output.get_fmt_diagnostic ())

src/bin/js/worker_js.ml

@@ -120,6 +120,22 @@ let main worker_id content =
       Frontend.print_status status n
     in
 
+    let print_model ppf env =
+      let ur = SAT.get_unknown_reason env in
+      Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
+        "@[<v 0>; Returned unknown reason = %a@]"
+        Sat_solver_sig.pp_unknown_reason_opt ur;
+      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."
+
+      | Some (lazy model) ->
+        Models.output_concrete_model ppf model
+    in
+
     let solve all_context (cnf, goal_name) =
       let used_context = Frontend.choose_used_context all_context ~goal_name in
       SAT.reset_refs ();
@@ -133,6 +149,16 @@ let main worker_id content =
       if Options.get_unsat_core () then begin
         unsat_core := Explanation.get_unsat_core ftnd_env.FE.expl;
       end;
+      let () =
+        match ftnd_env.FE.res with
+        | `Sat partial_model | `Unknown partial_model ->
+          begin
+            if Options.(get_interpretation () && get_dump_models ()) then
+              print_model (Options.Output.get_fmt_models ()) partial_model;
+          end
+        | `Unsat -> ()
+      in
+      ()
     in
 
     let typed_loop all_context state td =

src/lib/reasoners/sat_solver_sig.ml

@@ -47,6 +47,10 @@ let pp_unknown_reason ppf = function
   | Memout -> Fmt.pf ppf "Memout"
   | Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t
 
+let pp_unknown_reason_opt ppf = function
+  | None -> Fmt.pf ppf "Decided"
+  | Some ur -> pp_unknown_reason ppf ur
+
 module type S = sig
   type t
 

src/lib/reasoners/sat_solver_sig.mli

@@ -39,6 +39,7 @@ type unknown_reason =
   | Timeout of timeout_reason
 
 val pp_unknown_reason: unknown_reason Fmt.t
+val pp_unknown_reason_opt : unknown_reason option Fmt.t
 
 module type S = sig
   type t