Syntax-guided synthesis has been a prevalent theme in various computer-aided programming systems. However, the domain of bit-vector synthesis poses several unique challenges that have not yet been sufficiently addressed and resolved. In this paper, we propose a novel synthesis approach that incorporates a distinct enumeration strategy based on various factors. Technically, this approach weighs in subexpression recurrence by term-graph-based enumeration, avoids useless candidates by example-guided filtration, prioritizes valuable components identified by large language models. This approach also incorporates a bottom-up deduction step to enhance the enumeration algorithm by considering subproblems that contribute to the deductive resolution. We implement all the enhanced enumeration techniques in our S y G u S solver D ryad S ynth , which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, D ryad S ynth successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker’s Delight problems.

@article{paperbot2627,
  title = {Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations},
  author = {Yuantian Ding and Xiaokang Qiu},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632913}
}