Skip to content

Commit

Permalink
HConstr: add tree_size debug print
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jun 27, 2024
1 parent aaee55b commit fe1476f
Showing 1 changed file with 8 additions and 0 deletions.
8 changes: 8 additions & 0 deletions kernel/hConstr.ml
Original file line number Diff line number Diff line change
Expand Up @@ -358,16 +358,24 @@ and of_constr_aux tbl local_env c =

let dbg = CDebug.create ~name:"hconstr" ()

let tree_size c =
let rec aux size c =
Constr.fold aux (size+1) c
in
aux 0 c

let of_constr env c =
let local_env = empty_env () in
let local_env = iterate push_unknown_rel (Environ.nb_rel env) local_env in
let tbl = Tbl.create 57 in
let c = of_constr tbl local_env c in
dbg Pp.(fun () ->
let stats = Tbl.stats tbl in
let tree_size = tree_size (self c) in
v 0 (
str "hashes = " ++ int stats.Tbl.hashes ++ spc() ++
str "bindings = " ++ int stats.Tbl.bindings ++ spc() ++
str "tree size = " ++ int tree_size ++ spc() ++
str "most_collisions = " ++ int stats.Tbl.most_collisions
)
);
Expand Down

0 comments on commit fe1476f

Please sign in to comment.