Factorize the timers in Relation

src/lib/reasoners/adt_rel.ml

@@ -46,6 +46,8 @@ module LR = Uf.LX
 module SLR = Set.Make(LR)
 module MHs = Hs.Map
 
+let timer = Timers.M_Adt
+
 type t =
   {
     classes : E.Set.t list;
@@ -854,11 +856,3 @@ let query env uf (ra, _, ex, _) =
     | Ex.Inconsistent (expl, classes) -> Some (expl, classes)
 
 (* ################################################################ *)
-
-include Rel_utils.Instrumentation (struct
-    type nonrec t = t
-
-    let mod_ = Timers.M_Adt
-    let assume = assume
-    let query = query
-  end)

src/lib/reasoners/arrays_rel.ml

@@ -81,6 +81,8 @@ module TBS = struct
   let add k v mp = add k (S.add v (find k mp)) mp
 end
 
+let timer = Timers.M_Arrays
+
 type t =
   {gets  : G.t;               (* l'ensemble des "get" croises*)
    tbset : S.t TBS.t ;        (* map t |-> set(t,-,-) *)
@@ -439,11 +441,3 @@ let assume_th_elt t th_elt _ =
   | Util.Arrays ->
     failwith "This Theory does not support theories extension"
   | _ -> t
-
-include Rel_utils.Instrumentation (struct
-    type nonrec t = t
-
-    let mod_ = Timers.M_Arrays
-    let assume = assume
-    let query = query
-  end)

src/lib/reasoners/bitv_rel.ml

@@ -34,6 +34,8 @@ module Sy = Symbols
 module X = Shostak.Combine
 module L = Xliteral
 
+let timer = Timers.M_Bitv
+
 (* Currently we only compute, but in the future we may want to perform the same
    simplifications as in [Bitv.make]. We currently don't, because we don't
    really have a way to share code that uses polynome between the theory and the
@@ -715,11 +717,3 @@ let assume_th_elt t th_elt _ =
   | Util.Bitv ->
     failwith "This Theory does not support theories extension"
   | _ -> t
-
-include Rel_utils.Instrumentation (struct
-    type nonrec t = t
-
-    let mod_ = Timers.M_Bitv
-    let assume = assume
-    let query = query
-  end)

src/lib/reasoners/enum_rel.ml

@@ -32,6 +32,8 @@ module A  = Xliteral
 module L  = List
 module Hs = Hstring
 
+let timer = Timers.M_Sum
+
 type 'a abstract = 'a Enum.abstract =
   | Cons of Hs.t * Ty.t
   | Alien of 'a
@@ -346,11 +348,3 @@ let assume_th_elt t th_elt _ =
   | Util.Sum ->
     failwith "This Theory does not support theories extension"
   | _ -> t
-
-include Rel_utils.Instrumentation (struct
-    type nonrec t = t
-
-    let mod_ = Timers.M_Sum
-    let assume = assume
-    let query = query
-  end)

src/lib/reasoners/intervalCalculus.ml

@@ -100,6 +100,8 @@ end
 
 module Sim = OcplibSimplex.Basic.Make(SimVar)(Numbers.Q)(Explanation)
 
+let timer = Timers.M_Arith
+
 type t = {
   inequations : P.t Inequalities.t MPL.t;
   monomes: (I.t * SX.t) MX0.t;
@@ -2535,19 +2537,13 @@ let assume_th_elt t th_elt dep =
 
   | _ -> t
 
+let assume = assume ~query:false
+
 let instantiate ~do_syntactic_matching env uf selector =
-  Timers.with_timer Timers.M_Arith Timers.F_instantiate @@ fun () ->
+  Timers.with_timer timer Timers.F_instantiate @@ fun () ->
   instantiate ~do_syntactic_matching env uf selector
 
 let reinit_cache () =
   let module Oracle = (val get_oracle ()) in
   Oracle.reset_age_cpt ();
   EM.reinit_caches ()
-
-include Rel_utils.Instrumentation (struct
-    type nonrec t = t
-
-    let mod_ = Timers.M_Arith
-    let assume = assume ~query:false
-    let query = query
-  end)

src/lib/reasoners/ite_rel.ml

@@ -54,6 +54,8 @@ module TB =
         if c <> 0 then c else Stdlib.compare b1 b2
     end)
 
+let timer = Timers.M_Ite
+
 (* The present theory simplifies the ite terms t of the form
     ite(pred, t1, t2)
    where pred is an assumed predicate by introducing the equation
@@ -219,11 +221,3 @@ let new_terms _ = E.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
 
 let assume_th_elt t _ _ = t
-
-include Rel_utils.Instrumentation (struct
-    type nonrec t = t
-
-    let mod_ = Timers.M_Ite
-    let assume = assume
-    let query = query
-  end)

src/lib/reasoners/records_rel.ml

@@ -30,6 +30,8 @@
 
 type t = unit
 
+let timer = Timers.M_Records
+
 let empty _ = ()
 let assume _ _ _ =
   (), { Sig_rel.assume = []; remove = []}

src/lib/reasoners/rel_utils.ml

@@ -376,23 +376,3 @@ end = struct
     let dom = CS.fold Constraint.propagate bcs.fresh dom in
     { bcs with fresh = CS.empty }, dom
 end
-
-module Instrumentation (R : sig
-    open Sig_rel
-    type t
-
-    val mod_ : Timers.ty_module
-
-    val assume : t ->
-      Uf.t -> (Shostak.Combine.r input) list -> t * Shostak.Combine.r result
-
-    val query  : t -> Uf.t -> Shostak.Combine.r input -> Th_util.answer
-  end) = struct
-  let assume env uf la =
-    Timers.with_timer R.mod_ Timers.F_assume @@ fun () ->
-    R.assume env uf la
-
-  let query env uf la =
-    Timers.with_timer R.mod_ Timers.F_query @@ fun () ->
-    R.query env uf la
-end

src/lib/reasoners/relation.ml

@@ -46,6 +46,8 @@ module Rel6 : Sig_rel.RELATION = Adt_rel
 
 module Rel7 : Sig_rel.RELATION = Ite_rel
 
+let timer = Timers.M_None
+
 type t = {
   r1: Rel1.t;
   r2: Rel2.t;
@@ -74,19 +76,33 @@ let (|@|) l1 l2 =
 let assume env uf sa =
   Options.exec_thread_yield ();
   let env1, ({ assume = a1; remove = rm1}:_ Sig_rel.result) =
-    Rel1.assume env.r1 uf sa in
+    Timers.with_timer Rel1.timer Timers.F_assume @@ fun () ->
+    Rel1.assume env.r1 uf sa
+  in
   let env2, ({ assume = a2; remove = rm2}:_ Sig_rel.result) =
-    Rel2.assume env.r2 uf sa in
+    Timers.with_timer Rel2.timer Timers.F_assume @@ fun () ->
+    Rel2.assume env.r2 uf sa
+  in
   let env3, ({ assume = a3; remove = rm3}:_ Sig_rel.result) =
-    Rel3.assume env.r3 uf sa in
+    Timers.with_timer Rel3.timer Timers.F_assume @@ fun () ->
+    Rel3.assume env.r3 uf sa
+  in
   let env4, ({ assume = a4; remove = rm4}:_ Sig_rel.result) =
-    Rel4.assume env.r4 uf sa in
+    Timers.with_timer Rel4.timer Timers.F_assume @@ fun () ->
+    Rel4.assume env.r4 uf sa
+  in
   let env5, ({ assume = a5; remove = rm5}:_ Sig_rel.result) =
-    Rel5.assume env.r5 uf sa in
+    Timers.with_timer Rel5.timer Timers.F_assume @@ fun () ->
+    Rel5.assume env.r5 uf sa
+  in
   let env6, ({ assume = a6; remove = rm6}:_ Sig_rel.result) =
-    Rel6.assume env.r6 uf sa in
+    Timers.with_timer Rel6.timer Timers.F_assume @@ fun () ->
+    Rel6.assume env.r6 uf sa
+  in
   let env7, ({ assume = a7; remove = rm7}:_ Sig_rel.result) =
-    Rel7.assume env.r7 uf sa in
+    Timers.with_timer Rel7.timer Timers.F_assume @@ fun () ->
+    Rel7.assume env.r7 uf sa
+  in
   {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7},
   ({ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6 |@| a7;
      remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 |@| rm7}
@@ -103,26 +119,21 @@ let assume_th_elt env th_elt dep =
   let env7 = Rel7.assume_th_elt env.r7 th_elt dep in
   {r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7}
 
+let try_query (type a) (module R : Sig_rel.RELATION with type t = a) env uf a
+    k =
+  match Timers.with_timer R.timer Timers.F_query
+    @@ fun () -> R.query env uf a with
+  | Some r -> Some r
+  | None -> k ()
+
 let query env uf a =
-  Options.exec_thread_yield ();
-  match Rel1.query env.r1 uf a with
-  | Some _ as ans -> ans
-  | None ->
-    match Rel2.query env.r2 uf a with
-    | Some _ as ans -> ans
-    | None ->
-      match Rel3.query env.r3 uf a with
-      | Some _ as ans -> ans
-      | None ->
-        match Rel4.query env.r4 uf a with
-        | Some _ as ans -> ans
-        | None ->
-          match Rel5.query env.r5 uf a with
-          | Some _ as ans -> ans
-          | None ->
-            match Rel6.query env.r6 uf a with
-            | Some _ as ans -> ans
-            | None -> Rel7.query env.r7 uf a
+  try_query (module Rel1) env.r1 uf a @@ fun () ->
+  try_query (module Rel2) env.r2 uf a @@ fun () ->
+  try_query (module Rel3) env.r3 uf a @@ fun () ->
+  try_query (module Rel4) env.r4 uf a @@ fun () ->
+  try_query (module Rel5) env.r5 uf a @@ fun () ->
+  try_query (module Rel6) env.r6 uf a @@ fun () ->
+  try_query (module Rel7) env.r7 uf a @@ fun () -> None
 
 let case_split env uf ~for_model =
   Options.exec_thread_yield ();

src/lib/reasoners/sig_rel.mli

@@ -52,6 +52,8 @@ type 'a result = {
 module type RELATION = sig
   type t
 
+  val timer : Timers.ty_module
+
   val empty : Expr.Set.t list -> t
 
   val assume : t ->