Datatypes with Shared Selectors

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:

   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 = {}

(This webpage was created with bibtex2web.)