Finite instantiations in equivalence logic with uninterpreted functions

Abstract

We introduce a decision procedure for satisfability of equivalence logic formulas with uninterpreted functions and predicates. In a previous work ([PRSS99]) we presented a decision procedure for this problem which started by reducing the formula into a formula in equal- ity logic. As a second step, the formula structure was analyzed in orderto derive a small range of values for each variable that is sucient for preserving the formula's satisfability. 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 signifcantly smaller domains. Both theoretical and experimental results show that the new method is superior to the previous one and to the method suggested in [BGV99].