Adding instruction handler to solving loop

OCamlPro · Oct 9, 2023 · 9fc24e4 · 9fc24e4
1 parent 5342be6
commit 9fc24e4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 4 deletions.
diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml
@@ -484,7 +484,11 @@ let main () =
       pp_reason_unknown st
     | ":version" ->
       print_std Fmt.string Version._version
-    | ":all-statistics"
+    | ":all-statistics" ->
+      if Options.get_profiling () then
+        Printer.print_std "%t" Profiling.print_get_statistics
+      else
+        Printer.print_smtlib_err "Profiling disactivated (try --profiling)"
     | ":assertion-stack-levels" ->
       unsupported_opt name
     | _ ->

diff --git a/src/lib/structures/profiling.ml b/src/lib/structures/profiling.ml
@@ -709,14 +709,17 @@ let register_int_stat (key : string) (getter : unit -> int) =
   register_stat key (fun () -> string_of_int (getter ()))
 
 let register_float_stat (key : string) (getter : unit -> float) =
-  register_stat key (fun () -> string_of_float (getter ()))
+  register_stat
+    key
+    (fun () ->
+       Format.sprintf "%.9f" (getter ()))
 
 let print_get_statistics fmt =
-  Format.fprintf fmt "(@[<v 0>";
+  Format.fprintf fmt "(@[<v 0>@,";
   Hashtbl.iter
     (fun key getter -> Format.fprintf fmt ":%s %s@," key (getter ()))
     statistics_table;
-  Format.fprintf fmt ")@]"
+  Format.fprintf fmt "@])@,"
 
 (* Now, registering the statistics we want in get-statistics. *)
 let () =