Skip to content

Commit

Permalink
Display steps number even when profiling is off
Browse files Browse the repository at this point in the history
  • Loading branch information
Stevendeo committed Nov 16, 2023
1 parent e6d3112 commit a84336e
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 6 deletions.
4 changes: 1 addition & 3 deletions src/bin/common/solving_loop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -698,9 +698,7 @@ let main () =
| ":version" ->
print_std Fmt.string Version._version
| ":all-statistics" ->
Printer.print_std "%t" Profiling.print_statistics;
if not (Options.get_profiling ()) then
warning "Profiling disactivated (try --profiling)"
Printer.print_std "%t" Profiling.print_statistics
| ":assertion-stack-levels" ->
unsupported_opt name
| _ ->
Expand Down
9 changes: 6 additions & 3 deletions src/lib/structures/profiling.ml
Original file line number Diff line number Diff line change
Expand Up @@ -728,6 +728,7 @@ let print =
the (get-statistics) instruction is performed. *)
let statistics_table : (string, (unit -> string)) Hashtbl.t = Hashtbl.create 7


let register_stat (key : string) (getter : unit -> string) =
Hashtbl.add statistics_table key getter

Expand All @@ -747,6 +748,10 @@ let print_statistics fmt =
statistics_table;
Fmt.pf fmt "@])@,"

(* Registering the statistics we want to display even when profiling is off. *)
let () =
register_int_stat "steps" (fun () -> Steps.get_steps ())

let init () =
let state = Lazy.force state in
state.decisions <- 0;
Expand All @@ -773,9 +778,7 @@ let init () =
Timers.set_timer_pause (Timers.pause timers);
Timers.reset timers;
set_sigprof ();

(* Now, registering the statistics we want in (get-info :all-statistics). *)
register_int_stat "steps" (fun () -> Steps.get_steps ());
(* Registering timer statistics. *)
List.iter
(fun (m : Timers.ty_module) ->
let name = Format.sprintf "timer-%s" (Timers.string_of_ty_module m) in
Expand Down

0 comments on commit a84336e

Please sign in to comment.