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

Jump to bottom

Bubble printing model #932

Merged
merged 6 commits into from
Nov 17, 2023
Merged

Bubble printing model #932

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f934b75
Bubbling the model printing in the binary
Halbaroth Nov 14, 2023
c8e4fa1
Update the JS worker
Halbaroth Nov 14, 2023
dbfed1b
Save a timeout reason in the exception Util.Timeout
Halbaroth Nov 14, 2023
29c3841
Revert "Save a timeout reason in the exception Util.Timeout"
Halbaroth Nov 14, 2023
9cc2fd6
Review changes
Halbaroth Nov 14, 2023
1b77978
Factorizing `print_model`
Halbaroth Nov 17, 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
53 changes: 33 additions & 20 deletions src/bin/common/solving_loop.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,23 @@ let main () =
O.get_sat_solver (),
(module SatCont.Make(TH) : Sat_solver_sig.S)
in

let print_model ppf (Model ((module SAT), env)) =
let ur = SAT.get_unknown_reason env in
Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
"@[<v 0>; Returned unknown reason = %a@]"
Copy link
Collaborator

Choose a reason for hiding this comment

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

There shouldn't be ; comments on the diagnostic channel.

Sat_solver_sig.pp_unknown_reason_opt ur;
match SAT.get_model env with
| None ->
Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
"@[<v 0>It seems that no model has been computed so \
bclement-ocp marked this conversation as resolved.
Show resolved Hide resolved
far. You may need to change your model generation strategy \
or to increase your timeouts."
Copy link
Collaborator

Choose a reason for hiding this comment

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

Why change the error message?

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 didn't change it but I print the timeout reason just before. Now, if we don't print always the unknown reason while outputting the model, it makes sense to keep print it if we fail to produce a model here.


| Some (lazy model) ->
Models.output_concrete_model ppf model
in

let solve (module SAT : Sat_solver_sig.S) all_context (cnf, goal_name) =
let module FE = Frontend.Make (SAT) in
if Options.get_debug_commands () then
Expand Down Expand Up @@ -186,7 +203,12 @@ let main () =
printing wrong model. *)
match ftdn_env.FE.res with
| `Sat partial_model | `Unknown partial_model ->
Some (Model ((module SAT), partial_model))
begin
let mdl = Model ((module SAT), partial_model) in
if Options.(get_interpretation () && get_dump_models ()) then
print_model (Options.Output.get_fmt_models ()) mdl;
Some mdl
end
| `Unsat -> None
with Util.Timeout ->
if not (Options.get_timelimit_per_goal()) then exit_as_timeout ();
Expand Down Expand Up @@ -675,10 +697,8 @@ let main () =
| Some Model ((module SAT), sat) ->
match SAT.get_unknown_reason sat with
| None -> err ()
| Some s ->
print_std
Format.pp_print_string
(Frontend.unknown_reason_to_string s)
| Some ur ->
print_std Sat_solver_sig.pp_unknown_reason ur
in
match name with
| ":authors" ->
Expand Down Expand Up @@ -837,21 +857,14 @@ let main () =

| {contents = `Get_model; _ } ->
if Options.get_interpretation () then
match State.get partial_model_key st with
| Some Model ((module SAT), partial_model) ->
begin
match SAT.get_model partial_model with
| Some (lazy model) ->
Models.output_concrete_model
(Options.Output.get_fmt_regular ()) model;
st
| _ ->
(* TODO: is it reachable? *)
st
end
| None ->
(* TODO: add the location of the statement. *)
recoverable_error "No model produced."; st
let _ = match State.get partial_model_key st with
| Some model ->
print_model (Options.Output.get_fmt_regular ()) model
| None ->
(* TODO: add the location of the statement. *)
recoverable_error "No model produced."
in
st
Copy link
Collaborator

Choose a reason for hiding this comment

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

Not convinced we should print the unknown reason when we have a model, it will just be noise. If the user wants to see the unkonwn reason, they can call (get-info :unknown-reason), we shouldn't force it down their throat.

(For --dump-models I am not entirely convinced either but it kind of makes sense b/c the user has no control & it helps distinguish the intermediate models from the final models with --interpretation every, but for (get-model) there is a mechanism in place to display that information with (get-info :unknown-reason) already)

else
begin
(* TODO: add the location of the statement. *)
Expand Down
26 changes: 26 additions & 0 deletions src/bin/js/worker_js.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,22 @@ let main worker_id content =
Frontend.print_status status n
in

let print_model ppf env =
let ur = SAT.get_unknown_reason env in
Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
"@[<v 0>; Returned unknown reason = %a@]"
Sat_solver_sig.pp_unknown_reason_opt ur;
match SAT.get_model env with
| None ->
Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
"@[<v 0>It seems that no model has been computed so \
far. You may need to change your model generation strategy \
or to increase your timeouts."

| Some (lazy model) ->
Models.output_concrete_model ppf model
in

