diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2013-02-05 00:49:39 -0500 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2013-02-05 00:49:39 -0500 |
| commit | 76805f8b4690093888bbb3d68e4d5c2c6ff221de (patch) | |
| tree | 4c650ccb0b6c44035daaafdfbd3026e117eb9d4b /src/theory/bv/slicer.cpp | |
| parent | 8aaee8d5acce9887329f3e5a6fdeb425e428ec79 (diff) | |
Added path compression and caching for getBaseDecomposition.
Diffstat (limited to 'src/theory/bv/slicer.cpp')
| -rw-r--r-- | src/theory/bv/slicer.cpp | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 87295e8f6..f41612df3 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -220,10 +220,13 @@ void UnionFind::merge(TermId t1, TermId t2) { d_statistics.d_numRepresentatives += -1; } -TermId UnionFind::find(TermId id) const { +TermId UnionFind::find(TermId id) { TermId repr = getRepr(id); - if (repr != UndefinedId) - return find(repr); + if (repr != UndefinedId) { + TermId find_id = find(repr); + setRepr(id, find_id); + return find_id; + } return id; } /** |