Computing a Complete Basis for Equalities Implied by a System of LRA Constraints

Martin Bromberger (1, 2, 3) , Christoph Weidenbach (3, 2)

1 Saarbrücken Graduate School of Computer Science
2 MPII - Max-Planck-Institut für Informatik
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

We present three new methods that investigate the equalities implied by a system of linear arithmetic constraints. Implied equalities can be used to simplify linear arithmetic constraints and are valuable in the context of Nelson-Oppen style combinations of theories. The first method efficiently checks whether a system of linear arithmetic constraints implies an equality at all. In case the system does, the method also returns a valid equality as an explanation. The second method uses the first method to compute a basis for all implied equalities, i.e., a finite representation of all equalities implied by the linear arithmetic constraints. The third method uses the second method to check efficiently whether a system of linear arithmetic constraints implies a given equality.

Domaines: Logique en informatique [cs.LO]

Martin Bromberger, Christoph Weidenbach. Computing a Complete Basis for Equalities Implied by a System of LRA Constraints. 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. pp.15-30. ⟨hal-01403214⟩