Consequence finding is used in many applications of deduction. This paper
develops and evaluates a suite of optimized SMT-based algorithms for computing
equality consequences over arbitrary formulas and theories supported by SMT
solvers. It is inspired by an application in the SLAyer analyzer, where our new
algorithms are commonly 10-100x faster than simpler algorithms. The main idea is
to incrementally refine an initially coarse partition using models extracted from
a solver. Our approach requires only O(N) solver calls for N terms, but in the
worst case creates O(N^{2}) fresh subformulas. Simpler algorithms, in
contrast, require O(N^{2}) solver calls. We also describe an
asymptotically superior algorithm that requires O(N) solver calls and only O(N
log N) fresh subformulas. We evaluate algorithms which reduce the number of
fresh formulas required either by using specialized data structures or by relying
on subformula sharing.