Add Z3_get_estimated_alloc_size to OCaml API (#7068)

Z3Prover · Dec 21, 2023 · 68a2c08 · 68a2c08
1 parent 19f3ad4
commit 68a2c08
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 0 deletions.
diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml
@@ -308,6 +308,7 @@ let fpa_example ( ctx : context ) =
   (
     let solver = (mk_solver ctx None) in
 	(Solver.add solver [ c5 ]) ;
+    Printf.printf "Memory in use before `check`: %Lu bytes\n" (Statistics.get_estimated_alloc_size());
     if (check solver []) != SATISFIABLE then
 	  raise (TestFailedException "")
     else

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
@@ -1832,6 +1832,9 @@ struct
   let get (x:statistics) (key:string) =
     try Some(List.find (fun c -> Entry.get_key c = key) (get_entries x)) with
     | Not_found -> None
+
+  let get_estimated_alloc_size =
+    Z3native.get_estimated_alloc_size
 end
 
 

diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
@@ -3224,6 +3224,9 @@ sig
 
   (** The value of a particular statistical counter. *)
   val get : statistics -> string -> Entry.statistics_entry option
+
+  (** The estimated allocated memory in bytes. *)
+  val get_estimated_alloc_size : unit -> int64
 end
 
 (** Solvers *)