Adds Solver.get_statistics function (Closes #85)

lib/bitwuzla_mappings.default.ml

@@ -381,6 +381,9 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
       (* does nothing *)
       ()
 
+    let get_statistics _ =
+      failwith "Bitwuzla_mappings: Solver.get_statistics not implemented"
+
     let pp_statistics fmt solver = Solver.pp_statistics fmt solver
   end
 
@@ -406,6 +409,9 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
     let interrupt _ =
       failwith "Bitwuzla_mappings: Optimizer.interrupt not implemented"
 
+    let get_statistics _ =
+      failwith "Bitwuzla_mappings: Solver.get_statistics not implemented"
+
     let pp_statistics _ =
       failwith "Bitwuzla_mappings: Optimizer.pp_statistics not implemented"
   end

lib/colibri2_mappings.default.ml

@@ -957,7 +957,8 @@ module Fresh = struct
 
       let interrupt _ = ()
 
-      let pp_statistics _ _ = ()
+      let get_statistics _ =
+        err "Colibri2_mappings: Solver.get_statistics not implemented"
     end
 
     module Optimizer = struct
@@ -988,7 +989,8 @@ module Fresh = struct
 
       let interrupt _ = ()
 
-      let pp_statistics _ _ = ()
+      let get_statistics _ =
+        err "Colibri2_mappings: Optimizer.get_statistics not implemented"
     end
 
     let c2value_to_value (ty : Ty.t) (v : Colibri2_core.Value.t) =

lib/cvc5_mappings.default.ml

@@ -396,6 +396,9 @@ module Fresh_cvc5 () = struct
 
     let interrupt _ = ()
 
+    let get_statistics _ =
+      failwith "Cvc5_mappings: Solver.get_statistics not implemented!"
+
     let pp_statistics _ = assert false
   end
 
@@ -420,6 +423,9 @@ module Fresh_cvc5 () = struct
     let interrupt _ = assert false
 
     let pp_statistics _ = assert false
+
+    let get_statistics _ =
+      failwith "Cvc5_mappings: Optimizer.get_statistics not implemented!"
   end
 end
 

lib/dune

@@ -36,6 +36,7 @@
   solver_intf
   solver_dispatcher
   symbol
+  statistics
   ty
   utils
   value

lib/mappings.ml

@@ -662,7 +662,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       let interrupt _ = M.Solver.interrupt ()
 
-      let pp_statistics fmt { solver; _ } = M.Solver.pp_statistics fmt solver
+      let get_statistics { solver; _ } = M.Solver.get_statistics solver
     end
 
     module Optimizer = struct
@@ -690,7 +690,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
 
       let interrupt _ = M.Optimizer.interrupt ()
 
-      let pp_statistics fmt { opt; _ } = M.Optimizer.pp_statistics fmt opt
+      let get_statistics { opt; _ } = M.Optimizer.get_statistics opt
     end
   end
 

lib/mappings.nop.ml

@@ -323,6 +323,8 @@ module Nop = struct
 
       let interrupt _ = die ()
 
+      let get_statistics _ = die ()
+
       let pp_statistics _ = die ()
     end
 
@@ -345,6 +347,8 @@ module Nop = struct
 
       let interrupt _ = die ()
 
+      let get_statistics _ = die ()
+
       let pp_statistics _ = die ()
     end
   end

lib/mappings_intf.ml

@@ -338,6 +338,8 @@ module type M = sig
 
     val interrupt : unit -> unit
 
+    val get_statistics : solver -> Statistics.t
+
     val pp_statistics : Format.formatter -> solver -> unit
   end
 
@@ -360,6 +362,8 @@ module type M = sig
 
     val interrupt : unit -> unit
 
+    val get_statistics : optimizer -> Statistics.t
+
     val pp_statistics : Format.formatter -> optimizer -> unit
   end
 end
@@ -410,7 +414,7 @@ module type S = sig
 
     val interrupt : solver -> unit
 
-    val pp_statistics : Format.formatter -> solver -> unit
+    val get_statistics : solver -> Statistics.t
   end
 
   module Optimizer : sig
@@ -432,7 +436,7 @@ module type S = sig
 
     val interrupt : optimize -> unit
 
-    val pp_statistics : Format.formatter -> optimize -> unit
+    val get_statistics : optimize -> Statistics.t
   end
 end
 

lib/model.ml

@@ -18,7 +18,6 @@
 
 type t = (Symbol.t, Value.t) Hashtbl.t
 
-
 let iter f model = Hashtbl.iter (fun a b -> f (a, b)) model
 
 let get_symbols (model : t) : Symbol.t List.t =

lib/optimizer.ml

@@ -65,6 +65,8 @@ module Make (M : Mappings_intf.S) = struct
       let+ model = O.model opt in
       M.value model e
     | _ -> None
+
+  let get_statistics (opt : t) : Statistics.t = M.Optimizer.get_statistics opt
 end
 
 module Z3 = Make (Z3_mappings)

lib/optimizer_intf.ml

@@ -20,6 +20,8 @@ module type S = sig
   val maximize : t -> Expr.t -> Value.t option
 
   val minimize : t -> Expr.t -> Value.t option
+
+  val get_statistics : t -> Statistics.t
 end
 
 module type Intf = sig

lib/solver.ml

@@ -29,7 +29,7 @@ module Base (M : Mappings_intf.S) = struct
 
   let solver_count = ref 0
 
-  let pp_statistics fmt solver = M.Solver.pp_statistics fmt solver
+  let pp_statistics _fmt _solver = ()
 
   let create ?params ?logic () : t = M.Solver.make ?params ?logic ()
 
@@ -47,6 +47,9 @@ module Base (M : Mappings_intf.S) = struct
 
   let get_assertions (_solver : t) : Expr.t list = assert false
 
+  let get_statistics (solver : t) : Statistics.t =
+    M.Solver.get_statistics solver
+
   let check (solver : M.solver) (es : Expr.t list) : satisfiability =
     solver_count := !solver_count + 1;
     Utils.run_and_time_call
@@ -107,6 +110,8 @@ module Make_batch (Mappings : Mappings_intf.S) = struct
 
   let get_assertions (s : t) : Expr.t list = s.top [@@inline]
 
+  let get_statistics (s : t) : Statistics.t = get_statistics s.solver
+
   let check (s : t) (es : Expr.t list) : satisfiability =
     check s.solver (es @ s.top)
 

lib/solver_intf.ml

@@ -63,6 +63,9 @@ module type S = sig
 
   (** The set of assertions in the solver. *)
   val get_assertions : t -> Expr.t list
+  [@@deprecated "Please use 'get_statistics' instead"]
+
+  val get_statistics : t -> Statistics.t
 
   (** [check solver es] checks the satisfiability of the assertions in the
       solver using the assumptions in [es].

lib/statistics.ml

@@ -0,0 +1,37 @@
+type entry =
+  [ `Int of int
+  | `Float of float
+  ]
+
+module Map = Map.Make (String)
+
+type t = entry Map.t
+
+let combine e1 e2 =
+  match (e1, e2) with
+  | `Int i1, `Int i2 -> `Int (i1 + i2)
+  | `Float f1, `Float f2 -> `Float (f1 +. f2)
+  | _ -> failwith "Statistics: entry type mismatch"
+
+let merge s1 s2 =
+  Map.merge
+    (fun _ left right ->
+      match (left, right) with
+      | Some v1, Some v2 -> Some (combine v1 v2)
+      | (Some _ as v), None | None, (Some _ as v) -> v
+      | None, None -> None )
+    s1 s2
+
+let pp_entry fmt = function
+  | `Int i -> Format.pp_print_int fmt i
+  | `Float f -> Format.pp_print_float fmt f
+
+let pp fmt m =
+  let iter f v = Map.iter (fun a b -> f (a, b)) v in
+  let pp_v fmt (k, v) = Format.fprintf fmt "(%s, %a)" k pp_entry v in
+  let is_first = ref true in
+  let pp_v v =
+    if !is_first then is_first := false else Format.pp_print_newline fmt ();
+    pp_v fmt v
+  in
+  iter pp_v m

lib/z3_mappings.default.ml

@@ -643,10 +643,21 @@ module Fresh = struct
         (Z3.SMT.benchmark_to_smtstring ctx "" "" st "" (List.tl es')
            (List.hd es') )
 
-    let pp_entry fmt entry =
-      let key = Z3.Statistics.Entry.get_key entry in
-      let value = Z3.Statistics.Entry.to_string_value entry in
-      Format.fprintf fmt "(%s %s)" key value
+    let get_statistics stats =
+      let statistics = Z3.Statistics.get_entries stats in
+      let add_entry map entry =
+        let key = Z3.Statistics.Entry.get_key entry in
+        let value =
+          if Z3.Statistics.Entry.is_int entry then
+            `Int (Z3.Statistics.Entry.get_int entry)
+          else begin
+            assert (Z3.Statistics.Entry.is_float entry);
+            `Float (Z3.Statistics.Entry.get_float entry)
+          end
+        in
+        Statistics.Map.add key value map
+      in
+      List.fold_left add_entry Statistics.Map.empty statistics
 
     module Solver = struct
       let make ?params ?logic () : solver =
@@ -690,13 +701,8 @@ module Fresh = struct
 
       let interrupt _ = Z3.Tactic.interrupt ctx
 
-      let pp_statistics fmt solver =
-        let module Entry = Z3.Statistics.Entry in
-        let stats = Z3.Solver.get_statistics solver in
-        let entries = Z3.Statistics.get_entries stats in
-        Format.pp_print_list
-          ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
-          pp_entry fmt entries
+      let get_statistics solver =
+        get_statistics (Z3.Solver.get_statistics solver)
     end
 
     module Optimizer = struct
@@ -722,13 +728,8 @@ module Fresh = struct
 
       let interrupt _ = Z3.Tactic.interrupt ctx
 
-      let pp_statistics fmt o =
-        let module Entry = Z3.Statistics.Entry in
-        let stats = Z3.Optimize.get_statistics o in
-        let entries = Z3.Statistics.get_entries stats in
-        Format.pp_print_list
-          ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
-          pp_entry fmt entries
+      let get_statistics solver =
+        get_statistics (Z3.Optimize.get_statistics solver)
     end
 
     let set (s : string) (i : int) (n : char) =

lib/z3_mappings2.default.ml

@@ -19,6 +19,7 @@
 include Mappings_intf
 module P = Params
 module Sym = Symbol
+module Stats = Statistics
 
 let err = Log.err
 
@@ -387,6 +388,22 @@ module M = struct
         ~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
         pp_entry fmt entries
 
+    let get_statistics (stats : Statistics.statistics) =
+      let statistics = Z3.Statistics.get_entries stats in
+      let add_entry map entry =
+        let key = Z3.Statistics.Entry.get_key entry in
+        let value =
+          if Z3.Statistics.Entry.is_int entry then
+            `Int (Z3.Statistics.Entry.get_int entry)
+          else begin
+            assert (Z3.Statistics.Entry.is_float entry);
+            `Float (Z3.Statistics.Entry.get_float entry)
+          end
+        in
+        Stats.Map.add key value map
+      in
+      List.fold_left add_entry Stats.Map.empty statistics
+
     let set_params (params : P.t) =
       Z3.set_global_param "smt.ematching"
         (string_of_bool @@ P.get params Ematching);
@@ -440,6 +457,9 @@ module M = struct
 
       let interrupt () = Tactic.interrupt ctx
 
+      let get_statistics solver =
+        get_statistics (Z3.Solver.get_statistics solver)
+
       let pp_statistics fmt solver =
         pp_statistics fmt @@ Solver.get_statistics solver
     end
@@ -467,6 +487,8 @@ module M = struct
 
       let interrupt () = Tactic.interrupt ctx
 
+      let get_statistics opt = get_statistics (Optimize.get_statistics opt)
+
       let pp_statistics fmt opt =
         pp_statistics fmt @@ Optimize.get_statistics opt
     end

test/unit/dune

@@ -8,5 +8,6 @@
   test_relop
   test_cvtop
   test_naryop
-  test_model)
+  test_model
+  test_statistics)
  (libraries smtml yojson))

test/unit/test_statistics.ml

@@ -0,0 +1,7 @@
+open Smtml
+module Map = Statistics.Map
+
+let () =
+  let s1 = Map.empty |> Map.add "time" (`Float 10.0) in
+  let s2 = Map.empty |> Map.add "time" (`Float 20.0) in
+  assert (Statistics.merge s1 s2 |> Map.find "time" = `Float 30.0)