Remove get_first_interpretation adn get_every_interpretation

As noticed by Basile, this feature is broken in presence of optimization
and no one used it. This PR removes these options.

I kept the cli option but it is now a no-op.

src/bin/common/parse_command.ml

@@ -423,7 +423,7 @@ let mk_limit_opt age_bound fm_cross_limit timelimit_interpretation
     `Ok()
 
 let mk_output_opt
-    interpretation objectives_in_interpretation unsat_core
+    model_generation objectives_in_interpretation unsat_core
     output_format model_type () () () ()
   =
   set_infer_output_format (Option.is_none output_format);
@@ -435,7 +435,7 @@ let mk_output_opt
     | None -> Value
     | Some v -> v
   in
-  set_interpretation interpretation;
+  set_model_generation model_generation;
   set_objectives_in_interpretation objectives_in_interpretation;
   set_unsat_core unsat_core;
   set_output_format output_format;
@@ -912,28 +912,17 @@ let parse_output_opt =
      --interpretation last) to determine the interpretation value. *)
   let interpretation, dump_models, dump_models_on, frontend =
     let interpretation =
-      let doc = Format.sprintf
-          "Best effort support for counter-example generation. \
-           $(docv) must be %s. %s shows the first computed interpretation. \
-           %s compute an interpretation before every decision, \
-           and %s only before returning unknown. \
-           Note that $(b, --max-split) limitation will \
-           be ignored in model generation phase."
-          (Arg.doc_alts
-             ["none"; "first"; "every"; "last"])
-          (Arg.doc_quote "first") (Arg.doc_quote "every")
-          (Arg.doc_quote "last") in
-      let docv = "VAL" in
-      let interpretation =
-        Arg.enum
-          [ "none", INone
-          ; "first", IFirst
-          ; "every", IEvery
-          ; "last", ILast
-          ]
+      let doc =
+        Fmt.str
+          "This option allowed choosing when the model generation occurs. \
+           It have been removed in Alt-Ergo 2.7.0. If model generation is \
+           enabled, it is performed as the final step, which was the default \
+           in previous versions."
       in
-      Arg.(value & opt interpretation INone &
-           info ["interpretation"] ~docv ~docs:s_models ~doc)
+      let docv = "VAL" in
+      let deprecated = "this option is deprecated and is ignored." in
+      Arg.(value & opt string "dummy" &
+           info ["interpretation"] ~docv ~docs:s_models ~doc ~deprecated)
     in
     let produce_models =
       let doc =
@@ -980,15 +969,11 @@ let parse_output_opt =
            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
+    let mk_interpretation _interpretation produce_models dump_models =
+      produce_models || dump_models
     in
     Term.(
-      const mk_interpretation $ interpretation $
-      produce_models $ dump_models
-    ),
+      const mk_interpretation $ interpretation $ produce_models $ dump_models),
     dump_models,
     dump_models_on,
     frontend

src/bin/common/solving_loop.ml

@@ -209,7 +209,7 @@ let process_source ?selector_inst ~print_status src =
       | `Sat ->
         begin
           let mdl = Model ((module SAT), partial_model) in
-          if Options.(get_interpretation () && get_dump_models ()) then begin
+          if Options.(get_model_generation () && get_dump_models ()) then begin
             Fmt.pf (Options.Output.get_fmt_models ()) "%a@."
               FE.print_model partial_model
           end;
@@ -218,7 +218,7 @@ let process_source ?selector_inst ~print_status src =
       | `Unknown ->
         begin
           let mdl = Model ((module SAT), partial_model) in
-          if Options.(get_interpretation () && get_dump_models ()) then begin
+          if Options.(get_model_generation () && get_dump_models ()) then begin
             let ur = SAT.get_unknown_reason partial_model in
             Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
               "@[<v 0>Returned unknown reason = %a@]"
@@ -430,10 +430,10 @@ let process_source ?selector_inst ~print_status src =
       |> Options.Output.set_diagnostic;
       st
     | ":produce-models", Symbol { name = Simple "true"; _ } ->
-      Options.set_interpretation ILast;
+      Options.set_model_generation true;
       st
     | ":produce-models", Symbol { name = Simple "false"; _ } ->
-      Options.set_interpretation INone;
+      Options.set_model_generation false;
       st
     | ":produce-unsat-cores", Symbol { name = Simple "true"; _ } ->
       (* The generation of unsat core is supported only with the SAT
@@ -572,7 +572,7 @@ let process_source ?selector_inst ~print_status src =
   let handle_get_objectives ~loc (_args : DStd.Expr.Term.t list) st =
     let module Sat = (val DO.SatSolverModule.get st) in
     let () =
-      if Options.get_interpretation () then
+      if Options.get_model_generation () then
         if not Sat.supports_optimization then
           recoverable_error ~loc
             "the selected solver does not support optimization"
@@ -802,7 +802,7 @@ let process_source ?selector_inst ~print_status src =
 
       | {contents = `Get_model; _ } ->
         cmd_on_modes st [Sat] "get-model";
