New Techniques for Linear Arithmetic: Cubes and Equalities

Abstract : We present several new techniques for linear arithmetic constraint solving. They are all based on the linear cube transformation, a method presented here, which allows us to efficiently determine whether a system of linear arithmetic constraints contains a hypercube of a given edge length. Our first findings based on this transformation are two sound tests that find integer solutions for linear arithmetic constraints. While many complete methods search along the problem surface for a solution, these tests use cubes to explore the interior of the problems. The tests are especially efficient for constraints with a large number of integer solutions, e.g., those with infinite lattice width. Inside the SMT-LIB benchmarks, we have found almost one thousand problem instances with infinite lattice width. Experimental results confirm that our tests are superior on these instances compared to several state-of-the-art SMT solvers. We also discovered that the linear cube transformation can be used to investigate the equalities implied by a system of linear arithmetic constraints. For this purpose, we developed a method that computes a basis for all implied equalities, i.e., a finite representation of all equalities implied by the linear arithmetic constraints. The equality basis has several applications. For instance, it allows us to verify whether a system of linear arithmetic constraints implies a given equality. This is valuable in the context of Nelson-Oppen style combinations of theories.
Document type :
Journal articles
Liste complète des métadonnées

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/hal-01656397
Contributor : Stephan Merz <>
Submitted on : Tuesday, December 5, 2017 - 3:58:13 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:04 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Citation

Martin Bromberger, Christoph Weidenbach. New Techniques for Linear Arithmetic: Cubes and Equalities. Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.433-461. ⟨10.1007/s10703-017-0278-7⟩. ⟨hal-01656397⟩

Share

Metrics

Record views

138

Files downloads

48