bclement-ocp marked this conversation as resolved.
Show resolved Hide resolved
let solve all_context (cnf, goal_name) =
let used_context = Frontend.choose_used_context all_context ~goal_name in
SAT.reset_refs ();
Expand All @@ -133,6 +149,16 @@ let main worker_id content =
if Options.get_unsat_core () then begin
unsat_core := Explanation.get_unsat_core ftnd_env.FE.expl;
end;
let () =
match ftnd_env.FE.res with
| `Sat partial_model | `Unknown partial_model ->
begin
if Options.(get_interpretation () && get_dump_models ()) then
print_model (Options.Output.get_fmt_models ()) partial_model;
end
| `Unsat -> ()
in
()
in

let typed_loop all_context state td =
Expand Down
37 changes: 2 additions & 35 deletions src/lib/frontend/frontend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,21 +32,6 @@ open Commands
open Format
open Options

let timeout_reason_to_string = function
| Sat_solver_sig.Assume -> "Assume"
| ProofSearch -> "ProofSearch"
| ModelGen -> "ModelGen"

let unknown_reason_to_string = function
| Sat_solver_sig.Incomplete -> "Incomplete"
| Memout -> "Memout"
| Timeout t -> Format.sprintf "Timeout:%s" (timeout_reason_to_string t)

let unknown_reason_opt_to_string =
function
| None -> "Decided"
| Some r -> unknown_reason_to_string r

module E = Expr
module Ex = Explanation

Expand Down Expand Up @@ -311,23 +296,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
else Ex.empty

let print_model env unknown_reason_opt =
if Options.(get_interpretation () && get_dump_models ()) then begin
let s = unknown_reason_opt_to_string unknown_reason_opt in
match SAT.get_model env with
| None ->
Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
"@[<v 0>It seems that no model has been computed so \
far. You may need to change your model generation strategy \
or to increase your timeouts. Returned unknown reason = %s@]" s

| Some (lazy model) ->
Printer.print_fmt
(Options.Output.get_fmt_diagnostic ())
"@[<v 0>; Returned unknown reason = %s@]" s;
Models.output_concrete_model (Options.Output.get_fmt_models ()) model
end

let internal_push ?(loc = Loc.dummy) (env : env) (n : int) : env =
ignore loc;
Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
Expand Down Expand Up @@ -470,8 +438,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
(* This case should mainly occur when a query has a non-unsat result,
so we want to print the status in this case. *)
hook_on_status (Sat (d,t)) (Steps.get_steps ());
print_model env.sat_env None;
{env with res = `Sat t}

| SAT.Unsat expl' ->
(* This case should mainly occur when a new assumption results in an unsat
env, in which case we do not want to print status, since the correct
Expand All @@ -480,6 +448,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
if get_debug_unsat_core () then check_produced_unsat_core expl;
(* print_status (Inconsistent d) (Steps.get_steps ()); *)
{env with res = `Unsat; expl}

| SAT.I_dont_know t ->
(* TODO: always print Unknown for why3 ? *)
let ur = SAT.get_unknown_reason t in
Expand All @@ -489,7 +458,6 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
| _ -> Unknown (d, t)
in
hook_on_status status (Steps.get_steps ());
print_model t ur;
(* TODO: Is it an appropriate behaviour? *)
(* if timeout != NoTimeout then raise Util.Timeout; *)
{env with res = `Unknown t}
Expand All @@ -498,6 +466,5 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
(* In this case, we obviously want to print the status,
since we exit right after *)
hook_on_status (Timeout (Some d)) (Steps.get_steps ());
print_model env.sat_env None;
raise e
end
2 changes: 0 additions & 2 deletions src/lib/frontend/frontend.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,5 +90,3 @@ module type S = sig
end

module Make (SAT: Sat_solver_sig.S) : S with type sat_env = SAT.t

val unknown_reason_to_string : Sat_solver_sig.unknown_reason -> string
10 changes: 10 additions & 0 deletions src/lib/reasoners/sat_solver_sig.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,22 @@ type timeout_reason =
| Assume
| ProofSearch
| ModelGen
[@@deriving show]

type unknown_reason =
| Incomplete
| Memout
| Timeout of timeout_reason
Copy link
Collaborator

@Stevendeo Stevendeo Nov 14, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

Why not [@@deriving show] ?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Not sure to understand your remark :D


let pp_unknown_reason ppf = function
| Incomplete -> Fmt.pf ppf "Incomplete"
| Memout -> Fmt.pf ppf "Memout"
| Timeout t -> Fmt.pf ppf "Timeout:%a" pp_timeout_reason t

let pp_unknown_reason_opt ppf = function
| None -> Fmt.pf ppf "Decided"
| Some ur -> pp_unknown_reason ppf ur

module type S = sig
type t

Expand Down
3 changes: 3 additions & 0 deletions src/lib/reasoners/sat_solver_sig.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@ type unknown_reason =
| Memout
| Timeout of timeout_reason

val pp_unknown_reason: unknown_reason Fmt.t
val pp_unknown_reason_opt : unknown_reason option Fmt.t

module type S = sig
type t

Expand Down
Loading