Computing All Implied Equalities via SMT-based Partition Refinement

ABSTRACT. Consequence finding is used in many applications of deduction. This paper develops and evaluates an optimized SMT-based algorithm 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 algorithm is commonly 10-100x faster than simpler folklore algorithms. The new algorithm is based on incrementally refining an initially coarse partition, and is entirely driven by models extracted from a solver to maximize the benefit of model generation capabilities. Our new algorithm 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. Our algorithm demonstrates low space overhead for SLAyer, yet we also describe an asymptotically superior algorithm that requires O(N) solver calls and only O(N log N) fresh subformulas.