From caad52dbe63dcf493abcce47aea18286b9bd5e77 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 9 Oct 2023 16:40:19 +0200 Subject: [PATCH] Going back from hashtables to arrays --- alt-ergo-lib.opam | 1 + src/lib/dune | 2 +- src/lib/util/timers.ml | 221 +++++++++++++++++------------------------ 3 files changed, 94 insertions(+), 130 deletions(-) diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index 623bc3d8a..a1f4a97c4 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -28,6 +28,7 @@ depends: [ "ppx_blob" {>= "0.7.2"} "camlzip" {>= "1.07"} "odoc" {with-doc} + "ppx_deriving" ] conflicts: [ "ppxlib" {< "0.30.0"} diff --git a/src/lib/dune b/src/lib/dune index fe1f9080f..23c57e936 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -25,7 +25,7 @@ alt_ergo_prelude fmt ) - (preprocess (pps ppx_blob)) + (preprocess (pps ppx_blob ppx_deriving.show ppx_deriving.enum ppx_deriving.fold)) (preprocessor_deps (glob_files ../preludes/*.ae)) ; .mli only modules *also* need to be in this field diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index af4b3eade..bb9df94dd 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -28,6 +28,10 @@ (* *) (**************************************************************************) +(* To get rid of warnings produced by ppx_deriving. *) +[@@@warning "-32"] + +(* The type of modules, followed by the list of every element. *) type ty_module = | M_None | M_Typing @@ -44,26 +48,31 @@ type ty_module = | M_Triggers | M_Simplex | M_Ite - -let all_modules = [ - M_None; - M_Typing; - M_Sat; - M_Match; - M_CC; - M_UF; - M_Arith; - M_Arrays; - M_Sum; - M_Records; - M_AC; - M_Expr; - M_Triggers; - M_Simplex; - M_Ite -] - - +[@@deriving enum] + +let all_modules = + let l = [ + M_None; + M_Typing; + M_Sat; + M_Match; + M_CC; + M_UF; + M_Arith; + M_Arrays; + M_Sum; + M_Records; + M_AC; + M_Expr; + M_Triggers; + M_Simplex; + M_Ite + ] + in + assert ((List.length l) = max_ty_module + 1); + l + +(* The type of functions, followed by the list of every element. *) type ty_function = | F_add | F_add_lemma @@ -85,30 +94,34 @@ type ty_function = | F_new_facts | F_apply_subst | F_instantiate - -let all_functions = [ - F_add; - F_add_lemma; - F_add_predicate; - F_add_terms; - F_are_equal; - F_assume; - F_class_of; - F_leaves; - F_make; - F_m_lemmas; - F_m_predicates; - F_query; - F_solve; - F_subst; - F_union; - F_unsat; - F_none; - F_new_facts; - F_apply_subst; - F_instantiate; -] - +[@@deriving enum] + +let all_functions = + let l = [ + F_add; + F_add_lemma; + F_add_predicate; + F_add_terms; + F_are_equal; + F_assume; + F_class_of; + F_leaves; + F_make; + F_m_lemmas; + F_m_predicates; + F_query; + F_solve; + F_subst; + F_union; + F_unsat; + F_none; + F_new_facts; + F_apply_subst; + F_instantiate; + ] + in + assert ((List.length l) = max_ty_function + 1); + l let string_of_ty_module k = match k with | M_None -> "None" @@ -149,94 +162,44 @@ let string_of_ty_function f = match f with | F_apply_subst -> "apply_subst" | F_instantiate -> "instantiate" -module TimerTable = struct - module FTbl = Hashtbl.Make( - struct - type t = ty_function - - let hash = function - | F_add -> 0 - | F_add_lemma -> 1 - | F_assume -> 2 - | F_class_of -> 3 - | F_leaves -> 4 - | F_make -> 5 - | F_m_lemmas -> 6 - | F_m_predicates -> 7 - | F_query -> 8 - | F_solve -> 9 - | F_subst -> 10 - | F_union -> 11 - | F_unsat -> 12 - | F_add_predicate -> 13 - | F_add_terms -> 14 - | F_are_equal -> 15 - | F_none -> 16 - | F_new_facts -> 17 - | F_apply_subst -> 18 - | F_instantiate -> 19 - - let equal t t' = hash t = hash t' - end) - - module MTbl = Hashtbl.Make( - struct - type t = ty_module - - let hash = - function - | 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 equal t t' = hash t = hash t' - end) - - type t = float FTbl.t MTbl.t - - let create = MTbl.create - - let clear = MTbl.clear - - (** Returns the timer value associated to the module [m] - and the function [f]. *) +module TimerTable : sig + (** The table of timers (module -> function -> float). *) + type t + + (** Clears the table. *) + val clear : t -> unit + + (** Creates a new type of tables. *) + val create : unit -> t + + (** Returns the time stored in the table. If it has never been + stored, returns 0.. *) + val get : t -> ty_module -> ty_function -> float + + (** Sets the time spend to a given function in a given module.. *) + val set : t -> ty_module -> ty_function -> float -> unit + + (** Gets the total time spent in a given module. *) + val get_sum : t -> ty_module -> float +end = struct + type t = float array array + + let create () = + Array.init + max_ty_module + (fun _ -> Array.init max_ty_function (fun _ -> 0.)) + + let clear = + Array.iter (fun a -> Array.iteri (fun j _ -> a.(j) <- 0.) a) + let get t m f = - match MTbl.find_opt t m with - | None -> 0. - | Some t -> - match FTbl.find_opt t f with - | None -> 0. - | Some f -> f - - (** Sets the timer value associated to the module [m] - and the function [f]. *) + t.(ty_module_to_enum m).(ty_function_to_enum f) + let set t m f v = - let ftbl = - match MTbl.find_opt t m with - | None -> - let new_tbl = FTbl.create 1 in - MTbl.add t m new_tbl; - new_tbl - | Some tbl -> tbl - in - FTbl.add ftbl f v + t.(ty_module_to_enum m).(ty_function_to_enum f) <- v let get_sum t m = - match MTbl.find_opt t m with - | None -> 0. - | Some ft -> FTbl.fold (fun _ -> (+.)) ft 0. + Array.fold_left (+.) 0. t.(ty_module_to_enum m) end type t = { @@ -262,7 +225,7 @@ let empty () = { cur_t = (M_None, F_none, 0); cur_u = 0.0; stack = []; - z = TimerTable.create 5 + z = TimerTable.create () } (** reset the references of the given env to empty **)