In this paper we describe our solver for systems of linear integer arithmetic logic. Such systems are commonly used in design verification applications and are classified under satisfiability modulo theories (SMT) problems. Recognizing the fact that in many such applications the majority of atoms are equalities or integer unit-two-variable inequalities (UTVPIs), we present a framework that integrates specialized theory solvers for those atoms within a SAT solver. The unique feature of our strategy is its simultaneous adoption of both a congruence-closure equality solver and a transitive-closure UTVPI solver to find a satisfiable set of those atoms. A full-scale ILP solver is then utilized to check the consistency of all integer constraints within the solution. Other notable features of our solver include its combined deduction and learning schemes that collectively make our solver distinct among similar solvers
展开▼
