Efficient Instantiation Techniques in SMT (Work In Progress)

Abstract : In SMT solving one generally applies heuristic instantiation to handle quantified formulas. This has the side effect of producing many spurious instances and may lead to loss of performance. Therefore deriving both fewer and more meaningful instances as well as eliminating or dismissing , i.e., keeping but ignoring, those not significant for the solving are desirable features for dealing with first-order problems. This paper presents preliminary work on two approaches: the implementation of an efficient instantiation framework with an incomplete goal-oriented search; and the introduction of dismissing criteria for heuristic instances. Our experiments show that while the former improves performance in general the latter is highly dependent on the problem structure, but its combination with the classic strategy leads to competitive results w.r.t. state-of-the-art SMT solvers in several benchmark libraries.
Type de document :
Communication dans un congrès
PAAR 2016 - 5th Workshop on Practical Aspects of Automated Reasoning co-located with IJCAR 2016 - 8th International Joint Conference on Automated Reasoning, Jul 2016, Coimbra, Portugal. Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 1635, pp.1-10, 2016, CEUR Workshop Proceedings
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01388976
Contributeur : Haniel Barbosa <>
Soumis le : jeudi 27 octobre 2016 - 18:26:23
Dernière modification le : mercredi 18 juillet 2018 - 09:46:25

Fichier

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

Licence


Domaine public

Identifiants

  • HAL Id : hal-01388976, version 1

Collections

Citation

Haniel Barbosa. Efficient Instantiation Techniques in SMT (Work In Progress). PAAR 2016 - 5th Workshop on Practical Aspects of Automated Reasoning co-located with IJCAR 2016 - 8th International Joint Conference on Automated Reasoning, Jul 2016, Coimbra, Portugal. Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), 1635, pp.1-10, 2016, CEUR Workshop Proceedings. 〈hal-01388976〉

Partager

Métriques

Consultations de la notice

95

Téléchargements de fichiers

93