Skip to content

Commit

Permalink
Bubbling the model printing in the binary
Browse files Browse the repository at this point in the history 
This commit bubbles the decision of printing models in the binary. Now,
the library do not print models at all.
  • Loading branch information
@Halbaroth
Halbaroth committed Nov 14, 2023
1 parent fd6a475 commit e0096a2
Show file tree
Hide file tree
Showing 5 changed files with 51 additions and 61 deletions.
74 changes: 37 additions & 37 deletions src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,27 @@ let main () =
O.get_sat_solver (),
(module SatCont.Make(TH) : Sat_solver_sig.S)
in

let pp_unknown_reason_opt ppf = function
| None -> Fmt.pf ppf "Decided"
| Some ur -> Sat_solver_sig.pp_unknown_reason ppf ur
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@]" 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

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 +207,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 +701,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 @@ -746,23 +770,6 @@ let main () =
assignments
in

let handle_model (env: model) =
match env with
| Model ((module SAT : Sat_solver_sig.S with type t), env) ->
begin
if Options.get_interpretation () then
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) ->
Models.output_concrete_model (Options.Output.get_fmt_models ()) model
end
in

let handle_stmt :
Frontend.used_context -> State.t ->
_ D_loop.Typer_Pipe.stmt -> State.t =
Expand Down Expand Up @@ -854,21 +861,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
else
begin
(* TODO: add the location of the statement. *)
Expand Down
28 changes: 6 additions & 22 deletions src/lib/frontend/frontend.ml
View file
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,8 +296,8 @@ 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 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 ->
Expand All @@ -326,8 +311,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
(Options.Output.get_fmt_diagnostic ())
"@[<v 0>; Returned unknown reason = %s@]" s;
Models.output_concrete_model (Options.Output.get_fmt_models ()) model
end

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 +455,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 +465,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 +475,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 +483,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
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
6 changes: 6 additions & 0 deletions src/lib/reasoners/sat_solver_sig.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,12 +35,18 @@ type timeout_reason =
| Assume
| ProofSearch
| ModelGen
[@@deriving show]

type unknown_reason =
| Incomplete
| Memout
| Timeout of timeout_reason

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

module type S = sig
type t

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

val pp_unknown_reason: unknown_reason Fmt.t

module type S = sig
type t

Expand Down

0 comments on commit e0096a2

Please sign in to comment.