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.
Technical report 2001