| ||||
| ||||
![]() Title:Datatypes with Shared Selectors Conference:IJCAR-2018 Tags:Datatypes, Decision Procedures, SMT and Syntax-guided Synthesis 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 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 solver CVC4 on syntax-guided synthesis and other domains shows evidence that the use of shared selectors improves state-of-the-art SMT-based approaches for datatype constraints. Datatypes with Shared Selectors ![]() Datatypes with Shared Selectors | ||||
Copyright © 2002 – 2025 EasyChair |