Program synthesis has seen many new applications in recent years, in large part thanks to the introduction of SyGuS. However, no existing SyGuS solvers have support for synthesizing recursive functions. We introduce an multi-phase algorithm for the synthesis of recursive ``looplike'' programs in SyGuS for programming-by-example. We solve constraints individually and treat them as ``unrolled`` examples of how a recursive program would behave, and solve for the generalized recursive solution. Our approach is modular and supports any SyGuS Solver.
翻译:近年来,方案综合发现许多新的应用,这在很大程度上要归功于引入SyGuS。然而,现有的SyGuS解答器都没有支持合成循环函数。我们引入了一种多阶段算法,用于合成SyGuS中循环的“循环式”程序,用于逐例编程。我们单独解决制约,将其作为“无序”的例子,说明循环程序将如何行事,并解决普遍循环的解决方案。我们的方法是模块化的,支持任何SyGuS解答器。