“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.)