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.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2017, 51 (3), pp.433-461. 〈10.1007/s10703-017-0278-7〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01656397
Contributeur : Stephan Merz <>
Soumis le : mardi 5 décembre 2017 - 15:58:13
Dernière modification le : lundi 11 décembre 2017 - 11:17:34

Fichier

paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

23

Téléchargements de fichiers

5