Skip to content

Commit

Permalink
Remove Preprocess status in Frontend (#1285)
Browse files Browse the repository at this point in the history
This status was used by the legacy frontend.
  • Loading branch information
Halbaroth authored Feb 4, 2025
1 parent 3198371 commit 1b7fd77
Show file tree
Hide file tree
Showing 5 changed files with 1 addition and 24 deletions.
1 change: 0 additions & 1 deletion src/bin/js/worker_js.ml
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,6 @@ let main worker_id filename filecontent =
| Sat _ -> Worker_interface.Sat n
| Unknown _ -> Worker_interface.Unknown n
| Timeout _ -> Worker_interface.LimitReached "timeout"
| Preprocess -> Worker_interface.Unknown n
end;
Frontend.print_status status n
in
Expand Down
7 changes: 1 addition & 6 deletions src/lib/frontend/frontend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ type status =
| Sat of Commands.sat_tdecl
| Unknown of Commands.sat_tdecl
| Timeout of Commands.sat_tdecl option
| Preprocess

let print_status status steps =
let check_status_consistency s =
Expand All @@ -63,7 +62,7 @@ let print_status status steps =
"This file is known to be Unsat but Alt-Ergo return Sat";
Errors.warning_as_error ()
end
| Inconsistent _ | Unknown _ | Timeout _ | Preprocess ->
| Inconsistent _ | Unknown _ | Timeout _ ->
assert false
in
let validity_mode =
Expand Down Expand Up @@ -117,10 +116,6 @@ let print_status status steps =
Printer.print_status_timeout ~validity_mode
None (Some time) (Some steps) None;

| Preprocess ->
Printer.print_status_preprocess ~validity_mode
(Some time) (Some steps)

module type S = sig

type sat_env
Expand Down
1 change: 0 additions & 1 deletion src/lib/frontend/frontend.mli
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,6 @@ type status =
| Sat of Commands.sat_tdecl
| Unknown of Commands.sat_tdecl
| Timeout of Commands.sat_tdecl option
| Preprocess

val print_status : status -> int -> unit

Expand Down
7 changes: 0 additions & 7 deletions src/lib/util/printer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -373,13 +373,6 @@ let print_status_timeout ?(validity_mode=true) loc
("Timeout","unknown","fg_orange") loc
time steps goal

let print_status_preprocess ?(validity_mode=true)
time steps =
print_status ~validity_mode
~formatter:(Options.Output.get_fmt_diagnostic ())
("Preprocessing","","fg_magenta") None
time steps None

let print_smtlib_err ?(flushed=true) s =
(* The smtlib error messages are printed on the regular output. *)
pp_std_smt ();
Expand Down
9 changes: 0 additions & 9 deletions src/lib/util/printer.mli
Original file line number Diff line number Diff line change
Expand Up @@ -161,15 +161,6 @@ val print_status_inconsistent :
int option ->
string option -> unit

(** Print preprocess status message from the frontend on the standard output.
If validity_mode is set, the status print :
`Preprocess (<time>s) (<steps> steps)`
else, we print nothing. *)
val print_status_preprocess :
?validity_mode:bool ->
float option ->
int option -> unit

(** Print smtlib error message on the regular formatter, accessible with
{!val:Options.get_fmt_regular} and set by default to stdout.
The regular formatter is flushed after the print if flushed is set. *)
Expand Down

0 comments on commit 1b7fd77

Please sign in to comment.