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

Fix timeout #982

Merged
merged 4 commits into from
Nov 28, 2023
Merged

Fix timeout #982

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6104473
Reactivating timeouts
Stevendeo Nov 27, 2023
d9e3482
Removing model generation when timeout on satml
Stevendeo Nov 27, 2023
aefb37b
Processing timeout on the binary side
Stevendeo Nov 27, 2023
0ce1664
Poetry
Stevendeo Nov 28, 2023
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
11 changes: 10 additions & 1 deletion src/bin/common/solving_loop.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -137,9 +137,16 @@ let main () =
end;
SAT.reset_refs ();
let ftdn_env = FE.init_env used_context in
let hook_on_status status i =
Frontend.print_status status i;
match status with
| Timeout _ when not (Options.get_timelimit_per_goal ()) ->
exit_as_timeout ()
| _ -> ()
Comment on lines +141 to +145
Copy link
Collaborator

Choose a reason for hiding this comment

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

Just a thought: wondering if we should call Frontend.print_status at all when we call exit_as_timeout, since it leads to slightly weird output:

unknown
(error "timeout")

Maybe just (error "timeout") (or even timeout as we used to do; it is not a standard SMT-LIB response, but it is used by Z3 and hence parsed by many tools, including Why3 — and since we don't support unknown-reason with the "hard" timeout that would be easier for them to get the information out).

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 am in favor of either the current solution (unknown + error) or the timeout only, but I have a preference for the first one because it matches the standard

Copy link
Collaborator

Choose a reason for hiding this comment

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

My understanding is that the current behavior is actually not standard-compliant because we give two responses to a (check-sat) command where the standard only expects (at most; success can be skipped) one response per command.

(In any case, this is unrelated to this PR)

Copy link
Collaborator Author

@Stevendeo Stevendeo Nov 28, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

Error handling is quite generic in the smtlib reference:

An expression of the form (error e) should be returned for any kind of error situation 
(wrong command syntax, incorrect parameters, erroneous execution, and so on).

Copy link
Collaborator

Choose a reason for hiding this comment

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

I understand this as being a particular case of:

Generally, once a solver completes its processing in response to a command, it should print to its regular output channel a 〈general_response〉

But it doesn't really matter; tools can process either output anyway (I had a glance at Why3's code for the SMT variant of Alt-Ergo and it looks like they currently don't parse timeouts at all there, so eh).

in
let () =
List.iter
(FE.process_decl ~hook_on_status:Frontend.print_status ftdn_env)
(FE.process_decl ~hook_on_status ftdn_env)
cnf
in
if Options.get_timelimit_per_goal() then
Expand Down Expand Up @@ -167,6 +174,8 @@ let main () =
end
| `Unsat -> None
with Util.Timeout ->
(* It is still necessary to leave this catch here, because we may
trigger this exception in between calls of the sat solver. *)
if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
None
in
Expand Down
20 changes: 11 additions & 9 deletions src/lib/frontend/frontend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -396,9 +396,11 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
env.expl <- expl
| `Unsat -> ()

let check_step_limit f env =
(** Checks whether the env can be used before actually calling the
function. *)
let check_if_over f env =
match SAT.get_unknown_reason env.sat_env with
| Some (Step_limit _) -> ()
| Some (Step_limit _ | Timeout _) -> ()
| _ -> f env

let handle_sat_exn f ?loc x env =
Expand All @@ -415,7 +417,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
don't do anything), and then calls the function & catches the
exceptions. *)
let wrap_f f ?loc x env =
check_step_limit (handle_sat_exn f ?loc x) env
check_if_over (handle_sat_exn f ?loc x) env

let push = wrap_f internal_push

