From d4c1c259d621ab3d189c5181c8b90fc427db3be4 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 8 Feb 2024 17:13:19 +0100 Subject: [PATCH] Factorize the timers in Relation --- src/lib/reasoners/adt_rel.ml | 10 +---- src/lib/reasoners/arrays_rel.ml | 10 +---- src/lib/reasoners/bitv_rel.ml | 10 +---- src/lib/reasoners/enum_rel.ml | 10 +---- src/lib/reasoners/intervalCalculus.ml | 14 +++--- src/lib/reasoners/ite_rel.ml | 10 +---- src/lib/reasoners/records_rel.ml | 2 + src/lib/reasoners/rel_utils.ml | 20 --------- src/lib/reasoners/relation.ml | 63 ++++++++++++++++----------- src/lib/reasoners/sig_rel.mli | 2 + 10 files changed, 56 insertions(+), 95 deletions(-) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index 2b12c04eb..b0f248c4d 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/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) diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml index 8680014f4..cb4f31bc6 100644 --- a/src/lib/reasoners/arrays_rel.ml +++ b/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) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index 52224d4d0..d40d3ec2c 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/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) diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index b6fa99497..3b6b42135 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/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) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index c79a044ce..54ea08468 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/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) diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml index 37f70603d..a73bdc8d5 100644 --- a/src/lib/reasoners/ite_rel.ml +++ b/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) diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml index 48d08e8fd..f50a99333 100644 --- a/src/lib/reasoners/records_rel.ml +++ b/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 = []} diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index b1007ef7c..f79d48d21 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/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 diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index b8e788a60..c632a3cb9 100644 --- a/src/lib/reasoners/relation.ml +++ b/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 (); diff --git a/src/lib/reasoners/sig_rel.mli b/src/lib/reasoners/sig_rel.mli index 401ab1c09..23040a4bf 100644 --- a/src/lib/reasoners/sig_rel.mli +++ b/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 ->