Skip to content

Commit 69dc00f

Browse files
Add Clone() to UnionFind, use in UnifyTermsExtend
Pre-allocates map capacity when copying the union-find structure, avoiding unnecessary rehashing during term unification. Based on github.com//pull/91 Co-Authored-By: apocalypse9949 <dchittibabu641@gmail.com>
1 parent 146d96b commit 69dc00f

1 file changed

Lines changed: 12 additions & 4 deletions

File tree

unionfind/unionfind.go

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -161,16 +161,24 @@ func UnifyTerms(xs []ast.BaseTerm, ys []ast.BaseTerm) (UnionFind, error) {
161161
return uf, unifyTermsUpdate(newXs, newYs, uf)
162162
}
163163

164+
// Clone returns a new UnionFind that is a copy of this one.
165+
func (uf UnionFind) Clone() UnionFind {
166+
newUf := UnionFind{make(map[ast.BaseTerm]ast.BaseTerm, len(uf.parent))}
167+
for k, v := range uf.parent {
168+
newUf.parent[k] = v
169+
}
170+
return newUf
171+
}
172+
164173
// UnifyTermsExtend unifies two same-length lists of relational terms, returning
165174
// an extended UnionFind. It does not handle apply-expressions.
175+
// The caller needs to ensure that none of the variables is "_" and none of the variables appears among the terms.
176+
// The caller also needs to ensure that the base UnionFind is consistent with the new terms.
166177
func UnifyTermsExtend(xs []ast.BaseTerm, ys []ast.BaseTerm, base UnionFind) (UnionFind, error) {
167178
if len(xs) != len(ys) {
168179
return UnionFind{}, fmt.Errorf("not of equal size")
169180
}
170-
uf := UnionFind{make(map[ast.BaseTerm]ast.BaseTerm)}
171-
for k, v := range base.parent {
172-
uf.parent[k] = v
173-
}
181+
uf := base.Clone()
174182
var newXs []ast.BaseTerm
175183
var newYs []ast.BaseTerm
176184
for i, x := range xs {

0 commit comments

Comments
 (0)