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

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.
Type de document :
Communication dans un congrès
Tim King and Ruzica Piskac. 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. 1617, pp.15-30, 2016, CEUR Workshop Proceedings
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01403214
Contributeur : Stephan Merz <>
Soumis le : vendredi 25 novembre 2016 - 15:21:04
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : lundi 20 mars 2017 - 18:34:31

Fichier

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

Identifiants

  • 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. Tim King and Ruzica Piskac. 14th International Workshop on Satisfiability Modulo Theories, 2016, Coimbra, Portugal. 1617, pp.15-30, 2016, CEUR Workshop Proceedings. 〈hal-01403214〉

Partager

Métriques

Consultations de la notice

145

Téléchargements de fichiers

30