Rename interpretation option values to None First Last and Every

src/bin/common/parse_command.ml

@@ -60,19 +60,17 @@ 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))
 
 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)

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

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

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 _