From cb621ca0a9d1fa5b2f77954833a725fb88e7b0bd Mon Sep 17 00:00:00 2001
From: joaomhmpereira <joaompereira07@gmail.com>
Date: Mon, 30 Sep 2024 16:55:38 +0100
Subject: [PATCH] Add percentage count do --dry runs

---
 bin/main.ml          | 10 ++++++++++
 src/parser/smtlib.ml |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/bin/main.ml b/bin/main.ml
index 7349bfd6..9ba6545a 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -42,11 +42,14 @@ let test debug solver prover_mode print_statistics dry files =
   (* TODO: Add proper logs *)
   let debug fmt k = if debug then k (Fmt.epr fmt) in
   let exception_log = ref [] in
+  let total_tests = ref 0 in
+  let exception_count = ref 0 in
   let rec test_path state path =
     if Sys.is_directory (Fpath.to_string path) then test_dir state path
     else begin
       debug "File %a...@." (fun k -> k Fpath.pp path);
       try
+        incr total_tests;
         let ast = Compile.until_rewrite path in
         if dry then begin
           state
@@ -55,6 +58,7 @@ let test debug solver prover_mode print_statistics dry files =
           Some (Interpret.start ?state ast)
         end
       with exn ->
+        incr exception_count;
         let exn_msg = Printexc.to_string exn in
         exception_log := (path, exn_msg) :: !exception_log;
         debug "Error processing file %a@." (fun k -> k Fpath.pp path);
@@ -72,6 +76,12 @@ let test debug solver prover_mode print_statistics dry files =
   let state = test_files files in
   let write_exception_log () =
     let oc = open_out "exceptions.log" in
+    let total = !total_tests in
+    let exceptions = !exception_count in
+    let percentage = if total = 0 then 0.0 else (float_of_int exceptions /. float_of_int total) *. 100.0 in
+    Printf.fprintf oc "Total tests: %d\n" total;
+    Printf.fprintf oc "Exceptions: %d\n" exceptions;
+    Printf.fprintf oc "Exception percentage: %.2f%%\n\n" percentage;
     List.iter
       (fun (path, exn_msg) ->
         Printf.fprintf oc "File: %s\nError: %s\n\n" (Fpath.to_string path)
diff --git a/src/parser/smtlib.ml b/src/parser/smtlib.ml
index 5b40572e..be65df52 100644
--- a/src/parser/smtlib.ml
+++ b/src/parser/smtlib.ml
@@ -291,7 +291,7 @@ module Statement = struct
     let name = (match Symbol.name id with
       | Simple name -> name
       | _ -> assert false) in
-    Hashtbl.add custom_sorts name (Expr.ty t);
+    Hashtbl.replace custom_sorts name (Expr.ty t);
     Echo ""
 
   let datatypes ?loc:_ = assert false