feat: support (get-info :all-statistics) and refactoring Profiling mo…

…dule (#863)

This PR was initially open to add the get-statistics option. Some bugs and (IMHO) bad design choices in the Timer and Profiling module changed the purpose of this PR to not only add the get-statistics feature, but also to rework it.

alt-ergo-lib.opam

@@ -28,6 +28,7 @@ depends: [
   "ppx_blob" {>= "0.7.2"}
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
+  "ppx_deriving"
 ]
 conflicts: [
   "ppxlib" {< "0.30.0"}

src/bin/common/signals_profiling.ml

@@ -30,10 +30,6 @@
 
 open AltErgoLib
 
-let timers = Timers.empty ()
-
-let get_timers () = timers
-
 let init_sigterm_6 () =
   (* what to do with Ctrl+C ? *)
   Sys.set_signal Sys.sigint(*-6*)
@@ -58,7 +54,7 @@ let init_sigterm_11_9 () =
            (Sys.Signal_handle
               (fun _ ->
                  Profiling.print true (Steps.get_steps ())
-                   timers (Options.Output.get_fmt_diagnostic ());
+                   (Options.Output.get_fmt_diagnostic ());
                  exit 1
               )
            )
@@ -71,7 +67,7 @@ let init_sigterm_21 () =
     Sys.set_signal Sys.sigprof (*-21*)
       (Sys.Signal_handle
          (fun _ ->
-            Profiling.print false (Steps.get_steps ()) timers
+            Profiling.print false (Steps.get_steps ())
               (Options.Output.get_fmt_diagnostic ());
          )
       )
@@ -84,10 +80,7 @@ let init_sigalarm () =
 
 let init_profiling () =
   if Options.get_profiling () then begin
-    Timers.reset timers;
     assert (Options.get_timers());
-    Timers.set_timer_start (Timers.start timers);
-    Timers.set_timer_pause (Timers.pause timers);
     Profiling.init ();
   end
 

src/bin/common/signals_profiling.mli

@@ -28,9 +28,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Return a timer *)
-val get_timers : unit -> AltErgoLib.Timers.t
-
 (** Initialise signals handler for system signals *)
 val init_signals : unit -> unit
 

src/bin/common/solving_loop.ml

@@ -120,7 +120,6 @@ let main () =
       if Options.get_profiling() then
         Profiling.print true
           (Steps.get_steps ())
-          (Signals_profiling.get_timers ())
           (Options.Output.get_fmt_diagnostic ());
       (* If the status of the SAT environment is inconsistent,
          we have to drop the partial model in order to prevent
@@ -393,6 +392,7 @@ let main () =
 
   let handle_option st_loc name (value : DStd.Term.t) =
     match name, value.term with
+    (* Smtlib2 regular options *)
     | ":regular-output-channel", Symbol { name = Simple name; _ } ->
       Options.Output.create_channel name
       |> Options.Output.set_regular
@@ -445,6 +445,13 @@ let main () =
       | ":random-seed"), _
       ->
       unsupported_opt name
+    (* Alt-Ergo custom options *)
+    | ":profiling", Symbol { name = Simple level; _ } ->
+      begin
+        match float_of_string_opt level with
+        | None -> print_wrn_opt ~name st_loc "nonnegative integer" value
+        | Some i -> Options.set_profiling true i
+      end
     | _ ->
       unsupported_opt name
   in
@@ -485,7 +492,10 @@ let main () =
       pp_reason_unknown st
     | ":version" ->
       print_std Fmt.string Version._version
-    | ":all-statistics"
+    | ":all-statistics" ->
+      Printer.print_std "%t" Profiling.print_statistics;
+      if not (Options.get_profiling ()) then
+        warning "Profiling disactivated (try --profiling)"
     | ":assertion-stack-levels" ->
       unsupported_opt name
     | _ ->

src/lib/dune

@@ -25,7 +25,7 @@
     alt_ergo_prelude
     fmt
   )
-  (preprocess (pps ppx_blob))
+  (preprocess (pps ppx_blob ppx_deriving.show ppx_deriving.enum ppx_deriving.fold))
   (preprocessor_deps (glob_files ../preludes/*.ae))
 
   ; .mli only modules *also* need to be in this field