fix cache hits test

Author: S41d

README.md

@@ -143,8 +143,6 @@ module Z3 :
     val get_sat_model :
       ?symbols:Symbol.t list ->
       t -> Expr.Set.t -> [ `Model of Model.t | `Unknown | `Unsat ]
-    val cache_hits : unit -> int
-    val cache_misses : unit -> int
   end
 # let solver = Z3.create ();;
 val solver : Z3.t = <abstr>

doc/index.mld

@@ -52,8 +52,6 @@ module Z3 :
       ?symbols:Smtml.Symbol.t list ->
       t ->
       Smtml.Expr.Set.t -> [ `Model of Smtml.Model.t | `Unknown | `Unsat ]
-    val cache_hits : unit -> int
-    val cache_misses : unit -> int
   end
 # let solver = Z3.create ();;
 val solver : Z3.t = <abstr>

src/smtml/altergo_mappings.default.ml

@@ -224,8 +224,7 @@ module M = struct
       let interrupt _ =
         Fmt.failwith "Altergo_mappings: interrupt is not implemented"
 
-      let get_statistics _ =
-        Fmt.failwith "Altergo_mappings: get_statistics is not implemented"
+      let get_statistics _ = Statistics.Map.empty
 
       let pp_statistics _fmt _solver = ()
     end

src/smtml/bitwuzla_mappings.default.ml

@@ -552,8 +552,7 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
       (* does nothing *)
       ()
 
-    let get_statistics _ =
-      Fmt.failwith "Bitwuzla_mappings: Solver.get_statistics not implemented"
+    let get_statistics _ = Statistics.Map.empty
 
     let pp_statistics fmt solver = Solver.pp_statistics fmt solver
   end

src/smtml/colibri2_mappings.default.ml

@@ -206,8 +206,7 @@ module M = struct
 
       let interrupt _ = ()
 
-      let get_statistics _ =
-        Fmt.failwith "Colibri2_mappings: Solver.get_statistics not implemented"
+      let get_statistics _ = Statistics.Map.empty
 
       let pp_statistics _fmt _solver = ()
     end

src/smtml/cvc5_mappings.default.ml

@@ -561,11 +561,9 @@ module Fresh_cvc5 () = struct
 
     let interrupt _ = ()
 
-    let get_statistics _ =
-      Fmt.failwith "Cvc5_mappings: Solver.get_statistics not implemented!"
+    let get_statistics _ = Statistics.Map.empty
 
-    let pp_statistics _ =
-      Fmt.failwith "Cvc5_mappings: Solver.pp_statistics not implemented!"
+    let pp_statistics _ _ = ()
   end
 
   (* Not supported *)

test/integration/test_solver.ml

@@ -44,12 +44,20 @@ module Make (M : Mappings_intf.S_with_fresh) = struct
     let solver = Cached.create ~logic:LIA () in
     let x = Infix.symbol "x" Ty_int in
     let c = Infix.(Int.(x >= int 0)) in
-    assert (Cached.cache_hits () = 0);
+    let get_stat key =
+      let stats = Cached.get_statistics solver in
+      let stat = Statistics.Map.find_opt key stats in
+      match stat with
+      (* we're using this for cache hitrate so it's always `Int *)
+      | Some (`Int s) -> s
+      | _ -> Fmt.failwith "%s should exist and be an int in stats" key
+    in
+    assert (get_stat "cache hits" = 0);
     assert_sat (Cached.check_set solver @@ Expr.Set.singleton c);
     assert_sat (Cached.check_set solver @@ Expr.Set.singleton c);
     assert_sat (Cached.check_set solver @@ Expr.Set.singleton c);
-    assert (Cached.cache_misses () = 1);
-    assert (Cached.cache_hits () = 2)
+    assert (get_stat "cache misses" = 1);
+    assert (get_stat "cache hits" = 2)
 
   let test_cache_get_model _ =
     let open Infix in