Program synthesis algorithms sufer 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.
Given a grammar and a logical specification program synthesis methods attempt to find a program
within the grammar that satisfies the logical specification. Program synthesis is hard [
A common method used to reduce this intractable search space is Observational Equivalence [
In this work, we leverage equivalence graphs (e-graphs) to lift equivalence based pruning to synthesis
with logical specifications over infinite domains. E-graphs are well suited to compactly storing large
sets of terms, and have been used for quantifier instantiation via e-matching [
However, despite the compact representation aforded by e-graphs, the algorithm is still overwhelmed
by combinatorial explosion. In an attempt to overcome this, we use equivalence relations that only hold
under certain assumptions. A common method for synthesis over symbolic variables is
Counterexample Guided Inductive Synthesis [
In this work, we consider syntax-guided synthesis problems, where a logical specification is given alongside a grammar expressing the space of possible solutions. An example is shown in Fig. 1, which gives a specification for a program that computes the maximum of 3 numbers. In the worst case, a traditional CEGIS loop would need to generate ∼ 50, 000, 000 programs before finding one that satisfies the specification, with each of these needing to be checked against the counterexamples and a subset needing to be checked over the whole specification. It is evident that some method to reduce the number of programs generated is required in order to make such synthesis feasible.
A syntax-guided synthesis (SyGuS) [
A context-free grammar is a 4-tuple = (Ω , Σ , , ). Ω is a finite set of variables also known as non-terminal symbols. Σ with Σ ∩Ω = ∅ is called the set of terminal symbols or alphabet. ⊆ Ω × (Ω ∪ Σ) * is a finite relation describing the production rules of the grammar. ∈ Ω is the start symbol of the grammar . (set-logic LIA) (synth-fun max3 ((x Int) (y Int) (z Int)) Int ((Start Int) (StartBool Bool)) ((Start Int (x y z
(ite StartBool Start Start))) (StartBool Bool ((>= Start Start))))) (declare-var a Int) (declare-var b Int) (declare-var c Int) (constraint (>= (max3 a b c) a)) (constraint (>= (max3 a b c) b)) (constraint (>= (max3 a b c) c)) (constraint (or (= a (max3 a b c)) (= b (max3 a b c)) (= c (max3 a b c)))) (check-synth)
Given a context-free grammar = (Ω , Σ , , ) with , ∈ (Ω ∪Σ) * and (, ) ∈ we say that yields , written → . We say that derives written → * if either = or → 1 → . . . → for ≥ 0. Finally, we define the language of a grammar (which gives the space of possible solutions for our SyGuS problem). ℒ = { ∈ Σ * | → * }.
Definition 2.2 (Syntax-Guided Synthesis). A syntax-guided synthesis problem is a 4-tuple ⟨ , , , ⟩, where is a context-free grammar, is a first-order formula in the background theory , and is a function symbol that occurs in . A valid solution to the SyGuS problem ⟨ , , , ⟩ is a function such that the formula [ / ] is -valid, according to the background theory, and ∈ ℒ .
We use [/ ] to indicate the result of substituting the symbol with a defined function , and we use ⃗ = 1, 2, . . . to represent the set of free (nullary) variables in .
In this work, we assume the background theory is Linear Integer Arithmetic, and the grammar contains one non-terminal symbol of type integer, and one non-terminal symbol of type bool.
The most common algorithm for solving program synthesis problems is CounterExample Guided Inductive Synthesis, CEGIS, shown in Fig. 2.
The e-graph data structure captures symbolic equivalence between terms through equivalence relations
defined as rewrite rules. It also supports equality saturation; a non-destructive compositional method
for propagating equivalences [
In order to use e-graphs to express the space of possible solutions to a synthesis problem, let us first map the production rules in our grammar into function symbols. Given a production rule → ℎ, where ∈ Ω and ℎ ∈ (Ω ∪ Σ) * , we say the production rule is an -ary production rule if ℎ contains occurrences of a non-terminal symbol.
Intuitively, an e-graph representing the space of terms within our context-free grammar can be given as: • A set of e-classes, which consist of groups of e-nodes determined to be equivalent terms in the underlying language. • An e-node is an -ary production rule → ℎ from our grammar, with associated child eclasses. An e-node represents the set of terms obtained by substituting the non-terminal symbols in ℎ with any node from within the corresponding child e-classes. An e-node representing applications of → ℎ is annotated with its corresponding non-terminal symbol .
Given a synthesis problem ⟨, , , ⟩, we can define an e-graph which represents the space of possible solutions as follows: Definition 2.3 (e-graphs). An e-graph is as a tuple ( , ∼=) where is a set of terms in a ℒ , and ∼=⊂ × is an equivalence relation, such that, for any 1, 2 ∈ if (1, 2) ∈∼=, then 1 = 2 is -valid. Each term is annotated with its corresponding non-terminal symbol.
Rewrite rules An e-graph is equipped with rewrite rules, that define the equivalence relation as patterns of the form ℓ → . If a rewrite rule finds a term matching the pattern ℓ, it will create a e-node representing the expression generated by the substitution defined by the rule. If the new e-node already exists in the e-graph, the e-class of this node and the e-node representing the original term are merged, otherwise the new e-node is added to the e-class of the original e-node. We assume that all rewrite rules result in programs that abide by the syntactic restriction of the SyGuS problem, i.e., rewrite rules cannot result in terms that are not contained within ℒ .
For instance, take an e-graph of the term (+ ) with the rewrite rule (+ ? ?) → (× ? 2), where ? is a pattern that captures any term. The equivalence relation defines that (+ ? ?) ∼= (× ? 2). Applying the rewrite will add the two new e-nodes required to represent (× 2) with the relevant children, namely 2 and × , to the e-graph. Rewrite rules are applied until no further changes occur, referred to as equality saturation.
The first approach we present is a naive bottom-up enumerative algorithm using e-graphs to represent and eficiently prune the pool of possible programs. This enables us to lift the notation of observational equivalence, which has been used successfully to prune the search space of programs in programmingby-example, to more general synthesis specifications.
Bottom-up enumeration has been used as the synthesis phase in many CEGIS implementations [
The pool of programs grows exponentially large as the length of the programs increases. For
specifications over finite inputs, like programming-by-example, this exponential growth is tamed by observational
equivalence [
In our approach, we lift this equivalence-based pruning to general synthesis specifications (even those reasoning about infinite inputs), by using e-graphs to represent the pool of programs and eficiently perform the equivalence check. The synthesis proceeds as follows: Constructing the initial e-graph Given a syntax-guided synthesis problem ⟨, , , ⟩, we initially construct an e-graph = ( , ∼=), where is the set of terms on ℒ that can be obtained from the start symbol with 1 derivation, and ∼= is initially empty.
Equality saturation At the start of each growing iteration, we iteratively apply a set of rewrite rules to saturation, adding equivalence relations to ∼=, and resulting in an e-graph where each e-class represents groups of equivalent terms in the background theory. That is, for any two terms 1, 2 ∈ , (1, 2) ∈∼= implies that 1 = 2 is -valid, according to the background theory . Checking the pool As before, we check the pool of programs against the counterexamples. However, this time, instead of iteratively checking all programs, we instead iterate through the e-classes and then extract and check the canonical form from each e-class. Growing the e-graph Once we have checked all the e-classes in the pool, we grow the pool. To do this, we add all terms to the e-graph that can be obtained by combining e-classes from with a single production rule from the grammar. By using e-classes to replace the non-terminal symbols in the production rules instead of e-nodes, we tame the exponential growth of the search space. The full algorithm is shown in Appendix A.1 - Algorithm 2, along with an algorithm showing standard bottom-up enumeration, Algorithm 1.
Optimizations: Since rewrite rules in e-graphs are non-destructive, i.e., e-nodes for both the left and
right hand side of the rule are retained within the e-graph, we implement two optimizations: First, before
adding a new program, during the growing phase, we check whether it already exists in a previously
explored e-class in at a rewrite distance of one. This slows the growth of the program pool. Specifically,
we use compactive rewrites, whereby we do not add new e-nodes generated by rules and instead only
use them to merge e-classes already present in the e-graph, this ensures equality saturation does not
add unnecessary e-nodes. Additionally, when checking programs we use structural generalization,
described in [
Bottom-up enumeration with e-graphs significantly reduces the number of programs we have to send to the verifier, but the program space still grows impractically large. For our second synthesis approach, we introduce the notion of counterexample e-graphs, or CE-graphs, which capture the sets of programs that behave equivalently under a given counterexample. We exploit CE-graphs for two purposes: firstly, they enable us to prune the space of candidates using equivalence rules that are conditioned on the counterexample; second, they allow us to guide the growth of the program pool, based on the needs of the counterexamples obtained so far. In this section, we first define CE-graphs, and how to construct them, before presenting a CE-graph based synthesis algorithm.
Recall that a counterexample ⃗ is an assignment to all the free variables ⃗ which caused a previous candidate solution * to violate the specification .
Definition 4.1 (CE-graph). Given a counterexample ⃗, a counterexample e-graph is defined as ⃗ = ( ∼=⃗), where is a set of terms in the language , and the congruence relation ∼=⃗ is defined such that, for any two terms 1 ∼= 2 if and only if 1[⃗/⃗] = 2[⃗/⃗] is -valid under the background theory .
Given a CE-graph, ⃗, we can now group the e-classes into invalid e-classes and valid e-classes. An invalid e-class is an e-class that contains only programs that fail to satisfy the specification on the given counterexample. A valid e-class is an e-class that contains only programs that satisfy the specification for the given counterexample.
Synthesis with CE-graphs proceeds through two stages: first, building the CE-graph, which allows us to obtain an infinite set of terms which satisfy the specification under the current counterexample; second, pruning the search space by joining the current CE-graph with the previously obtained CE-graphs. This pruning restricts the set of infinite terms to only the depth required by the counterexamples obtained so far. This implicit e-graph growth, achieved through counterexample guided rewrite rules, allows us to avoid the explicit growth of the e-graph that is necessary in Section 3.
As an overview, the synthesis proceeds as follows: Initialization We initialise the algorithm by constructing a base e-graph, 0, which contains all terminal symbols in , and an application of each production rule in , applied to all possible terminal symbol combinations. We do this using bottom-up enumeration, as before, to a depth of 2. We then select a term randomly from the e-graph, and pass this to the verifier. We assume this term will fail verification, and a counterexample will be returned.
Build Given a counterexample ⃗′, we build ⃗′ from 0. If the valid set of ⃗′ is empty, we grow 0, adding one more layer of programs.
Join Join the new CE-graph, ⃗′ to the previous ⃗, and set this to be the current CE-graph, i.e., ⃗ = ⃗′ ⊔ ⃗. If this is the first CE-graph we have seen, simply set ⃗ = ⃗′.
Verify Sample a program from the valid e-classes of ⃗, and pass this to the verifier. If it passes verification, return this solution to the user. If it fails, return the counterexample to the Build step and repeat.
Pseudocode for the full algorithm is included in Appendix A.1, Algorithm 4. We will now discuss the build and join phases in more detail.
Building the CE-graph Given a counterexample, ⃗, we encode the counterexample equivalence relation ∼=⃗ using a set of rewrites derived from the counterexample; for instance, given the counterexample [ ↦→ 1, ↦→ 0], we generate the rewrites such as (> ) → ⊤. For example, when considering a grammar involving equivalence relations, we may generate the following rules: • For each pair of variables in the assignment we have a set of rewrites for the lt, gt and eq comparators. • If the specific constants 0 and 1 are within the assignment, we define rewrite sets for assignments that assign free variables to either.
This allows us to construct the e-graph ⃗, as defined above, by applying these rewrite rules to the base e-graph 0. Note that ∼=⃗ introduces recursive edges to the e-graph, efectively representing infinite sets of terms that behave equivalently under the counterexample, as shown in Fig. 3.
We test one term from each e-class against the current counterexample, and if [/, ⃗/⃗] = ⊤, we mark the e-class as . If there are no valid terms, we grow the base e-graph by one iteration. The pseudocode for building the CE-graph is in Appendix A.1 - Algorithm 3.
Pruning via Join We note that any valid solution to the synthesis problem must be in a valid e-class on every counterexample e-graph. Thus, by performing the join of the current counterexample e-graph with the previous one, we can reduce our search space to only terms in the intersection of the valid e-classes. Further optimisations of this join are possible, in which unnecessary e-nodes are removed, however, our current implementation defines join as e-graph intersection, defined below: Definition 4.2 (Join of CE-graph). Given two CE-graphs, ⃗1 = (⃗1 , ∼=⃗1 ) and ⃗2 = (⃗2 , ∼=⃗2 ), the join of the two e-graphs, ⃗1 ⊔ ⃗2 is an e-graph ⃗1⊔⃗2 = (⃗1 ∩ ⃗2 , ∼=⃗1⊔⃗2 ), where (1, 2) ∈∼=⃗1⊔⃗2 ⇐⇒ (1, 2) ∈∼=⃗1 ∧(1, 2) ∈∼=⃗2 .
At each iteration, we join the most recent CE-graph to the CE-graph representing the current search space, . The result of this join is then set to be the new . We then sample a program from the valid e-class of and send this to verification, repeating the loop.
Note that this join discards equivalence relations that are not valid under both counterexamples, efectively pruning the terms represented in the CE-graph by unrolling recursion not supported by all counterexamples obtained so far. Running Example: To more clearly describe the algorithm let us follow an example of a possible path this method may take, visualised in Fig. 3. Assume that we are searching for a program that returns the maximum of three values, as in Fig. 1. In line with the motivating example, the algorithm provides a guess from the grammar’s terminal symbols, x, to which the oracle returns the counterexample, ⃗1 = [ ↦→ 1, ↦→ 2, ↦→ 0]. Using 0, a CE-graph ⃗1 is built rewrite rules derived from the counterexample, including, but not limited to:
(≥ ) → ⊥ (≥ ) → ⊤ (≥ ) → ⊥ (× ?) → ? (× ?) → 0 → 1
We use ⃗1 to generate a new candidate which satisfies the specification for ⃗1, y. The counterexample ⃗2 = [ ↦→ 2, ↦→ 1, ↦→ 0] is returned and used to create ⃗2 . We then generate a new CE-graph, = ⃗1 ⊔ ⃗2 , representing the subset of ℒ that satisfies both ⃗1 and ⃗2. The remaining satisfying terms in are made up of those that compare and , returning the largest of the two, for instance ( ite (>= x y) x y). Providing this as a candidate yields ⃗3 = [ ↦→ 0, ↦→ 1, ↦→ 2], used to generate = ⊔ ⃗3 . The satisfying terms in now only contains terms that compare the three variables and returns the largest of the three, the set of all satisfying terms.
We implement preliminary versions of both approaches. We use the rust egg crate [
Performance: The results in Table 1 show that both e-graph based synthesis methods reduce the number of candidate programs sent to the verifier substantially, which is to be expected. The naive bottom-up enumerator solves fewer benchmarks than cvc5, but Fig. 4 shows the performance is comparable with cvc5 on the ones it does solve, which is surprising given the highly preliminary nature of our implementation. From Table 1 we see that the CE-graph approach does not outperform the naive bottom-up method, which we hypothesize is due to an ineficient (for our purposes) implementation of join, as well as an incomplete conditional rewrite rule set.
Naive bottom-up e-graph ce-graphs CVC5
78 54 87 70 85 61 9
Completeness of rewrite rules: The set of rewrite rules we provide to both approaches is incomplete (i.e., (1, 2) ∈∼=⃗⇒ 1[/⃗] = 2[/⃗], but 1[/⃗] = 2[/⃗] ⇏ (1, 2) ∈∼=⃗). For the naive enumeration, this will result in checking more programs than necessary. For the CE-graph synthesis, incomplete rewrite rules will result in more occasions where the valid set does not contain the valid solution and we must explicitly grow the base e-graph. The rewrite rules are also written by hand. One possible direction to explore is executing the terms on each counterexample, and using these results to infer rewrite rules. Generality: The current CE-graph synthesis formulation is biased towards solving benchmarks with solutions that rely on comparators captured in our conditional rewrites. For other benchmarks, relying on predefined rewrite rules may always be significantly less efective.
Join Eficiency: As mentioned in Section 4.2, there is significant ineficiency in the CE-graph method
due to the ineficient implementation of join. Namely, that we calculate the join of all e-classes, including
terms that are not within the valid set. A more eficient CE-graph join, inspired by ideas from colored
e-graphs [
Counterexample Ordering: As with many synthesis approaches, the order that we encounter
counterexamples in can result in big variations in solving time, as this produces a diferent sequence of
CE-graphs. Determining the best counterexample is an open question in synthesis [
Soundness and Completeness Our approach is sound, in that any result that is returned is guaranteed to be correct, provided the verifier is correct. It is not complete, and cannot be complete as the synthesis problem in general is undecidable. However, if the grammar is restricted to one that expresses a finite number of programs, it should be possible to provide guarantees that a program will be found.
There are many approaches to pruning the search space in program synthesis, including using deductive
reasoning [
Observational equivalence has been leveraged for programming by example by using finite tree
automata (FTA), in which each node contains all observationally equivalent programs with hyper-edges
representing productions rule applied to child nodes [
In SyMetric [
Equivalence abstraction in FTAs was introduced in the tool Blaze [
Granularity of equivalence relations Extending the capabilities of e-graphs to represent multiple
levels of equivalence relations, as describe in our methods, has been explored. As eluded to in Section 5
colored e-graphs [
We have presented an approach to using e-graphs to eficiently represent and enumerate the space of possible programs for general program synthesis. To the best of our knowledge, this is the first approach to use e-graphs in this way. There are a number of limitations to our approach, yet, despite this, it performs comparably to the state of the art on a small set of benchmarks. Given the intertwined nature of synthesis, SMT solving, and e-graphs, we would welcome discussion with the community on the directions this work should take next.
The authors used Grammarly for grammar and spell-checking, and Claude to assist with the implementation of the proposed algorithms. After using these tools, the authors reviewed and edited content as needed and take full responsibility for the publication’s content. Algorithm 1 Bottom-Up Enumerator ◁ Add all terminal symbols to the pool of programs ◁ Check against counterexamples ◁ iterate through production rules ◁ Build list of lists of possible operands ◁ iterate through symbols in RHS of rule ◁ If this is a nonterminal symbol
◁ Get all of the same type as Algorithm 2 Naive Bottom-Up Enumeration using E-graph 1: procedure Enumerate(, , ) 2: ← BuildInitialGraph() ◁ Initial e-graph 3: while 1 do 4: for ∈ GetEClasses() do ◁ Check for each new e-class against counterexamples 5: ← Extract() ◁ Extract a canonical program from e-class 6: if ∀⃗ ∈ .(, ⃗) then 7: return 8: end if 9: end for 10: for (, ) ∈ do ◁ iterate through production rules 11: ← [] ◁ Build list of lists of possible operands 12: for ∈ do ◁ iterate through symbols in RHS of rule 13: if ∈ Ω then ◁ If this is a nonterminal symbol 14: ← FilterEClasses(, ) ◁ Get all e-classes annotated with 15: ← [, ] 16: end if 17: for ∈ CartesianProduct() do 18: ← BuildProgram(, ) 19: if !RewriteOnce() ∈ then ◁ Check if equivalent program exists in e-graph by a single rewrite 20: ← Add(, ) 21: end if 22: end for 23: end for 24: end for 25: ← EqualitySaturation() 26: end while 27: end procedure Algorithm 3 Building a Conditioned E-Graph 1: procedure BuildCEGraph(0, , ⃗) 2: ← ⊥ 3: while not do 4: ← GenerateConRewrites(⃗) 5: ⃗ ← Run(0, ) 6: ← GetValid(⃗) 7: if then 8: return ⃗ 9: end if 10: 0 ← Enumerate(0) 11: end while 12: end procedure ◁ Generate rewrites conditioned on ⃗ ◁ Run equality saturation with conditional rewrites Algorithm 4 CE-Graph Synthesis 1: procedure CE-CEGIS(, ) 2: ← ∅ 3: 0 ← InitialEGraph() 4: ← ∅ 5: Pick * ∈ .Σ 6: while true do 7: if ∃ . ¬( * , ) then 8: ← ∪ {} 9: ⃗ ← BuildCEGraph(0, ) 10: ← ⊔ ⃗ 11: Pick * ∈ { ∈ | (, )} 12: else 13: return * 14: end if 15: end while 16: end procedure ◁ Set of counterexamples ◁ Initial e-graph built from the grammar
◁ Choose an initial terminal symbol ◁ Join with new conditioned e-graph