We introduce a decision procedure for satisfiability of equivalence
logic formulas with uninterpreted functions and predicates. In a
previous work, we presented a decision procedure for this
problem which starts by reducing the formula into a formula in
equality logic. As a second step, the formula structure was analyzed
in order to derive a small range of values for each variable that is
sufficient for preserving the formula's satisfiability. Then, a
standard BDD based tool was used in order to check the formula under
the new small domain. In this paper we change the reduction method
and perform a more careful analysis of the formula, which results in
significantly smaller domains. Both theoretical and experimental
results show that the new method is superior to the previous one and
to other methods that were suggested in the last few years.
