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

Martin Bromberger 1, 2, 3 Christoph Weidenbach 3, 2
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-01403214
Contributor : Stephan Merz <>
Submitted on : Friday, November 25, 2016 - 3:21:04 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM
Long-term archiving on : Monday, March 20, 2017 - 6:34:31 PM

File

SMT2016.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01403214, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

221

Files downloads

69