From 365aedb1382151d8b2a8cd6ac4381e8a920032be Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sat, 16 Feb 2019 15:28:16 -0600
Subject: [PATCH] perf(cc): path compression

---
 src/cc/Congruence_closure.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/cc/Congruence_closure.ml b/src/cc/Congruence_closure.ml
index eab9fe76..6a4821af 100644
--- a/src/cc/Congruence_closure.ml
+++ b/src/cc/Congruence_closure.ml
@@ -276,13 +276,14 @@ module Make(A: ARG) = struct
   let[@inline] mem (cc:t) (t:term): bool = T_tbl.mem cc.tbl t
 
   (* 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 (
       n
     ) else (
-      (* TODO: path compression, assuming backtracking restores equiv classes
-         properly *)
       let root = find_rec n.n_root in
+      if root != n.n_root then (
+        n.n_root <- root; (* path compression *)
+      );
       root
     )