From 76deb5aa104cd147ca9f245e94be520e361fbbfb Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 19 Feb 2025 17:59:07 +0100 Subject: [PATCH] Remove get_first_interpretation adn get_every_interpretation (#1299) * Remove get_first_interpretation and get_every_interpretation options 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 | 46 +++++++++----------------- src/bin/common/solving_loop.ml | 12 +++---- src/bin/js/options_interface.ml | 11 ------- src/bin/js/worker_example.ml | 1 - src/bin/js/worker_interface.ml | 35 +------------------- src/bin/js/worker_interface.mli | 4 --- src/lib/reasoners/fun_sat.ml | 25 +++++--------- src/lib/reasoners/satml_frontend.ml | 44 ++++++++++--------------- src/lib/util/options.ml | 20 ++--------- src/lib/util/options.mli | 51 +++-------------------------- 10 files changed, 55 insertions(+), 194 deletions(-) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index c43b2a58c..a914eb21b 100644 --- a/src/bin/common/parse_command.ml +++ b/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 + produce_models 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_produce_models produce_models; 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 has 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,12 @@ 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_produce_models _interpretation produce_models dump_models = + produce_models || dump_models in Term.( - const mk_interpretation $ interpretation $ - produce_models $ dump_models - ), + const mk_produce_models $ interpretation $ produce_models + $ dump_models), dump_models, dump_models_on, frontend diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index bb752d681..4fd6bcf00 100644 --- a/src/bin/common/solving_loop.ml +++ b/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_produce_models () && 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_produce_models () && get_dump_models ()) then begin let ur = SAT.get_unknown_reason partial_model in Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) "@[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_produce_models true; st | ":produce-models", Symbol { name = Simple "false"; _ } -> - Options.set_interpretation INone; + Options.set_produce_models 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_produce_models () 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_produce_models () then let () = match State.get partial_model_key st with | Some (Model ((module SAT), env)) -> let module FE = Frontend.Make (SAT) in diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index afaeafb70..9d9f5321a 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -66,14 +66,6 @@ let get_instantiation_heuristic = function | IAuto -> Some Options.IAuto | IGreedy -> Some Options.IGreedy -let get_interpretation = function - | None -> None - | Some m -> match m with - | INone -> Some Options.INone - | IFirst -> Some Options.IFirst - | IEvery -> Some Options.IEvery - | ILast -> Some Options.ILast - let get_no_decisions_on = function | None -> None | Some l -> @@ -140,9 +132,6 @@ let set_options r = set_options_opt Options.set_fm_cross_limit (get_numbers r.fm_cross_limit); set_options_opt Options.set_steps_bound r.steps_bound; - set_options_opt Options.set_interpretation - (get_interpretation r.interpretation); - set_options_opt Options.set_output_format (get_output_format r.output_format); Options.set_infer_output_format diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml index 6b425f006..75b67c1b7 100644 --- a/src/bin/js/worker_example.ml +++ b/src/bin/js/worker_example.ml @@ -68,7 +68,6 @@ let solve () = debug = Some true; verbose = Some true; answers_with_loc = Some false; - interpretation = Some IEvery; sat_solver = Some Worker_interface.Tableaux; unsat_core = Some true; } in diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 80bf9178c..f20c03286 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -112,7 +112,6 @@ let sat_solver_encoding = ] type instantiation_heuristic = INormal | IAuto | IGreedy -type interpretation = INone | IFirst | IEvery | ILast let instantiation_heuristic_encoding = union [ @@ -133,30 +132,6 @@ let instantiation_heuristic_encoding = (fun () -> IGreedy); ] -let interpretation_encoding = - union [ - case(Tag 1) - ~title:"INone" - (constant "INone") - (function INone -> Some () | _ -> None) - (fun () -> INone); - case(Tag 2) - ~title:"IFirst" - (constant "IFirst") - (function IFirst -> Some () | _ -> None) - (fun () -> IFirst); - case(Tag 3) - ~title:"IEvery" - (constant "IEvery") - (function IEvery -> Some () | _ -> None) - (fun () -> IEvery); - case(Tag 4) - ~title:"ILast" - (constant "ILast") - (function ILast -> Some () | _ -> None) - (fun () -> ILast); - ] - type options = { debug : bool option; debug_ac : bool option; @@ -206,8 +181,6 @@ type options = { fm_cross_limit : int option; steps_bound : int option; - interpretation : interpretation option; - output_format : output_format option; unsat_core : bool option; @@ -303,8 +276,6 @@ let init_options () = { fm_cross_limit = None; steps_bound = None; - interpretation = None; - output_format = None; unsat_core = None; @@ -428,13 +399,12 @@ let opt3_encoding = conv (fun opt3 -> opt3) (fun opt3 -> opt3) - (obj8 + (obj7 (opt "disable_weaks" bool) (opt "enable_assertions" bool) (opt "age_bound" int31) (opt "fm_cross_limit" int31) (opt "steps_bound" int31) - (opt "interpretation" interpretation_encoding) (opt "output_format" format_encoding) (opt "unsat_core" bool) ) @@ -569,7 +539,6 @@ let options_to_json opt = opt.age_bound, opt.fm_cross_limit, opt.steps_bound, - opt.interpretation, opt.output_format, opt.unsat_core) in @@ -687,7 +656,6 @@ let options_from_json options = age_bound, fm_cross_limit, steps_bound, - interpretation, output_format, unsat_core) = all_opt3 in let (verbose, @@ -769,7 +737,6 @@ let options_from_json options = age_bound; fm_cross_limit; steps_bound; - interpretation; output_format; unsat_core; verbose; diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index c10118e47..0d7ff895c 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -50,8 +50,6 @@ type sat_solver = type instantiation_heuristic = INormal | IAuto | IGreedy -type interpretation = INone | IFirst | IEvery | ILast - (** Record type that contains all options that can be set for the Alt-Ergo's worker. *) type options = { @@ -103,8 +101,6 @@ type options = { fm_cross_limit : int option; steps_bound : int option; - interpretation : interpretation option; - output_format : output_format option; unsat_core : bool option; diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 347ef6cc4..88c845c54 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/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_produce_models () then env else begin try (* also performs case-split and pushes pending atoms to CS *) @@ -1142,9 +1138,9 @@ 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) -> @@ -1152,7 +1148,7 @@ module Make (Th : Theory.S) = struct i_dont_know env (Timeout ModelGen) let model_gen_on_timeout env = - let i = Options.get_interpretation () in + let i = Options.get_produce_models () 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 (); diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 4691c7ce7..773efe1a2 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1000,28 +1000,18 @@ 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 + | Util.Timeout -> i_dont_know env (Timeout ModelGen) exception Give_up of (E.t * E.t * bool * bool) list @@ -1169,7 +1159,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 +1187,11 @@ 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_produce_models () then update_model env; + Options.Time.unset_timeout (); + i_dont_know env Incomplete + ); unsat_rec env ~first_call:false with diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 761a4b943..081b1e501 100644 --- a/src/lib/util/options.ml +++ b/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 produce_models = 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_produce_models b = produce_models := 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_produce_models () = !produce_models 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 () = diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index f67d8e76a..c0d9754d0 100644 --- a/src/lib/util/options.mli +++ b/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_produce_models : 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_produce_models : 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