Example-Based Synthesis using Context-Sensitive E-Graph Saturation

Abstract

Program synthesis is the task of constructing a program that satisfies specified constraints. One popular formulation of program synthesis is example-based synthesis. Here, the synthesizer attempts to find a program in a specified domain that satisfies a set of input-output examples. Enumeration is the most common approach to finding the desired program. However, the exponentially growing search space makes this infeasible. The size of the domain can be largely attributed to its inefficient representation. Often, programs are only syntactically distinguished, meaning programs that behave the same are seen as different. We introduce Context-Sensitive E-Graph Saturation, a novel method that limits the search space to programs that solve at least one of the provided examples. This allows focusing only on programs that behave similarly to the desired one. Crucial is finding contextual equivalences for each example over a generated termset. These equivalences allow generating many solutions for each individual example. A program in the intersection of these programs solves all examples. In experiments on a subset from SyGus SLIA, our method solves the problems that enumeration solves, but not more. These results highlight a trade-off: with a small termset, the discovered equivalences are often too limited to capture the relationships needed to find a universal solution. Conversely, increasing the termset size quickly leads to inefficiency. To address this, we propose a strategy for constructing a more expressive yet small termset, enabling our method to solve a broader range of synthesis problems.