“Datatypes with Shared Selectors” by Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark Barrett. In Proceedings of the 9^th International Joint Conference on Automated Reasoning (IJCAR '18), (Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, eds.), June 2018, pp. 591-608. Oxford, United Kingdom.
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.
BibTeX entry:
@inproceedings{RVB+18,
author = {Andrew Reynolds and Arjun Viswanathan and Haniel Barbosa and
Cesare Tinelli and Clark Barrett},
editor = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
title = {Datatypes with Shared Selectors},
booktitle = {Proceedings of the {\it 9^{th}} International Joint
Conference on Automated Reasoning (IJCAR '18)},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {591--608},
publisher = {Springer International Publishing},
month = jun,
year = {2018},
isbn = {978-3-319-94205-6},
doi = {10.1007/978-3-319-94205-6_39},
note = {Oxford, United Kingdom},
url = {http://theory.stanford.edu/~barrett/pubs/RVB+18.pdf}
}
(This webpage was created with bibtex2web.)