From c48a365a8cf90b21c92a34becb35d2ca5a4170e8 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Sep 2023 17:08:44 +0200 Subject: [PATCH] Adding an option to dump models on a specific output channel --- src/bin/common/parse_command.ml | 31 +++++++++++++++++++++++++++---- src/lib/reasoners/fun_sat.ml | 2 +- src/lib/util/options.ml | 18 ++++++++++++++---- src/lib/util/options.mli | 16 +++++++++++++++- 4 files changed, 57 insertions(+), 10 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 04a2c61b4..439b99a7a 100644 --- a/src/bin/common/parse_command.ml +++ b/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,23 @@ 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." + 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 +938,7 @@ let parse_output_opt = produce_models $ dump_models ), dump_models, + dump_models_on, frontend in @@ -1073,6 +1092,10 @@ 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 @@ -1080,8 +1103,8 @@ let parse_output_opt = 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 = diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index fb2cfb874..9f5a08ac9 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/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; diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index bbfe77d6e..2a74ee911 100644 --- a/src/lib/util/options.ml +++ b/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,17 @@ 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 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 -> () @@ -75,9 +83,11 @@ module Output = struct 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 *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 21d841bc7..f146f33d0 100644 --- a/src/lib/util/options.mli +++ b/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