simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-27 20:04:49 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor(cc): disable path compression

Browse source
This commit is contained in:
Simon Cruanes 2018-08-18 14:52:00 -05:00
parent 1d212350ef
commit 6d2d1c91e8
1 changed files with 2 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/Congruence_closure.ml
View file

@ -78,20 +78,12 @@ let[@inline] size_ (r:repr) =
Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *) Invariant: [in_cc t ∧ do_cc t => forall u subterm t, in_cc u] *)
let[@inline] mem (cc:t) (t:term): bool = Term.Tbl.mem cc.tbl t let[@inline] mem (cc:t) (t:term): bool = Term.Tbl.mem cc.tbl t
(* TODO: remove path compression, point to new root explicitely during `union` *) (* find representative, recursively *)
(* find representative, recursively, and perform path compression *)
let rec find_rec cc (n:node) : repr = let rec find_rec cc (n:node) : repr =
if n==n.n_root then ( if n==n.n_root then (
n n
) else ( ) else (
let old_root = n.n_root in let root = find_rec cc n.n_root in
let root = find_rec cc old_root in
(* path compression *)
if root != old_root then (
on_backtrack cc (fun () -> n.n_root <- old_root);
n.n_root <- root;
);
root root
) )