simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

perf(cc): path compression

Browse source
This commit is contained in:
Simon Cruanes 2019-02-16 15:28:16 -06:00
parent ac030641db
commit 365aedb138
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/cc/Congruence_closure.ml
View file

@ -276,13 +276,14 @@ module Make(A: ARG) = struct
let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
(* find representative, recursively *) (* find representative, recursively *)
let[@unroll 1] rec find_rec (n:node) : repr = let[@unroll 2] rec find_rec (n:node) : repr =
if n==n.n_root then ( if n==n.n_root then (
n n
) else ( ) else (
(* TODO: path compression, assuming backtracking restores equiv classes
properly *)
let root = find_rec n.n_root in let root = find_rec n.n_root in
if root != n.n_root then (
n.n_root <- root; (* path compression *)
);
root root
) )