A Decision Procedure For EUF Formulas Based On Eager Encoding

The equality logic with uninterpreted functions(EUF)is a theory with strong expressive power,which has been occupied an important position in the formal method.In this paper,we study EUF theory without quantifiers,its decision problem has been proved to be NP-complete,and its decision procedure has been widely used in the formal verification community.Furthermore,some of the practical problems can be modeled as the decision problems of EUF formulas,such as equivalence verification for circuits,equivalence checking for programs,and verifying a compilation process with translation validationFor the satisfiability problems of EUF formulas,there are already SMT solvers that can decide them.However,the solvers can only solve a conjunction of equalities and uninterpreted functions with congruence closure.The objective of this paper is to decide the general EUF formulas,whose decision procedures can be roughly divided into two categories,lazy encoding and eager encoding.Lazy encoding is a method based on the interplay between a SAT solver and a theory solver,while eager encoding is a method that translates EUF formulas to propositional formulas and only uses a SAT solver.Obviously,the decision procedure based on eager encoding does not require the development of a specific theory solver for EUF theory,which has advantages in solving certain problems.It also promotes the option of deciding a combination of theories.In this paper,we study an eager encoding approach that a full reduction of EUF formulas to propositional formulas by Ackermann's method and algorithm based on a nonpolar equality graph.In this method,a large number of constraints are added,which is very difficult to implement.Therefore,we provide the DPLIB library written in C++ language for simplify development of the procedure.According to the above algorithms,we add some code and successfully compile it on Linux system.It proves that the method is a realizable decision procedure and can be called to solve the general EUF formulas.In addition,a list of conjunctions of equalities and uninterpreted functions is presented,and we use the two methods mentioned in this paper to solve them respectively.The experiment data show that the eager encoding is more efficient than the congruence closure algorithm.