Computing All Implied Equalities via SMT-based Partition Refinement

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²) fresh subformulas. Simpler algorithms, in contrast, require O(N²) 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.