A BDD-representation for the logic of equality and uninterpreted functions (a full version with proofs).

The logic of equality and uninterpreted functions (EUF) has been proposed for processor verification. This paper presents a new data structure called Binary Decision Diagrams for representing EUF formulas (EUF-BDDs). We define EUF-BDDs similar to BDDs, but we allow equalities between terms as labels instead of Boolean variables. We provide an approach to build a reduced ordered EUF-BDD (EUF-ROBDD) and prove that every path to a leaf is satisfiable by construction. Moreover, EUF-ROBDDs are logically equivalent representations of EUF-formulae, so they can also be used to represent state spaces in symbolic model checking with data