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 all 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
43 changes: 23 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,7 @@ let main () =
O.get_sat_solver (),
(module SatCont.Make(TH) : Sat_solver_sig.S)
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 +187,17 @@ 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 begin
let ur = SAT.get_unknown_reason partial_model in
Printer.print_fmt (Options.Output.get_fmt_diagnostic ())
"@[<v 0>Returned unknown reason = %a@]"
Sat_solver_sig.pp_unknown_reason_opt ur;
FE.print_model (Options.Output.get_fmt_models ()) partial_model
end;
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 +686,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 +846,15 @@ 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 ((module SAT), env)) ->
let module FE = Frontend.Make (SAT) in
FE.print_model (Options.Output.get_fmt_regular ()) env
| None ->
(* TODO: add the location of the statement. *)
recoverable_error "No model produced."
in
st
else
begin
(* TODO: add the location of the statement. *)
Expand Down
10 changes: 10 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 @@ -133,6 +133,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
FE.print_model (Options.Output.get_fmt_models ()) partial_model;
end
| `Unsat -> ()
in
()
in

let typed_loop all_context state td =
Expand Down
53 changes: 18 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 @@ -178,6 +163,8 @@ module type S = sig
env ->
sat_tdecl ->
env

val print_model: sat_env Fmt.t
end

let init_with_replay_used acc f =
Expand Down Expand Up @@ -311,23 +298,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 +440,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 +450,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 +460,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 +468,19 @@ 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

let print_model ppf env =
match SAT.get_model env with
| None ->
let ur = SAT.get_unknown_reason env in
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 = %a@]"
Sat_solver_sig.pp_unknown_reason_opt ur;

| Some (lazy model) ->
Models.output_concrete_model ppf model
end
4 changes: 2 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 @@ -87,8 +87,8 @@ module type S = sig
env ->
Commands.sat_tdecl ->
env

val print_model: sat_env Fmt.t
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