Syntax-guided synthesis with counterexample-guided E-graphs:A work-in-progress report

Program synthesis algorithms suffer serious scalability issues due to the exponential growth of the space of solutions as programs grow longer. A common way to tame this search space in programming-by-example is to use observational equivalence. In this work in progress report we discuss a method for using equivalence graphs (e-graphs) to lift observational equivalence to more general program synthesis problems. We first present a naive synthesis algorithm using an e-graph to perform bottom-up enumeration. We also propose an extension of e-graphs, using approximate equivalence guided by counterexamples. We evaluate a preliminary implementation of both approaches against a state-of-the-art solver, and further outline scope for improvements and further research.