The effect is that two terms can be compared several times, thereby causing duplication of work. The proposal is to maintain a local cache from addresses of terms (t1, t2) to booleans indicating results of their comparison. Homeomorphic embedding will thus have O(size(t1) * size(t2)) worst-case time complexity.
This cache can be used in conjunction with the already implemented size cache.
The following line exhibits a non-linear control flow:
https://github.com/mazeppa-dev/mazeppa/blob/a9f0350390a2c6c7e3eea74c38a9bf3384eb7985/lib/algebra/homeomorphic_emb.ml#L60
The effect is that two terms can be compared several times, thereby causing duplication of work. The proposal is to maintain a local cache from addresses of terms (t1, t2) to booleans indicating results of their comparison. Homeomorphic embedding will thus have O(size(t1) * size(t2)) worst-case time complexity.
This cache can be used in conjunction with the already implemented size cache.