Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

--dump-models-on implies --dump-models #864

Closed
wants to merge 1 commit into from
Closed

--dump-models-on implies --dump-models #864

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
57 changes: 25 additions & 32 deletions src/bin/common/parse_command.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -362,8 +362,17 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation

let mk_output_opt
interpretation use_underscore unsat_core output_format model_type
() () () ()
produce_models dump_models dump_models_on () ()
=
let _ =
match dump_models_on with
| None ->
Options.set_dump_models dump_models
| Some ch ->
let out = Options.Output.create_channel ch in
Options.Output.set_dump_models out;
Options.set_dump_models true
in
set_infer_output_format (Option.is_none output_format);
let output_format = match output_format with
| None -> Native
Expand All @@ -373,7 +382,14 @@ let mk_output_opt
| None -> Value
| Some v -> v
in
set_interpretation interpretation;
let _ =
match interpretation with
| INone when produce_models || dump_models
|| Option.is_some dump_models_on ->
set_interpretation ILast
| interpretation ->
set_interpretation interpretation
in
set_interpretation_use_underscore use_underscore;
set_unsat_core unsat_core;
set_output_format output_format;
Expand Down Expand Up @@ -844,7 +860,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, dump_models_on, frontend =
let interpretation, produce_models, dump_models, dump_models_on, frontend =
let interpretation =
let doc = Format.sprintf
"Best effort support for counter-example generation. \
Expand Down Expand Up @@ -903,30 +919,15 @@ let parse_output_opt =
let dump_models_on =
let doc =
"Select a channel to output the models dumped by the option \
--dump-model."
--dump-models (implies --dump-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") &
Arg.(value & opt (some string) None &
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
| interpretation -> interpretation
in
Term.(
const mk_interpretation $ interpretation $
produce_models $ dump_models
),
interpretation,
produce_models,
dump_models,
dump_models_on,
frontend
Expand Down Expand Up @@ -1058,22 +1059,14 @@ let parse_output_opt =
)
in

let set_dump_models =
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_dump_models_on $
output_format $ model_type $ produce_models $
dump_models $ dump_models_on $
set_sat_options $ set_frontend
))

Expand Down
Loading