Adding an option to dump models on a specific output channel

src/bin/common/parse_command.ml

@@ -367,7 +367,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
 
 let mk_output_opt
     interpretation use_underscore unsat_core output_format model_type
-    () () ()
+    () () () ()
   =
   set_infer_output_format (Option.is_none output_format);
   let output_format = match output_format with
@@ -849,7 +849,7 @@ let parse_output_opt =
 
   (* Use the --interpretation and --produce-models (which is equivalent to
      --interpretation last) to determine the interpretation value. *)
-  let interpretation, dump_models, frontend =
+  let interpretation, dump_models, dump_models_on, frontend =
     let interpretation =
       let doc = Format.sprintf
           "Best effort support for counter-example generation. \
@@ -882,6 +882,7 @@ let parse_output_opt =
       Arg.(value & flag & info ["produce-models"] ~doc ~docs:s_models)
     in
 
+
     let frontend =
       let doc = "Select the parsing and typing frontend." in
       let docv = "FTD" in
@@ -910,6 +911,24 @@ let parse_output_opt =
       Arg.(value & flag & info ["dump-models"] ~doc ~docs:s_models)
     in
 
+    let dump_models_on =
+      let doc =
+        "Select a channel to output the models dumped by the option \
+         --dump-model."
+      in
+      let docv = "VAL" in
+      let chan =
+        Arg.conv
+          ~docv
+          (
+            (fun s -> Ok (Output.create_channel s)),
+            (fun fmt f -> Format.pp_print_string fmt (Output.to_string f))
+          )
+      in
+      Arg.(value & opt chan (Output.create_channel "stderr") &
+           info ["dump-models-on"] ~docv ~docs:s_models ~doc)
+    in
+
     let mk_interpretation interpretation produce_models dump_models =
       match interpretation with
       | INone when produce_models || dump_models -> ILast
@@ -920,6 +939,7 @@ let parse_output_opt =
       produce_models $ dump_models
     ),
     dump_models,
+    dump_models_on,
     frontend
   in
 
@@ -1073,15 +1093,19 @@ let parse_output_opt =
     Term.(const set_dump_models $ dump_models)
   in
 
+  let set_dump_models_on =
+    Term.(const Output.set_dump_models $ dump_models_on)
+  in
+
   let set_frontend =
     Term.(const set_frontend $ frontend)
   in
 
   Term.(ret (const mk_output_opt $
              interpretation $ use_underscore $ unsat_core $
              output_format $ model_type $
-             set_dump_models $ set_sat_options $
-             set_frontend
+             set_dump_models $ set_dump_models_on $
+             set_sat_options $ set_frontend
             ))
 
 let parse_profiling_opt =

src/lib/reasoners/fun_sat.ml

@@ -1193,7 +1193,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
     let prop_model = extract_prop_model ~complete_model:true env in
     if Options.(get_interpretation () && get_dump_models ()) then
-      Th.output_concrete_model (Options.Output.get_fmt_regular ()) ~prop_model
+      Th.output_concrete_model (Options.Output.get_fmt_models ()) ~prop_model
         env.tbox;
 
     terminated_normally := true;

src/lib/util/options.ml

@@ -32,16 +32,23 @@ module Output = struct
   type t =
     | Stdout
     | Stderr
-    | Channel of out_channel * Format.formatter
+    | Channel of string * out_channel * Format.formatter
     | Fmt of Format.formatter
     | Invalid
 
+  let to_string = function
+    | Stdout -> "stdout"
+    | Stderr -> "stderr"
+    | Channel (fname, _, _) -> fname
+    | Fmt _ -> "custom formatter"
+    | Invalid -> "invalid"
+
   let of_formatter fmt = Fmt fmt
 
   let to_formatter = function
     | Stdout -> Format.std_formatter
     | Stderr -> Format.err_formatter
-    | Channel (_, fmt) -> fmt
+    | Channel (_, _, fmt) -> fmt
     | Fmt fmt -> fmt
     | Invalid -> assert false
 
@@ -51,16 +58,23 @@ module Output = struct
     | str ->
       let cout = open_out str in
       let fmt = Format.formatter_of_out_channel cout in
-      Channel (cout, fmt)
+      Channel (str, cout, fmt)
 
   let regular_output = ref Stdout
   let diagnostic_output = ref Stderr
+  let dump_models_output = ref Stderr
+
+  let all_channels = [
+    regular_output;
+    diagnostic_output;
+    dump_models_output;
+  ]
 
   let close o =
     match o with
     | Stdout | Stderr | Fmt _ ->
       Format.pp_print_flush (to_formatter o) ();
-    | Channel (cout, _) ->
+    | Channel (_, cout, _) ->
       Format.pp_print_flush (to_formatter o) ();
       close_out cout
     | Invalid -> ()
@@ -69,15 +83,15 @@ module Output = struct
     close !output;
     output := o
 
-  let close_all () =
-    set_output regular_output Invalid;
-    set_output diagnostic_output Invalid
+  let close_all () = List.iter (fun o -> set_output o Invalid) all_channels
 
   let set_regular o = set_output regular_output o
   let set_diagnostic o = set_output diagnostic_output o
+  let set_dump_models o = set_output dump_models_output o
 
   let get_fmt_regular () = to_formatter !regular_output
   let get_fmt_diagnostic () = to_formatter !diagnostic_output
+  let get_fmt_models () = to_formatter !dump_models_output
 end
 
 (* Declaration of all the options as refs with default values *)

src/lib/util/options.mli

@@ -1071,10 +1071,13 @@ module Output : sig
   type t = private
     | Stdout
     | Stderr
-    | Channel of out_channel * Format.formatter
+    | Channel of string * out_channel * Format.formatter
     | Fmt of Format.formatter
     | Invalid
 
+  val to_string : t -> string
+  (** [to_string] Returns a string representation of the output channel. *)
+
   val of_formatter : Format.formatter -> t
   (** [of_formatter fmt] create an out channel of the formatter [fmt]. *)
 
@@ -1103,6 +1106,11 @@ module Output : sig
 
       Default to [Format.err_formatter]. *)
 
+  val set_dump_models : t -> unit
+  (** Set the models output channel used by the option `--dump-models`.
+
+      Default to [Format.err_formatter]. *)
+
   val get_fmt_regular : unit -> Format.formatter
   (** Value specifying the formatter used to output results.
 
@@ -1111,6 +1119,12 @@ module Output : sig
   val get_fmt_diagnostic : unit -> Format.formatter
   (** Value specifying the formatter used to output errors.
 
+      Default to [Format.err_formatter]. *)
+
+  val get_fmt_models : unit -> Format.formatter
+  (** Value specifying the formatter used to output models printed by
+      the `--dump-models` option.
+
       Default to [Format.err_formatter]. *)
 end