Skip to content

Commit

Permalink
Remove deprecated options
Browse files Browse the repository at this point in the history 
These options have been deprecated in v2.6.0.
  • Loading branch information
@Halbaroth
Halbaroth committed Nov 5, 2024
1 parent 35c0f14 commit 5ee6ed2
Show file tree
Hide file tree
Showing 3 changed files with 12 additions and 87 deletions.
87 changes: 12 additions & 75 deletions src/bin/common/parse_command.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,6 @@ module Debug = struct
| Arith
| Arrays
| Bitv
| Sum
| Ite
| Cc
| Combine
Expand All @@ -165,20 +164,18 @@ module Debug = struct
| Split
| Triggers
| Types
| Typing
| Uf
| Unsat_core
| Use
| Warnings
| Commands
| Optimize
[@@deriving eq]

let all = [
Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite;
Debug; Ac; Adt; Arith; Arrays; Bitv; Ite;
Cc; Combine; Constr; Explanations; Fm; Fpa; Gc;
Interpretation; Intervals; Matching; Sat; Split; Triggers;
Types; Typing; Uf; Unsat_core; Use; Warnings;
Types; Uf; Unsat_core; Use;
Commands; Optimize
]

Expand All @@ -189,7 +186,6 @@ module Debug = struct
| Arith -> "arith"
| Arrays -> "arrays"
| Bitv -> "bitv"
| Sum -> "sum"
| Ite -> "ite"
| Cc -> "cc"
| Combine -> "combine"
Expand All @@ -205,11 +201,9 @@ module Debug = struct
| Split -> "split"
| Triggers -> "triggers"
| Types -> "types"
| Typing -> "typing"
| Uf -> "uf"
| Unsat_core -> "unsat-core"
| Use -> "use"
| Warnings -> "warnings"
| Commands -> "commands"
| Optimize -> "optimize"

