Cleanup timers module: remove Sum and Typer constructors (#1275)

Author: hra687261

src/lib/structures/profiling.ml

@@ -454,12 +454,6 @@ let columns : (string * string * int * bool option * 'a) list =
        Format.sprintf "%s~%s"
          (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4));
 
-    "Sum", "Time spent in Sum module(s)", 16, Some false,
-    (fun _ gtime sz ->
-       let curr = Timers.get_sum (get_timers ()) Timers.M_Sum in
-       Format.sprintf "%s~%s"
-         (float_resize curr (sz - 5)) (string_resize (percent gtime curr) 4));
-
     "Records", "Time spent in Records module(s)", 16, Some false,
     (fun _ gtime sz ->
        let curr = Timers.get_sum (get_timers ()) Timers.M_Records in
@@ -480,10 +474,9 @@ let columns : (string * string * int * bool option * 'a) list =
        let tcc = Timers.get_sum timers Timers.M_CC in
        let tarith = Timers.get_sum timers Timers.M_Arith in
        let tarrays = Timers.get_sum timers Timers.M_Arrays in
-       let tsum = Timers.get_sum timers Timers.M_Sum in
        let trecs = Timers.get_sum timers Timers.M_Records in
        let tac = Timers.get_sum timers Timers.M_AC in
-       let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.tsum+.trecs+.tac in
+       let total = tsat+.tmatch+.tcc+.tarith+.tarrays+.trecs+.tac in
        float_resize total sz);
   ]
 

src/lib/util/timers.ml

@@ -32,14 +32,12 @@
 type ty_module =
   | M_None
   | M_Combine
-  | M_Typing
   | M_Sat
   | M_Match
   | M_CC
   | M_UF
   | M_Arith
   | M_Arrays
-  | M_Sum
   | M_Records
   | M_Adt
   | M_Bitv
@@ -54,14 +52,12 @@ let all_modules =
   let l = [
     M_None;
     M_Combine;
-    M_Typing;
     M_Sat;
     M_Match;
     M_CC;
     M_UF;
     M_Arith;
     M_Arrays;
-    M_Sum;
     M_Records;
     M_Adt;
     M_Bitv;
@@ -129,14 +125,12 @@ let all_functions =
 let string_of_ty_module k = match k with
   | M_None     -> "None"
   | M_Combine  -> "Combine"
-  | M_Typing   -> "Typing"
   | M_Sat      -> "Sat"
   | M_Match    -> "Match"
   | M_CC       -> "CC"
   | M_UF       -> "UF"
   | M_Arith    -> "Arith"
   | M_Arrays   -> "Arrays"
-  | M_Sum      -> "Sum"
   | M_Records  -> "Records"
   | M_Adt      -> "Adt"
   | M_Bitv     -> "Bitv"

src/lib/util/timers.mli

@@ -28,14 +28,12 @@
 type ty_module =
   | M_None
   | M_Combine
-  | M_Typing
   | M_Sat
   | M_Match
   | M_CC
   | M_UF
   | M_Arith
   | M_Arrays
-  | M_Sum
   | M_Records
   | M_Adt
   | M_Bitv

src/lib/util/util.ml

@@ -77,7 +77,6 @@ let pp_sat_solver ppf = function
   | CDCL_Tableaux -> Format.fprintf ppf "CDCL-Tableaux"
 
 type theories_extensions =
-  | Sum
   | Adt
   | Arrays
   | Records
@@ -116,7 +115,6 @@ let equal_mode x y = match x, y with
 
 let th_ext_of_string ext =
   match ext with
-  | "Sum" -> Some Sum
   | "Adt" -> Some Adt
   | "Arrays" -> Some Arrays
   | "Records" -> Some Records
@@ -131,7 +129,6 @@ let th_ext_of_string ext =
 
 let string_of_th_ext ext =
   match ext with
-  | Sum -> "Sum"
   | Adt -> "Adt"
   | Arrays -> "Arrays"
   | Records -> "Records"

src/lib/util/util.mli

@@ -59,7 +59,6 @@ type sat_solver =
 val pp_sat_solver : Format.formatter -> sat_solver -> unit
 
 type theories_extensions =
-  | Sum
   | Adt
   | Arrays
   | Records