From 202c7684c4396cf1713b0ca722e1707fbc76a426 Mon Sep 17 00:00:00 2001 From: Albin Coquereau Date: Wed, 23 Dec 2020 10:56:40 +0100 Subject: [PATCH] Rename interpretation option values to None First Last and Every --- src/bin/common/parse_command.ml | 10 ++++------ src/lib/reasoners/fun_sat.ml | 7 +++---- src/lib/util/options.ml | 13 ++++--------- src/lib/util/options.mli | 11 +++-------- 4 files changed, 14 insertions(+), 27 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 7d6b79a71..97a3d8a88 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -60,9 +60,8 @@ let instantiation_heuristic_conv = let interpretation_parser = function | "none" -> Ok INone | "first" -> Ok IFirst - | "before_inst" -> Ok IBefore_inst - | "before_dec" -> Ok IBefore_dec - | "before_end" -> Ok IBefore_end + | "every" -> Ok IEvery + | "last" -> Ok ILast | s -> Error (`Msg ("Option --interpretation does not accept the argument \"" ^ s)) @@ -70,9 +69,8 @@ let interpretation_parser = function let interpretation_to_string = function | INone -> "none" | IFirst -> "first" - | IBefore_inst -> "before_inst" - | IBefore_dec -> "before_dec" - | IBefore_end -> "before_end" + | IEvery -> "every" + | ILast -> "last" let interpretation_printer fmt interpretation = Format.fprintf fmt "%s" (interpretation_to_string interpretation) diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 8c0df707d..e00ad1161 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1400,7 +1400,7 @@ are not Th-reduced"; let greedy_instantiation env = match get_instantiation_heuristic () with | INormal -> - return_answer env (get_before_end_interpretation ()) + return_answer env (get_last_interpretation ()) (fun e -> raise (I_dont_know e)) | IAuto | IGreedy -> let gre_inst = @@ -1427,14 +1427,14 @@ are not Th-reduced"; let env = do_case_split env Util.AfterMatching in if ok1 || ok2 || ok3 || ok4 then env else - return_answer env (get_before_end_interpretation ()) + return_answer env (get_last_interpretation ()) (fun e -> raise (I_dont_know e)) let normal_instantiation env try_greedy = Debug.print_nb_related env; let env = do_case_split env Util.BeforeMatching in - let env = compute_concrete_model env (get_before_inst_interpretation ()) in + let env = compute_concrete_model env (get_every_interpretation ()) in let env = new_inst_level env in let mconf = {Util.nb_triggers = get_nb_triggers (); @@ -1528,7 +1528,6 @@ are not Th-reduced"; and back_tracking env = try - let env = compute_concrete_model env (get_before_dec_interpretation ()) in if env.delta == [] || Options.get_no_decisions() then back_tracking (normal_instantiation env true) else diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 26528fbbc..960b3a823 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -63,7 +63,7 @@ let set_fmt_usc f = fmt_usc := f type model = MNone | MDefault | MAll | MComplete type instantiation_heuristic = INormal | IAuto | IGreedy -type interpretation = INone | IFirst | IBefore_inst | IBefore_dec | IBefore_end +type interpretation = INone | IFirst | IEvery | ILast type input_format = Native | Smtlib2 | Why3 (* | SZS *) | Unknown of string type output_format = input_format @@ -310,15 +310,10 @@ let set_output_format b = output_format := b let set_infer_output_format f = infer_output_format := f = None let set_unsat_core b = unsat_core := b -let get_interpretation () = - !interpretation = IFirst || - !interpretation = IBefore_dec || - !interpretation = IBefore_inst || - !interpretation = IBefore_end +let get_interpretation () = !interpretation <> INone let get_first_interpretation () = !interpretation = IFirst -let get_before_dec_interpretation () = !interpretation = IBefore_dec -let get_before_inst_interpretation () = !interpretation = IBefore_inst -let get_before_end_interpretation () = !interpretation = IBefore_end +let get_every_interpretation () = !interpretation = IEvery +let get_last_interpretation () = !interpretation = ILast let get_interpretation_use_underscore () = !interpretation_use_underscore let get_model () = !model = MDefault || !model = MComplete let get_complete_model () = !model = MComplete diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 4cd0cf3fb..f4e0631f3 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -42,7 +42,7 @@ type model = MNone | MDefault | MAll | MComplete type instantiation_heuristic = INormal | IAuto | IGreedy (** Type used to describe the type of interpretation wanted *) -type interpretation = INone | IFirst | IBefore_inst | IBefore_dec | IBefore_end +type interpretation = INone | IFirst | IEvery | ILast (** Type used to describe the type of input wanted by {!val:set_input_format} *) @@ -716,19 +716,14 @@ val get_interpretation : unit -> bool val get_first_interpretation : unit -> bool (** Default to [false] *) -(** [true] if the interpretation is set to compute interpretation - before every decision *) -val get_before_dec_interpretation : unit -> bool -(** Default to [false] *) - (** [true] if the interpretation is set to compute interpretation before every instantiation *) -val get_before_inst_interpretation : unit -> bool +val get_every_interpretation : unit -> bool (** Default to [false] *) (** [true] if the interpretation is set to compute interpretation before the solver return unknown *) -val get_before_end_interpretation : unit -> bool +val get_last_interpretation : unit -> bool (** Default to [false] *) (** [true] if the interpretation_use_underscore is set to output _