No, I haven’t read that blog post and the idea is amazing (although I haven’t took the time to read the python code much).
In a previous post of mine, I thought about extending syntactical unification, but nobody brought egraph to the discussion.
So currently, the implementation treats variables like any other term.
But one could first saturate the egraph of a term, extract and check for syntactical unification:
?- phrase((
add_term(X+a, Xa),
add_term(a+b, AB),
saturate([comm]),
extract), [], G),
unifiable(Xa, AB, Unifs).
Xa = X+a,
AB = b+a,
G = [X-node(X, 1), a-node(a, 1), b-node(b, 1), ...],
Unifs = [X=b] ;
Xa = a+X,
AB = a+b,
G = [X-node(X, 1), a-node(a, 1), b-node(b, 1), ...],
Unifs = [X=b] ;
false.
But I suppose this is very, very inefficient.
I would guess a more efficient unification strategy would be to traverse the egraph classes directly without doing any extraction ?
I also don’t really understand where would constraints came into play here ?
Could you help me understand with a simple example ?