I am sorry to report that after a lot of experimentation with tabling, I couldn’t write an elegant version of the full congruence closure with tabling.
The problem has to do with the fact that when using tabling (so backtracking) with dynamic predicates, we need to ground the class ids.
However, when doing congruence closure, one need to replace all uses of a class id in all pairs that uses it. For example, let’s say you have the following pairs Node-Class: [a-a, f(a)-fa, f(fa)-ffa] and you want to unify a and ffa. You need to replace every instance of ffa in every pairs.
Doing this is extremely slow and very tedious. Moreover, I couldn’t manage to do batch rewrites and would always get incorrect nodes.
I have written another approach based on variables for class ids that is correct and scales quite a bit better.
I will post it when I have figured out how to make cost-based extraction to work.