Clp interface with egraph

General
1

Hello all,
I have just released a new version (v0.6.0) of my egraph library where you can now use a generalized form of an egraph rule where you can match and produce multiple terms:

egraph:rule(triangle, 
   [seg(A, B)-_, seg(B, C)-_, seg(C, A)-_], 
   [triangle(A, B, C)-_]
) :-
   A \== B, B \== C, A \== C.

After discussing it with the zulip egraph community, I have also came up with a clp like interface to the egraph, which you can use like this:

?- A #= a, FFA #= f(f(a)), A = FFA, FFFFA #= f(f(f(f(a)))).
A = FFA, FFA = FFFFA,
FFFFA#=a,
FFFFA#=f(f(a)),
FFFFA#=f(f(f(f(a)))).

The thing is that I am not really sure what use could this have ?
Anybody has ideas ?
I just find it neat.

N.B.: @jan The addon page is still stuck on version 0.5 ? I suppose it is still a problem with a server not updating correctly like last time ?

2

I don’t know whether its the same as backtracking? And
how about A \== B, is it anti-unification? Mc Cune used
inequality initiation / propagation rules in his heuristics.

Sometimes rewriting and backtracking is used in model finding.
Here is an example, first using a slow rewriter with a straight
forward dumb solving strategy resulting in ca. 7.5 seconds:

?- time(mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, _)).
% Zeit 7726.925 ms, GC 44.343 ms, Lips 13101 k
true

If desired I can post the full source code, its only 150
lines of Prolog. Or one can study the Mc Cune description
or sift the E-graph community for inspiration. Then using

a little faster rewriter and a unit heuristic down to ca. 150 ms:

?- time(mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, _)).
% Zeit 166.140 ms, GC 0.000 ms, Lips 18616 k
true

Mc Cune himself reported 0.010 seconds , so 10 ms. He has
some nice heuristics in stock, and it was implemented in
LADR Argonne. Do E-graphs have such an application

domain? In principle it is not necessary to do a full grounding,
although the result, as a model, is usually some operator tables,
which show quite some grounding. But it can also have

don’t cares, indicating model variation. With union find the
result might look differently, for example it could say 4*4-2*1
and 2*1-5 instead of 4*4-5 and 2*1-5.

The approach is different from CLP(FD), since we don’t
label variables , instead we label functions, i.e. operator tables.
So its already on the 2nd order MIL level.

P.S.: The problem input is something like:

image
image497×152 9.53 KB

The problem output is something lilke:

image
image367×270 8.59 KB

The 150 lines Prolog code produce a similar result:

?- mccune([e*X=X,X^(-1)*X=e,X*(Y*Z)=(X*Y)*Z, c*d\=d*c], 6, R).
R = [d-2, c-1, 5*2-3, 5*5-4, 4*3-2, 3*5-2, 3*2-5, 4*4-5, 2*4-3, 
2*3-4, 3*4-1, 3*1-4, 5*3-1, 4*1-3, 1*5-3, 1*3-5, 2*1-5, 2*5-1, 
5*1-2, 4*2-1, 1*4-2, 1*2-4, 5*0-5, 4*0-4, 4*5-0, 5^ -1-4, 5*4-0, 
4^ -1-5, 3*0-3, 3*3-0, 3^ -1-3, 2*0-2, 2*2-0, 2^ -1-2, 1*0-1, 
1*1-0, 1^ -1-1, 0^ -1-0, 0*5-5, 0*4-4, 0*3-3, 0*2-2, 
0*1-1, 0*0-0, e-0]
3

But you also see why the payback of union find in such
search examples is so low. If |D| = n is the domain size,
then although |D x D| has size n^2, the diagonal E_D,

namely E_D = { (x,y) | x e D, y e D, x = y } has
only size n. So the probability of a pair in certain problem
domains, is around 1/n, getting smaller and smaller with

larger and larger n. My experiments showed that union find
only generated overhead. But maybe I should try again.
It questions the whole E-graph idea from the viewpoint of

heuristics for some Mc Cune like model finding problems.
Maybe the more effective methods, that look for the needle
in the hay stack, attack the problem from a totally different

angle, still they use rewriting.

Edit 10.05.2026:
One challenge is that the example has not only anti-unification,
like the c*d\=d*c, the Mc Cune style model finder implementation
makes also heavy use of backtracking. So I even don’t know

whether ISAMORE papers with saturation would help:

Finding Reusable Instructions via E-Graph Anti-Unification
Youwei Xiao et al. - ASPLOS ’26
https://github.com/pku-liang/ISAMORE

But I guess ISAMORE also delivers rewriting challenges. But
their subject matter in the above paper is LLVM/GEM5, so maybe
I rather buy a new Mac Neo (only $500) and enjoy local AI.