Book chapter
Datatypes with Shared Selectors
Automated Reasoning, pp.591-608
Lecture Notes in Computer Science, Springer International Publishing
06/30/2018
DOI: 10.1007/978-3-319-94205-6_39
Abstract
We introduce a new theory of algebraic datatypes where selector symbols can be shared between multiple constructors, thereby reducing the number of terms considered by current SMT-based solving approaches. We show that the satisfiability problem for the traditional theory of algebraic datatypes can be reduced to problems where selectors are mapped to shared symbols based on a transformation provided in this paper. The use of shared selectors addresses a key bottleneck for an SMT-based enumerative approach to the Syntax-Guided Synthesis (SyGuS) problem. Our experimental evaluation of an implementation of the new theory in the SMT solver cvc4 on syntax-guided synthesis and other domains provides evidence that the use of shared selectors improves state-of-the-art SMT-based approaches for constraints over algebraic datatypes.
Details
- Title: Subtitle
- Datatypes with Shared Selectors
- Creators
- Andrew Reynolds - University of Iowa, Iowa City, USAArjun Viswanathan - University of Iowa, Iowa City, USAHaniel Barbosa - University of Iowa, Iowa City, USACesare Tinelli - University of Iowa, Iowa City, USAClark Barrett - Department of Computer Science, Stanford University, Stanford, USA
- Resource Type
- Book chapter
- Publication Details
- Automated Reasoning, pp.591-608
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-94205-6_39
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 06/30/2018
- Academic Unit
- Computer Science
- Record Identifier
- 9984002353802771
Metrics
25 Record Views