Expand Down Expand Up @@ -238,14 +232,6 @@ module Debug = struct
| Bitv ->
Options.set_debug_bitv true;
set_level Bitv.src
| Sum ->
Printer.print_wrn
"The debug flag 'sum' is deprecated and is replaced by 'adt'. \
It has the same effect as 'adt' and will be removed in a future \
version.";
Options.set_debug_adt true;
set_level Adt.src;
set_level Adt_rel.src
| Ite ->
Options.set_debug_ite true;
set_level Ite_rel.src
Expand Down Expand Up @@ -290,10 +276,6 @@ module Debug = struct
| Types ->
Options.set_debug_types true;
set_level S.types
| Typing ->
Printer.print_wrn
"The debug flag 'typing' has no effect. It will be removed in a \
future version."
| Uf ->
Options.set_debug_uf true;
set_level Uf.src
Expand All @@ -303,11 +285,6 @@ module Debug = struct
| Use ->
Options.set_debug_use true;
set_level Use.src
| Warnings ->
Printer.print_wrn
"The debug flag 'warning' is deprecated and will be removed in a \
future version.";
Options.set_debug_warnings true
| Commands ->
Options.set_debug_commands true;
set_level Commands.src
Expand Down Expand Up @@ -442,7 +419,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
`Ok()

let mk_output_opt
interpretation use_underscore objectives_in_interpretation unsat_core
interpretation objectives_in_interpretation unsat_core
output_format model_type () () () ()
=
set_infer_output_format (Option.is_none output_format);
Expand All @@ -455,7 +432,6 @@ let mk_output_opt
| Some v -> v
in
set_interpretation interpretation;
set_interpretation_use_underscore use_underscore;
set_objectives_in_interpretation objectives_in_interpretation;
set_unsat_core unsat_core;
set_output_format output_format;
Expand Down Expand Up @@ -529,7 +505,7 @@ let mk_term_opt disable_ites inline_lets rewriting no_term_like_pp

let mk_theory_opt () no_contracongru
no_fm no_nla no_tcp no_theory restricted tighten_vars
_use_fpa (theories)
(theories)
=
set_no_ac (not (List.exists (Theories.equal Theories.AC) theories));
set_no_fm no_fm;
Expand Down Expand Up @@ -1121,17 +1097,6 @@ let parse_output_opt =
Term.term_result' term
in

let use_underscore =
let doc = "Output \"_\" instead of fresh value in interpretation" in
let deprecated =
"this option will be removed as it does not produce a \
SMTLIB-compliant output."
in
let docv = "VAL" in
Arg.(value & flag & info
["interpretation-use-underscore";"use-underscore"]
~docv ~docs:s_models ~doc ~deprecated)
in
let objectives_in_interpretation =
let doc = " inline pretty-printing of optimized expressions in the \
model instead of a dedicated section '(objectives \
Expand Down Expand Up @@ -1190,7 +1155,7 @@ let parse_output_opt =
in

Term.(ret (const mk_output_opt $
interpretation $ use_underscore $
interpretation $
objectives_in_interpretation $ unsat_core $
output_format $ model_type $
set_dump_models $ set_dump_models_on $
Expand Down Expand Up @@ -1444,12 +1409,6 @@ let parse_theory_opt =
let doc = "Compute the best bounds for arithmetic variables." in
Arg.(value & flag & info ["tighten-vars"] ~docs ~doc) in

let use_fpa =
let doc = "Floating-point builtins are always enabled and this option has
no effect anymore. It will be removed in a future version." in
let deprecated = "this option is always enabled" in
Arg.(value & flag & info ["use-fpa"] ~docs ~doc ~deprecated) in

let theories =
let theory_enum =
Theories.all
Expand All @@ -1476,34 +1435,12 @@ let parse_theory_opt =
(Arg.doc_alts_enum theory_enum)
in
let docv = "THEORY" in
let disable_theories =
Term.(const List.concat $
Arg.(
value
& opt_all (list theory) []
& info ["disable-theory"; "disable-theories"] ~docs ~doc ~docv
))
in
let disable_adts =
let doc = "Disable Algebraic Datatypes theory. Deprecated alias for
`--disable-theories adt`." in
let deprecated = "use `--disable-theories ac` instead." in
Arg.(value & flag & info ["disable-adts"] ~docs ~doc ~deprecated)
in
let no_ac =
let doc = "Disable the AC theory of Associative and \
Commutative function symbols. Deprecated alias for
`--disable-theories ac`." in
let deprecated = "use `--disable-theories ac` instead" in
Arg.(value & flag & info ["no-ac"] ~docs ~doc ~deprecated)
in
let mk_disable_theories disable_theories disable_adts no_ac =
let open Theories in
(if disable_adts then [ ADT ] else []) @
(if no_ac then [ AC ] else []) @
disable_theories
in
Term.(const mk_disable_theories $ disable_theories $ disable_adts $ no_ac)
Term.(const List.concat $
Arg.(
value
& opt_all (list theory) []
& info ["disable-theory"; "disable-theories"] ~docs ~doc ~docv
))
in
let preludes enable_theories disable_theories =
let theories = Theories.Set.of_list Theories.default in
Expand Down Expand Up @@ -1535,7 +1472,7 @@ let parse_theory_opt =
Term.(ret (const mk_theory_opt $
inequalities_plugin $ no_contracongru $
no_fm $ no_nla $ no_tcp $ no_theory $ restricted $
tighten_vars $ use_fpa $ theories
tighten_vars $ theories
)
)

Expand Down
3 changes: 0 additions & 3 deletions src/lib/util/options.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -361,7 +361,6 @@ let get_timelimit_per_goal () = !timelimit_per_goal
let interpretation = ref INone
let strict_mode = ref false
let dump_models = ref false
let interpretation_use_underscore = ref false
let objectives_in_interpretation = ref false
let output_format = ref Native
let model_type = ref Value
Expand All @@ -371,7 +370,6 @@ let unsat_core = ref false
let set_interpretation b = interpretation := b
let set_strict_mode b = strict_mode := b
let set_dump_models b = dump_models := b
let set_interpretation_use_underscore b = interpretation_use_underscore := b
let set_objectives_in_interpretation b = objectives_in_interpretation := b
let set_output_format b = output_format := b
let set_model_type t = model_type := t
Expand Down Expand Up @@ -400,7 +398,6 @@ let get_dump_models () = !dump_models
let get_first_interpretation () = equal_mode !interpretation IFirst
let get_every_interpretation () = equal_mode !interpretation IEvery
let get_last_interpretation () = equal_mode !interpretation ILast
let get_interpretation_use_underscore () = !interpretation_use_underscore
let get_objectives_in_interpretation () = !objectives_in_interpretation
let get_output_format () = !output_format
let get_output_smtlib () =
Expand Down
9 changes: 0 additions & 9 deletions src/lib/util/options.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,10 +227,6 @@ val set_strict_mode : bool -> unit
(** [dump_models] accessible with {!val:get_dump_models}. *)
val set_dump_models : bool -> unit

(** Set [interpretation_use_underscore] accessible with
{!val:get_interpretation_use_underscore} *)
val set_interpretation_use_underscore : bool -> unit

(** Set [objectives_in_interpretation] accessible with
{!val:get_objectives_in_interpretation} *)
val set_objectives_in_interpretation : bool -> unit
Expand Down Expand Up @@ -746,11 +742,6 @@ val get_every_interpretation : unit -> bool
val get_last_interpretation : unit -> bool
(** Default to [false] *)

(** [true] if the interpretation_use_underscore is set to output _
instead of fresh values *)
val get_interpretation_use_underscore : unit -> bool
(** Default to [false] *)

(** [true] if the objectives_in_interpretation is set to inline
pretty-printing of optimized expressions in the model instead of a
dedicated section '(objectives ...)'. Be aware that the model may
Expand Down

0 comments on commit 5ee6ed2

Please sign in to comment.