Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove get_first_interpretation adn get_every_interpretation #1299

Merged
merged 3 commits into from
Feb 19, 2025
Merged

Remove get_first_interpretation adn get_every_interpretation #1299

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
8854efc
Remove get_first_interpretation adn get_every_interpretation
Halbaroth Feb 19, 2025
d4b42fe
review changes
Halbaroth Feb 19, 2025
38d3930
Remove the options in the js worker
Halbaroth Feb 19, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 16 additions & 30 deletions src/bin/common/parse_command.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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;
Expand Down Expand Up @@ -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 =
Expand Down Expand Up @@ -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
Expand Down
12 changes: 6 additions & 6 deletions src/bin/common/solving_loop.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 ())
"@[<v 0>Returned unknown reason = %a@]"
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down
25 changes: 8 additions & 17 deletions src/lib/reasoners/fun_sat.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand All @@ -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_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 *)
Expand All @@ -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) =
Expand Down Expand Up @@ -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
Expand All @@ -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 ();
Expand Down
44 changes: 17 additions & 27 deletions src/lib/reasoners/satml_frontend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe this line was removed because if we raise I_dont_know here the solver ends up in an inconsistent state and performing further commands can lead to incorrect output or crashes — is there a reason to add it back?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On next, if Timeout is raised during model generation, we catch it in unsat_rec and raise I_dont_know with Timeout ProofSearch as unknown reason, so the solver already ends up in an inconsistent state.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, that is true — we actually check for timeout outside of the solver, from the frontend (which is a design wart we should fix someday, but it does mean this line is OK).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added it because you pointed out that we cannot change the unknown reason as suggested by Steven. I don't understand what is wrong here.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

uhm, I see. It is because of the lazy value again...


exception Give_up of (E.t * E.t * bool * bool) list

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
20 changes: 3 additions & 17 deletions src/lib/util/options.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ]
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 () =
Expand Down
51 changes: 4 additions & 47 deletions src/lib/util/options.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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. *)
Expand All @@ -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
Expand Down
Loading