An optimizer can rewrite ((x + 0) * 1) + 2 * (1 + 2) in many ways. This
example explores every rewrite reachable within a small budget, scores each
candidate, and extracts the cheapest one, all as plain relations.
Run it in the playground · Source
Compilers and term-rewriting tools use equality saturation: apply every known equality to an expression, keep all the equivalent forms, then pick the best one. Real engines store the forms in an e-graph. EyeProlog has no e-graph, so this example asks the same question relationally: which terms are reachable from the start expression within six rewrite steps, and which of them is cheapest?
expr(start, add(mul(add(x, 0), 1), mul(2, add(1, 2)))).
fuel(6).
rewrite(add(X, 0), X).
rewrite(mul(X, 1), X).
rewrite(add(A, B), C) :- number(A), number(B), (C is A + B).
rewrite(mul(A, B), C) :- number(A), number(B), (C is A * B).
rewrite(mul(X, add(Y, Z)), add(mul(X, Y), mul(X, Z))).
Each rewrite/2 clause is one oriented equality: identity laws, constant
folding, and one distributive law. rewrite_anywhere/2 applies a rule at the
root or inside any subterm.
equivalent_at_depth(0, Expr, Expr).
equivalent_at_depth(Depth, Expr, Out) :-
(Depth > 0),
(Previous_depth is Depth - 1),
equivalent_at_depth(Previous_depth, Expr, Mid),
rewrite_anywhere(Mid, Out).
best_expression(Expr, Cost) :-
aggregate_min([Candidate_cost, Candidate], Candidate,
(candidate_expression(Candidate), expr_cost(Candidate, Candidate_cost)),
[Cost, Expr], Expr).
The fuel bound keeps the search finite. expr_cost/2 counts nodes, and
aggregate_min/5 keeps the candidate with the lowest cost, breaking ties by
term order so the result is deterministic.
eyeprolog examples/equality-saturation.pl
egraphAnswer(start, add(mul(add(x, 0), 1), mul(2, add(1, 2)))).
egraphAnswer(best, add(x, 6)).
egraphAnswer(cost, 3).
egraphAnswer(candidate_count, 32).
egraphAnswer(note, "bounded equality saturation extracts the cheapest term without a real e-graph").
Out of 32 candidate derivations, the cheapest equivalent form is x + 6, with
three nodes.
step(egraphAnswer(best, add(x, 6)),
rule(29),
['Expr' = add(x, 6)],
[best_expression(add(x, 6), 3)]).
step(best_expression(add(x, 6), 3),
rule(27),
['Expr' = add(x, 6), 'Cost' = 3],
[aggregate_min([Candidate_cost, Value], Value, (candidate_expression(Value), expr_cost(Value, Candidate_cost)), [3, add(x, 6)], add(x, 6))]).
The answer rests on best_expression/2, which rests on one aggregate_min/5
call. That call ranges over the whole candidate set, so the proof records it
as a single built-in step rather than replaying all 32 candidates.
condition('C1', resolution, ok, 7).
condition('C4', coverage, ok, 11).
condition('C7', relevance, ok, 14).
obligation(builtin, theory_scoped, aggregate_min([A, B], B, (candidate_expression(B), expr_cost(B, A)), [3, add(x, 6)], add(x, 6))).
obligation(builtin, theory_scoped, countall(candidate_expression(A), 32)).
verdict(checked_with_obligations).
Every rule step replays, but the two aggregates depend on the program’s own
candidate_expression/1, so the checker cannot recompute them in isolation.
It reports them as obligations: the proof is valid provided those two
summaries over the candidate set are right.
fuel(6) to fuel(2). Is x + 6 still reachable, and what does the
best expression become?rewrite(add(X, Y), add(Y, X)). (commutativity). Why would that blow up
the candidate count, and how does the fuel bound keep it finite?expr_cost/2 so multiplication costs more than addition and see
whether the extracted term changes.Learn more in The Art of EyeProlog, Chapters 22 and 23.