Building small equality graphs for deciding equality logic with uninterpreted functions

The logic of Equalities with Uninterpreted Functions is used in the formal verification community mainly for proofs of equivalence: proving that two versions of a hardware design are the same, or that input and output of a compiler are semantically equivalent are two prominent examples of such proofs. We introduce a new decision procedure for this logic that generalizes two leading decision procedures that were published in the last few years: the Positive Equality approach suggested by Bryant et al. [Exploiting positive equality in a logic of equality with uninterpreted functions, in: Proc. 11th Intl. Conference on Computer Aided Verification (CAV’99), 1999], and the Range-Allocation algorithm suggested by Pnueli et al. [The small model property: how small can it be? Information and Computation 178 (1) (2002) 279–293]. Both of these methods reduce this logic to pure Equality Logic (without Uninterpreted Functions), and then, due to the small model property that such formulas have, find a small domain to each variable that is sufficiently large to maintain the satisfiability of the formula. The state-space spanned by these domains is then traversed with a BDD-based engine. The Positive Equality approach identifies terms that have a certain characteristic in the original formula (before the reduction to pure Equality Logic) and replaces them with unique constants. The Range-Allocation algorithm analyzes the structure of the formula after the reduction to equality logic with a graph-based procedure to allocate a small set of values to each variable. The former, therefore, has an advantage when a large subset of the terms can be replaced with constants, and disadvantage in the other cases. In this paper we essentially merge the two methods, while improving both with a more careful analysis of the formula’s structure. We show that the new method is provably dominant over both methods, theoretically as well as empirically.1