Factorize the timers in Shostak

src/lib/reasoners/ac.ml

@@ -200,10 +200,6 @@ module Make (X : Sig.X) = struct
          got %i (%a)." (List.length xs) Expr.print_list xs;
       assert false
 
-  let make t =
-    Timers.with_timer Timers.M_AC Timers.F_make @@ fun () ->
-    make t
-
   let is_mine_symb sy _ = (not @@ Options.get_no_ac ()) && Sy.is_ac sy
 
   let type_info { t = ty; _ } = ty

src/lib/reasoners/adt.ml

@@ -80,6 +80,8 @@ module Shostak (X : ALIEN) = struct
 
   let name = "Adt"
 
+  let timer = Timers.M_Adt
+
   [@@ocaml.ppwarning "XXX: IsConstr not interpreted currently. Maybe \
                       it's OK"]
   let is_mine_symb sy ty =

src/lib/reasoners/arith.ml

@@ -87,6 +87,8 @@ module Shostak
 
   let name = "arith"
 
+  let timer = Timers.M_Arith
+
   (*BISECT-IGNORE-BEGIN*)
   module Debug = struct
 
@@ -742,14 +744,6 @@ module Shostak
     with Unsafe ->
       assert false
 
-  let make t =
-    Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () ->
-    make t
-
-  let solve r1 r2 pb =
-    Timers.with_timer Timers.M_Arith Timers.F_solve @@ fun () ->
-    solve r1 r2 pb
-
   let print = P.print
 
   let fully_interpreted sb =

src/lib/reasoners/bitv.ml

@@ -343,6 +343,8 @@ module Shostak(X : ALIEN) = struct
 
   let name = "bitv"
 
+  let timer = Timers.M_Bitv
+
   let is_mine_symb sy _ =
     match sy with
     | Sy.Bitv _

src/lib/reasoners/enum.ml

@@ -52,6 +52,8 @@ module Shostak (X : ALIEN) = struct
 
   let name = "Sum"
 
+  let timer = Timers.M_Sum
+
   let is_mine_symb sy ty =
     match sy, ty with
     | Sy.Op (Sy.Constr _), Ty.Tsum _ -> true
@@ -177,10 +179,6 @@ module Shostak (X : ALIEN) = struct
   let solve r1 r2 pb =
     Sig.{pb with sbt = List.rev_append (solve_bis r1 r2) pb.sbt}
 
-  let solve r1 r2 pb =
-    Timers.with_timer Timers.M_Sum Timers.F_solve @@ fun () ->
-    solve r1 r2 pb
-
   let assign_value _ _ _ =
     (* As the models of this theory are finite, the case-split
        mechanism can and does exhaust all the possible values.

src/lib/reasoners/records.ml

@@ -49,6 +49,8 @@ module Shostak (X : ALIEN) = struct
 
   let name = "records"
 
+  let timer = Timers.M_Records
+
   type t = X.r abstract
   type r = X.r
 
@@ -386,14 +388,6 @@ module Shostak (X : ALIEN) = struct
     | Access _ , _ -> assert false
     | _ , Access _ -> assert false
 
-  let make t =
-    Timers.with_timer Timers.M_Records Timers.F_make @@ fun () ->
-    make t
-
-  let solve r1 r2 pb =
-    Timers.with_timer Timers.M_Records Timers.F_solve @@ fun () ->
-    solve r1 r2 pb
-
   let assign_value t _ eq =
     match embed t with
     | Access _ -> None

src/lib/reasoners/shostak.ml

@@ -383,19 +383,33 @@ struct
       AC.is_mine_symb sb ty
     with
     | true  , false , false, false, false, false ->
+      Timers.with_timer Timers.M_Arith Timers.F_make @@ fun () ->
       ARITH.make t
+
     | false , true  , false, false, false, false ->
+      Timers.with_timer Timers.M_Records Timers.F_make @@ fun () ->
       RECORDS.make t
+
     | false , false , true  , false, false, false ->
+      Timers.with_timer Timers.M_Bitv Timers.F_make @@ fun () ->
       BITV.make t
+
     | false , false , false , true , false, false ->
+      Timers.with_timer Timers.M_Sum Timers.F_make @@ fun () ->
       ENUM.make t
+
     | false , false , false , false, true , false ->
+      Timers.with_timer Timers.M_Adt Timers.F_make @@ fun () ->
       ADT.make t
+
     | false , false , false , false, false, true  ->
+      Timers.with_timer Timers.M_AC Timers.F_make @@ fun () ->
       AC.make t
+
     | false , false , false , false, false, false ->
+      Timers.with_timer Timers.M_None Timers.F_make @@ fun () ->
       term_embed t, []
+
     | _ -> assert false
 
   let fully_interpreted sb ty =
@@ -544,14 +558,31 @@ struct
         let tyb = CX.type_info rb in
         Debug.assert_have_mem_types tya tyb;
         let pb = match tya with
-          | Ty.Tint | Ty.Treal -> ARITH.solve ra rb pb
-          | Ty.Trecord _       -> RECORDS.solve ra rb pb
-          | Ty.Tbitv _         -> BITV.solve ra rb pb
-          | Ty.Tsum _          -> ENUM.solve ra rb pb
+          | Ty.Tint | Ty.Treal ->
+            Timers.with_timer ARITH.timer Timers.F_solve @@ fun () ->
+            ARITH.solve ra rb pb
+
+          | Ty.Trecord _       ->
+            Timers.with_timer RECORDS.timer Timers.F_solve @@ fun () ->
+            RECORDS.solve ra rb pb
+
+          | Ty.Tbitv _         ->
+            Timers.with_timer BITV.timer Timers.F_solve @@ fun () ->
+            BITV.solve ra rb pb
+
+          | Ty.Tsum _          ->
+            Timers.with_timer ENUM.timer Timers.F_solve @@ fun () ->
+            ENUM.solve ra rb pb
+
           (*| Ty.Tunit           -> pb *)
+
           | Ty.Tadt _ when not (Options.get_disable_adts()) ->
+            Timers.with_timer ADT.timer Timers.F_solve @@ fun () ->
             ADT.solve ra rb pb
-          | _                  -> solve_uninterpreted ra rb pb
+
+          | _                  ->
+            Timers.with_timer Timers.M_None Timers.F_solve @@ fun () ->
+            solve_uninterpreted ra rb pb
         in
         solve_list pb
         [@ocaml.ppwarning "TODO: a simple way of handling equalities \

src/lib/reasoners/sig.mli

@@ -44,6 +44,8 @@ module type SHOSTAK = sig
   (** Name of the theory*)
   val name : string
 
+  val timer : Timers.ty_module
+
   (** return true if the symbol and the type are owned by the theory*)
   val is_mine_symb : Symbols.t -> Ty.t -> bool