-        if Options.get_interpretation () then
+        if Options.get_model_generation () then
           let () = match State.get partial_model_key st with
             | Some (Model ((module SAT), env)) ->
               let module FE = Frontend.Make (SAT) in

src/lib/reasoners/fun_sat.ml

@@ -1122,12 +1122,8 @@ module Make (Th : Theory.S) = struct
       ignore (update_instances_cache (Some []));
       env, true
 
-  let may_update_last_saved_model env compute =
-    let compute =
-      if not (Options.get_first_interpretation ()) then compute
-      else !(env.last_saved_model) == None
-    in
-    if not compute then env
+  let may_update_last_saved_model env =
+    if not @@ Options.get_model_generation () then env
     else begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
@@ -1142,17 +1138,17 @@ module Make (Th : Theory.S) = struct
         raise (IUnsat (expl, classes))
     end
 
-  let update_model_and_return_unknown env compute_model ~unknown_reason =
+  let update_model_and_return_unknown env ~unknown_reason =
     try
-      let env = may_update_last_saved_model env compute_model in
+      let env = may_update_last_saved_model env in
       Options.Time.unset_timeout ();
       i_dont_know env unknown_reason
     with Util.Timeout when !(env.model_gen_phase) ->
       (* In this case, timeout reason becomes 'ModelGen' *)
       i_dont_know env (Timeout ModelGen)
 
   let model_gen_on_timeout env =
-    let i = Options.get_interpretation () in
+    let i = Options.get_model_generation () in
     let ti = Options.get_timelimit_interpretation () in
     if not i || (* not asked to gen a model *)
        !(env.model_gen_phase) ||  (* we timeouted in model-gen-phase *)
@@ -1168,7 +1164,7 @@ module Make (Th : Theory.S) = struct
         Options.Time.unset_timeout ();
         Options.Time.set_timeout ti;
         update_model_and_return_unknown
-          env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *)
+          env ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *)
       end
 
   let reduce_hypotheses tcp_cache tmp_cache env acc (hyp, gf, dep) =
@@ -1279,8 +1275,7 @@ module Make (Th : Theory.S) = struct
     | INormal ->
       (* TODO: check if this test still produces a wrong model. *)
       update_model_and_return_unknown
-        env (Options.get_last_interpretation ())
-        ~unknown_reason:Incomplete (* may becomes ModelGen *)
+        env ~unknown_reason:Incomplete (* may becomes ModelGen *)
     | IAuto | IGreedy ->
       let gre_inst =
         ME.fold
@@ -1307,15 +1302,11 @@ module Make (Th : Theory.S) = struct
       if ok1 || ok2 || ok3 || ok4 then env
       else
         update_model_and_return_unknown
-          env (Options.get_last_interpretation ())
-          ~unknown_reason:Incomplete (* may becomes ModelGen *)
+          env ~unknown_reason:Incomplete (* may becomes ModelGen *)
 
   let normal_instantiation env try_greedy =
     Debug.print_nb_related env;
     let env = do_case_split env Util.BeforeMatching in