Expand All @@ -432,19 +434,19 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
try
match d.st_decl with
| Push n -> check_step_limit (internal_push ~loc:d.st_loc n) env
| Pop n -> check_step_limit (internal_pop ~loc:d.st_loc n) env
| Push n -> check_if_over (internal_push ~loc:d.st_loc n) env
| Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env
| Assume (n, f, mf) ->
check_step_limit (internal_assume ~loc:d.st_loc (n, f, mf)) env
check_if_over (internal_assume ~loc:d.st_loc (n, f, mf)) env
| PredDef (f, name) ->
check_step_limit (internal_pred_def ~loc:d.st_loc (name, f)) env
check_if_over (internal_pred_def ~loc:d.st_loc (name, f)) env
| RwtDef _ -> assert false
| Query (n, f, sort) ->
begin
(* If we have reached an unknown state, we can return it right
away. *)
match SAT.get_unknown_reason env.sat_env with
| Some (Step_limit _) -> raise SAT.I_dont_know
| Some (Step_limit _ | Timeout _) -> raise SAT.I_dont_know
| Some _ ->
(* For now, only the step limit is an unknown step reachable
here. We could raise SAT.I_dont_know as in the previous case,
Expand All @@ -458,7 +460,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
| _ -> assert false
end
| ThAssume th_elt ->
check_step_limit (internal_th_assume ~loc:d.st_loc th_elt) env
check_if_over (internal_th_assume ~loc:d.st_loc th_elt) env
with
| SAT.Sat ->
(* This case should mainly occur when a query has a non-unsat result,
Expand Down
56 changes: 9 additions & 47 deletions src/lib/reasoners/satml_frontend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
add_inst : E.t -> bool;
guards : guards;
mutable last_saved_model : Models.t Lazy.t option;
mutable model_gen_phase : bool;
mutable unknown_reason : Sat_solver_sig.unknown_reason option;
(** The reason why satml raised [I_dont_know] if it does; [None] by
default. *)
Expand Down Expand Up @@ -95,7 +94,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
guards = init_guards ();
add_inst = (fun _ -> true);
last_saved_model = None;
model_gen_phase = false;
unknown_reason = None;
objectives = None
}
Expand Down Expand Up @@ -997,36 +995,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
end

let update_model_and_return_unknown env compute_model ~unknown_reason =
try
may_update_last_saved_model env compute_model;
Options.Time.unset_timeout ();
i_dont_know env unknown_reason
(* Timeout -> I_dont_know conversions temporarily disabled
https://github.com/OCamlPro/alt-ergo/issues/946 *)
with Util.Timeout when env.model_gen_phase && false ->
(* In this case, timeout reason becomes 'ModelGen' *)
i_dont_know env (Timeout ModelGen)

(* WARNING: temporary unused after the PR #950. *)
(* let model_gen_on_timeout env =
let i = Options.get_interpretation () 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 *)
Stdlib.(=) ti 0. (* no time allocated for extra model search *)
then
i_dont_know env (Timeout ProofSearch)
else
begin
(* Beware: models generated on timeout of ProofSearch phase may
be incoherent wrt. the ground part of the pb (ie. if delta
is not empty ? *)
env.model_gen_phase := true;
Options.Time.unset_timeout ();
Options.Time.set_timeout ti;
update_model_and_return_unknown
env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *)
end *)
may_update_last_saved_model env compute_model;
Options.Time.unset_timeout ();
i_dont_know env unknown_reason

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

Expand Down Expand Up @@ -1143,9 +1114,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
try SAT.solve env.satml; assert false
with
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
(* Timeout -> I_dont_know conversions temporarily disabled
https://github.com/OCamlPro/alt-ergo/issues/946 *)
(* | Util.Timeout -> model_gen_on_timeout env *)
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Satml.Sat ->
try
do_case_split env Util.BeforeMatching;
Expand Down Expand Up @@ -1185,9 +1154,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
unsat_rec env ~first_call:false

with
(* Timeout -> I_dont_know conversions temporarily disabled
https://github.com/OCamlPro/alt-ergo/issues/946 *)
(* | Util.Timeout -> model_gen_on_timeout env *)
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
| Ex.Inconsistent (expl, _cls) -> (*may be raised during matching or CS*)
begin
Expand All @@ -1196,9 +1163,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
unsat_rec env ~first_call:false
with
| Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
(* Timeout -> I_dont_know conversions temporarily disabled
https://github.com/OCamlPro/alt-ergo/issues/946 *)
(* | Util.Timeout -> model_gen_on_timeout env *)
| Util.Timeout -> i_dont_know env (Timeout ProofSearch)
end

let rec unsat_rec_prem env ~first_call : unit =
Expand Down Expand Up @@ -1285,7 +1250,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
assert (not (Stack.is_empty env.guards.stack_guard));
let b = Stack.top env.guards.stack_guard in
Steps.pop_steps ();
env.model_gen_phase <- false;
env.last_saved_model <- None;
env.inst <- inst;
env.guards.current_guard <- b
Expand Down Expand Up @@ -1337,12 +1301,10 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
assert (SAT.decision_level env.satml == 0);
try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf])
with | IUnsat (_env, dep) -> raise (Unsat dep)
(* Timeout -> I_dont_know conversions temporarily disabled
https://github.com/OCamlPro/alt-ergo/issues/946 *)
(* | Util.Timeout ->
(* don't attempt to compute a model if timeout before
| Util.Timeout ->
(* don't attempt to compute a model if timeout before
calling unsat function *)
i_dont_know env (Timeout Assume) *)
i_dont_know env (Timeout Assume)
| Util.Step_limit_reached n ->
(* When reaching the step limit on an assume, we do not want to
answer 'unknown' right away. *)
Expand Down
Loading