Synthesis with Counterexample Guided Observational Equivalence Graphs

Abstract

Program synthesis is hard, as it must search in a huge space of possible programs for one that satisfies the desired specification. In programming-by-example, where specifications are purely given by input-output examples, we can reduce the space by exploiting observational equivalence: if two terms behave the same on all examples, then one can be discarded. But, how can we exploit observational equivalence for logical specifications that reason over potentially infinitely many program inputs? We explore the use of equivalence graphs in counterexample-guided inductive synthesis for general program synthesis. First, we investigate the use of traditional e-graphs and identify limitations that render them impractical for this task. Then, we present Observational Equivalence Graphs (ObsEGraph), a novel e-graph-inspired data structure. ObsEGraphs efficiently represent a set of programs, grouped by observational equivalence, which can be refined through additional observations. We then present Counterexample-guided Observational e-Graph Synthesis (COGS), a new synthesis approach that incrementally searches the space of possible programs by best-first counterexample-guided growth of an ObsEGraph. We show that COGS is sound and complete up to a bounded program size. Our evaluation on benchmarks from the Syntax-Guided Synthesis competition and the Termination competition finds that COGS solves 552 benchmarks, 69 more than cvc5, a state-of-the-art solver.