-    let env =
-      may_update_last_saved_model env (Options.get_every_interpretation ())
-    in
     let env = new_inst_level env in
     let mconf =
       {Util.nb_triggers = Options.get_nb_triggers ();

src/lib/reasoners/satml_frontend.ml

@@ -1000,28 +1000,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | C_bool _ -> assert false
     | C_theory expl -> raise (Ex.Inconsistent (expl, []))
 
-  let may_update_last_saved_model env compute =
-    let compute =
-      if not (Options.get_first_interpretation ()) then compute
-      else env.last_saved_model == None
-    in
-    if compute then begin
-      try
-        (* also performs case-split and pushes pending atoms to CS *)
-        let declared_ids = env.declare_top in
-        let model, objectives =
-          SAT.compute_concrete_model ~declared_ids env.satml
-        in
-        env.last_saved_model <- Some model;
-        env.last_saved_objectives <- Some objectives;
-      with Ex.Inconsistent (_expl, _classes) as e ->
-        raise e
-    end
-
-  let update_model_and_return_unknown env compute_model ~unknown_reason =
-    may_update_last_saved_model env compute_model;
-    Options.Time.unset_timeout ();
-    i_dont_know env unknown_reason
+  let update_model env =
+    try
+      (* also performs case-split and pushes pending atoms to CS *)
+      let declared_ids = env.declare_top in
+      let model, objectives =
+        SAT.compute_concrete_model ~declared_ids env.satml
+      in
+      env.last_saved_model <- Some model;
+      env.last_saved_objectives <- Some objectives;
+    with Ex.Inconsistent (_expl, _classes) as e ->
+      raise e
 
   exception Give_up of (E.t * E.t * bool * bool) list
 
@@ -1169,7 +1158,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | Satml.Sat ->
       try
         do_case_split env Util.BeforeMatching;
-        may_update_last_saved_model env (Options.get_every_interpretation ());
         let () =
           env.nb_mrounds <- env.nb_mrounds + 1
                             [@ocaml.ppwarning
@@ -1198,10 +1186,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
                instantiation doesn't allow to backjump *)
             env.last_forced_normal <- env.last_forced_normal - 1
         in
-        if not updated then
-          update_model_and_return_unknown
-            env (Options.get_last_interpretation ())
-            ~unknown_reason:Incomplete; (* may becomes ModelGen *)
+        if not updated then (
+          if Options.get_model_generation () then update_model env;
+          Options.Time.unset_timeout ();
+          (* may becomes ModelGen *)
+          i_dont_know env Incomplete
+        );
         unsat_rec env ~first_call:false
 
       with

src/lib/util/options.ml

@@ -109,7 +109,6 @@ end
 (* Declaration of all the options as refs with default values *)
 
 type instantiation_heuristic = INormal | IAuto | IGreedy
-type interpretation = INone | IFirst | IEvery | ILast
 
 (* As in Dolmen *)
 type smtlib2_version = [ `Latest | `V2_6 | `Poly ]
@@ -355,7 +354,7 @@ let get_timelimit_per_goal () = !timelimit_per_goal
 
 (** Output options *)
 
-let interpretation = ref INone
+let model_generation = ref false
 let strict_mode = ref false
 let dump_models = ref false
 let objectives_in_interpretation = ref false
@@ -364,7 +363,7 @@ let model_type = ref Value
 let infer_output_format = ref true
 let unsat_core = ref false
 
-let set_interpretation b = interpretation := b
+let set_model_generation b = model_generation := b
 let set_strict_mode b = strict_mode := b
 let set_dump_models b = dump_models := b
 let set_objectives_in_interpretation b = objectives_in_interpretation := b
@@ -373,28 +372,15 @@ let set_model_type t = model_type := t
 let set_infer_output_format b = infer_output_format := b
 let set_unsat_core b = unsat_core := b
 
-let equal_mode a b =
-  match a, b with
-  | INone, INone -> true
-  | INone, _ | _, INone -> false
-  | IFirst, IFirst -> true
-  | IFirst, _ | _, IFirst -> false
-  | IEvery, IEvery -> true
-  | IEvery, _ | _, IEvery -> false
-  | ILast, ILast -> true
-
 let equal_mode_type a b =
   match a, b with
   | Constraints, Constraints -> true
   | Constraints, _ | _, Constraints -> false
   | Value, Value -> true
 
-let get_interpretation () = not @@ equal_mode !interpretation INone
+let get_model_generation () = !model_generation
 let get_strict_mode () = !strict_mode
 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_objectives_in_interpretation () = !objectives_in_interpretation
 let get_output_format () = !output_format
 let get_output_smtlib () =

src/lib/util/options.mli

@@ -44,17 +44,6 @@ type instantiation_heuristic =
   | IGreedy      (** Force instantiation to be the greedier as possible,
                      use all available ground terms *)
 
-(** Type used to describe the type of interpretation wanted by
-    {!val:set_interpretation} *)
-type interpretation =
-  | INone        (** Default, No interpretation computed *)
-  | IFirst       (** Compute an interpretation after the first instantiation
-                     and output it at the end of the executionn *)
-  | IEvery       (** Compute an interpretation before every instantiation
-                     and return the last one computed *)
-  | ILast        (** Compute only the last interpretation just before
-                     returning SAT/Unknown *)
-
 type smtlib2_version =
   [ `Latest
   (** Latest version of the SMT-LIB standard. *)
@@ -209,14 +198,8 @@ val set_inline_lets : bool -> unit
 (** Set [input_format] accessible with {!val:get_input_format} *)
 val set_input_format : input_format option -> unit
 
-(** Set [interpretation] accessible with {!val:get_interpretation}
-
-    Possible values are :
-    {ol {- First} {- Before every instantiation}
-     {- Before every decision and instantiation}
-     {- Before end}}
-*)
-val set_interpretation : interpretation -> unit
+(** Set [produce_models] accessible with {!val:get_produce_models} *)
+val set_model_generation : bool -> unit
 
 (** Set [strict_mode] accessible with {!val:get_strict_mode}. *)
 val set_strict_mode : bool -> unit
@@ -695,20 +678,8 @@ val get_timelimit_per_goal : unit -> bool
 
 (** {4 Output options} *)
 
-(** Experimental support for counter-example generation.
-
-    Possible values are :
-     {ol {- First} {- Before every instantiation}
-      {- Before every decision and instantiation}
-      {- Before end}}
-
-    Which are used in the four getters below. This option answers
-    [true] if the interpretation is set to First, Before_end, Before_dec
-    or Before_inst.
-
-    Note that {!val:get_max_split} limitation will be ignored in model
-    generation phase. *)
-val get_interpretation : unit -> bool
+(** [true] if model generation is enabled. *)
+val get_model_generation : unit -> bool
 (** Default to [false] *)
 
 (** [true] if strict mode is enabled. *)
@@ -719,20 +690,6 @@ val get_strict_mode : unit -> bool
 val get_dump_models : unit -> bool
 (** Default to [false]. *)
 
-(** [true] if the interpretation is set to first interpretation *)
-val get_first_interpretation : unit -> bool
-(** Default to [false] *)
-
-(** [true] if the interpretation is set to compute interpretation
-    before every instantiation *)
-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_last_interpretation : 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