Satisfiability Modulo Free Data Structures Combined with Bridging Functions

Abstract : Free Data Structures are finite semantic trees modulo equational axioms that are useful to represent classical data structures such as lists, multisets and sets. We study the satisfiability problem when free data structures are combined with bridging functions. We discuss the possibility to get a combination methodàmethod`methodà la Nelson-Oppen for these particular non-disjoint unions of theories. In order to handle satisfiability problems with disequalities, we investigate a form of sufficient surjectivity for the bridging functions.
Type de document :
Communication dans un congrès
Tim King and Ruzica Piskac. 14th International Workshop on Satisfiability Modulo Theories, affiliated with IJCAR 2016, Jul 2016, Coimbra, Portugal. CEUR-WS.org, pp.71--80, 2016, CEUR Workshop Proceedings
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01389228
Contributeur : Christophe Ringeissen <>
Soumis le : vendredi 28 octobre 2016 - 10:51:23
Dernière modification le : jeudi 11 janvier 2018 - 06:27:43

Fichier

combi-fds.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01389228, version 1

Collections

Citation

Raphaël Berthon, Christophe Ringeissen. Satisfiability Modulo Free Data Structures Combined with Bridging Functions. Tim King and Ruzica Piskac. 14th International Workshop on Satisfiability Modulo Theories, affiliated with IJCAR 2016, Jul 2016, Coimbra, Portugal. CEUR-WS.org, pp.71--80, 2016, CEUR Workshop Proceedings. 〈hal-01389228〉

Partager

Métriques

Consultations de la notice

182

Téléchargements de fichiers

93