Merge pull request #714 from Halbaroth/create-timers

Create timers
OCamlPro · Jul 10, 2023 · 9422063 · 9422063
2 parents 5c0b9f0 + ffe602d
commit 9422063
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 31 deletions.
diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml
@@ -212,12 +212,12 @@ let assume env _ la =
 let assume env uf la =
   if Options.get_timers() then
     try
-      Timers.exec_timer_start Timers.M_Arrays Timers.F_assume;
+      Timers.exec_timer_start Timers.M_Ite Timers.F_assume;
       let res =assume env uf la in
-      Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume;
+      Timers.exec_timer_pause Timers.M_Ite Timers.F_assume;
       res
     with e ->
-      Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume;
+      Timers.exec_timer_pause Timers.M_Ite Timers.F_assume;
       raise e
   else assume env uf la
 

diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml
@@ -43,22 +43,24 @@ type ty_module =
   | M_Expr
   | M_Triggers
   | M_Simplex
+  | M_Ite
 
 let mtag k = match k with
-  | M_None   -> 0
-  | M_Typing -> 1
-  | M_Sat    -> 2
-  | M_Match  -> 3
-  | M_CC     -> 4
-  | M_UF     -> 5
-  | M_Arith  -> 6
-  | M_Arrays -> 7
-  | M_Sum    -> 8
-  | M_Records-> 9
-  | M_AC     -> 10
-  | M_Expr-> 11
-  | M_Triggers->12
-  | M_Simplex->13
+  | M_None     -> 0
+  | M_Typing   -> 1
+  | M_Sat      -> 2
+  | M_Match    -> 3
+  | M_CC       -> 4
+  | M_UF       -> 5
+  | M_Arith    -> 6
+  | M_Arrays   -> 7
+  | M_Sum      -> 8
+  | M_Records  -> 9
+  | M_AC       -> 10
+  | M_Expr     -> 11
+  | M_Triggers -> 12
+  | M_Simplex  -> 13
+  | M_Ite      -> 14
 
 let nb_mtag = 14
 
@@ -109,20 +111,21 @@ let ftag f = match f with
 let nb_ftag = 20
 
 let string_of_ty_module k = match k with
-  | M_None   -> "None"
-  | 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_AC     -> "AC"
-  | M_Expr-> "Expr"
-  | M_Triggers->"Triggers"
-  | M_Simplex->"Simplex"
+  | M_None     -> "None"
+  | 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_AC       -> "AC"
+  | M_Expr     -> "Expr"
+  | M_Triggers -> "Triggers"
+  | M_Simplex  -> "Simplex"
+  | M_Ite      -> "Ite"
 
 let string_of_ty_function f = match f with
   | F_add           -> "add"

diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli
@@ -43,6 +43,7 @@ type ty_module =
   | M_Expr
   | M_Triggers
   | M_Simplex
+  | M_Ite
 
 type ty_function =
   | F_add