E-graph modulo theory (EMT) sketch

Minimal E-graph implementation using Prolog variables as e-class ids. This is a pedagogical re-implementation of egraph.pl using the E-graph Modulo Theory approach, starting with AC theory support.

The EMT state is a list of Theory-Data pairs, e.g. [egraph-List]. Each theory manages its own data structure.

Design note: e-class ids are Prolog variables, merged by unification. Since we cannot mutate an existing node entry in place, congruence closure is done in batch: each theory's node list is sorted (sort for egraph to dedup identical nodes, msort for ac to canonize multiset nodes keeping duplicates) and grouped by canonical key so that congruent nodes collapse together (see rebuild//1 and merge_groups//2), rather than via an incremental union-find.

Notation recap:

DCG (-->) threads an implicit state pair S0,S through a sequence of operations (not for parsing). phrase(G, In, Out) runs it; {G} is a plain Prolog goal that skips the state.
SSU (==>) is one-sided, committing pattern matching: the head matches without instantiating the caller; on match it commits (no backtracking to later clauses).
Head, Cond ==> Body combines both: Cond may contain DCG goals (state-threaded) and {G} goals (plain). First matching clause commits. See add_term//2, ac_flatten//2.
Ordsets as multisets. We abuse library(ordsets) on msort-ed lists (which keep duplicates) to get sorted multiset ops: ord_union~multiset sum, ord_subtract~difference, ord_intersect/ord_subset~overlap/containment.

38:- use_module(library(pairs)). 39:- use_module(library(dcg/high_order)). 40 41lookup(Node-Class, [N-C | L]) :- 42 ( Node == N 43 -> Class = C 44 ; lookup(Node-Class, L) 45 ). 46 47:- meta_predicate with_theory(+, //, ?, ?). 48 49with_theory(Theory, Goal, In, Out) :- 50 selectchk(Theory-DataIn, In, Theory-DataOut, Out), 51 call(Goal, DataIn, DataOut). 52 53add_term(Term, Id), compound(Term) ==> 54 { compound_name_arguments(Term, F, Args) }, 55 add_terms(Args, Ids), 56 { compound_name_arguments(Node, F, Ids) }, 57 add_node(egraph, Node, Id). 58add_term(Term, Id) ==> 59 add_node(egraph, Term, Id). 60 61add_terms([], []) --> []. 62add_terms([Term | Terms], [Id | Ids]) --> 63 add_term(Term, Id), 64 add_terms(Terms, Ids). 65 66add_node(Theory, Node, Id) --> 67 with_theory(Theory, add_node(Node, Id)). 68 69add_node(Node, Id, In, Out) :- 70 ( lookup(Node-Id, In) 71 -> Out = In 72 ; ord_add_element(In, Node-Id, Out) 73 ). 74 75rebuild([A=B | Unifs]) --> 76 { A = B }, 77 rebuild(Unifs). 78rebuild([]) --> 79 with_theory(egraph, sort), 80 congruence_closure(Unifs, []), 81 ( { Unifs == [] } 82 -> [] 83 ; rebuild(Unifs) 84 ). 85 86congruence_closure(Unifs, UnifsTail, In, Out) :- 87 foldl(rebuild_groups, In, Out, Unifs, UnifsTail). 88rebuild_groups(Theory-In, Theory-Out) --> 89 { group_pairs_by_key(In, Groups) }, 90 merge_groups(Groups, Out). 91 92merge_groups([], []) --> []. 93merge_groups([Node-[Id | Ids] | Groups], [Node-Id | Out]) --> 94 sequence(merge_id(Id), Ids), 95 merge_groups(Groups, Out). 96merge_id(A, B) --> [A=B]. 97 98a_c([a-A], [c-C | Right], Right, [A=C | Unifs], Unifs). 99comm([A+B-AB], [B+A-BA | Right], Right, [AB=BA | Unifs], Unifs). 100assoc([A+BC-ABC, B+C-BC], [A+B-AB, AB+C-ABC_ | Right], Right, [ABC=ABC_ | Unifs], Unifs). 101 102match_goals(Module, Goals, Unifs, EGraph, Right) :- 103 foldl(match(EGraph, Module), Goals, Right-Unifs, EGraph-[]). 104 105match(EGraph, Mod, Goal, Right-Unifs, RightTail-UnifsTail) :- 106 call(Mod:Goal, Patterns, _, _, _, _), 107 match(Patterns, EGraph, Mod:Goal, [], [], Right, RightTail, Unifs, UnifsTail). 108 109match([], _EGraph, Goal, _Bindings, Left, Right, RightTail, Unifs, UnifsTail) :- 110 reverse(Left, RLeft), 111 call(Goal, RLeft, Right, RightTail, Unifs, UnifsTail). 112match([Pattern | Patterns], EGraph, Goal, Bindings, Left, Right, RightTail, Unifs, UnifsTail) :- 113 match(Pattern, EGraph, Goal, Patterns, EGraph, Bindings, Left, Right, RightTail, Unifs, UnifsTail). 114 115match(Pat-CPat, [Node-Class | L], Goal, Patterns, EGraph, In, Left, Right, RightTail, Unifs, UnifsTail), 116 compound(Pat), 117 compound(Node), 118 compound_name_arguments(Pat, F, Vars), 119 compound_name_arguments(Node, F, Args), 120 foldl(match_var, Vars, Args, In, Tmp), 121 match_var(CPat, Class, Tmp, Out) => 122 match(Patterns, EGraph, Goal, Out, [Node-Class | Left], Right, RightTmp, Unifs, UnifsTmp), 123 match(Pat-CPat, L, Goal, Patterns, EGraph, In, Left, RightTmp, RightTail, UnifsTmp, UnifsTail). 124match(Pat-CPat, [Pat-Class | L], Goal, Patterns, EGraph, In, Left, Right, RightTail, Unifs, UnifsTail), match_var(CPat, Class, In, Out) => 125 match(Patterns, EGraph, Goal, Out, [Pat-Class | Left], Right, RightTmp, Unifs, UnifsTmp), 126 match(Pat-CPat, L, Goal, Patterns, EGraph, In, Left, RightTmp, RightTail, UnifsTmp, UnifsTail). 127match(Pat, [_ | L], Goal, Patterns, EGraph, In, Left, Right, RightTail, Unifs, UnifsTail) => 128 match(Pat, L, Goal, Patterns, EGraph, In, Left, Right, RightTail, Unifs, UnifsTail). 129match(_, [], _, _, _, _, _, Right, RightTail, Unifs, UnifsTail) => RightTail = Right, UnifsTail = Unifs. 130 131match_var(Pat, Class, In, Out), var(Pat) => 132 ( is_bound(Pat=CPat, In) 133 -> CPat == Class, Out = In 134 ; ord_add_element(In, Pat=Class, Out) 135 ). 136 137is_bound(X=A, [X=B | _]) => A=B. 138is_bound(X, [_ | L]) => 139 is_bound(X, L). 140is_bound(_, []) => fail. 141 142:- meta_predicate saturate(:, +, ?, ?). 143 144egraph_length(N, In, In) :- 145 length(In, N). 146 147saturate(Module:Goals, N) --> 148 with_theory(egraph, egraph_length(L1)), 149 { debug(saturate, "~p", [L1]) }, 150 with_theory(egraph, match_goals(Module, Goals, Unifs)), 151 rebuild(Unifs), 152 with_theory(egraph, egraph_length(L2)), 153 ( { L1 == L2 } 154 -> [] 155 ; { N1 is N - 1 }, 156 saturate(Module:Goals, N1) 157 ). 158 159:- begin_tests(emt_lookup). 160 161test(head_match, true(C == 1)) :- 162 lookup(a-C, [a-1]). 163 164test(tail_match, true(C == 2)) :- 165 lookup(f(x)-C, [g-0, f(x)-2]). 166 167test(not_present, fail) :- 168 lookup(missing-_, [a-1]). 169 170test(identity_distinguishes_order, fail) :- 171 X = a, Y = b, 172 lookup(f(X, Y)-_, [f(Y, X)-_]). 173 174:- end_tests(emt_lookup). 175 176:- begin_tests(emt_add_node). 177 178test(atomic_insert) :- 179 phrase(add_node(egraph, a, Id), [egraph-[]], Out), 180 Out == [egraph-[a-Id]]. 181 182test(sorted_insertion) :- 183 phrase(( add_node(egraph, b, _), 184 add_node(egraph, a, _) 185 ), [egraph-[]], Out), 186 Out =@= [egraph-[a-_, b-_]]. 187 188test(idempotent_reinsert, true(Id1 == Id2)) :- 189 A = x, B = y, 190 phrase(( add_node(egraph, f(A, B), Id1), 191 add_node(egraph, f(A, B), Id2) 192 ), [egraph-[]], Out), 193 Out == [egraph-[f(A, B)-Id1]]. 194 195test(shared_args_dedup) :- 196 A = x, 197 phrase(add_node(egraph, h(A, A), _), [egraph-[]], Out), 198 Out =@= [egraph-[h(A, A)-_]]. 199 200:- end_tests(emt_add_node). 201 202:- begin_tests(emt_add_term). 203 204test(atomic_term) :- 205 phrase(add_term(atom, Id), [egraph-[]], Out), 206 Out == [egraph-[atom-Id]]. 207 208test(atomic_distinct) :- 209 phrase(( add_term(a, _), 210 add_term(b, _) 211 ), [egraph-[]], Out), 212 Out =@= [egraph-[a-_, b-_]]. 213 214test(atomic_reuse, true(Id1 == Id2)) :- 215 phrase(( add_term(a, Id1), 216 add_term(a, Id2) 217 ), [egraph-[]], Out), 218 Out == [egraph-[a-Id1]]. 219 220test(compound_term) :- 221 phrase(add_term(f(a, b), Id), [egraph-[]], Out), 222 Out =@= [egraph-[a-A, b-B, f(A, B)-Id]]. 223 224:- end_tests(emt_add_term). 225 226:- begin_tests(emt_rebuild). 227 228test(empty_graph) :- 229 phrase(rebuild([]), [egraph-[]], Out), 230 Out == [egraph-[]]. 231 232test(noop_no_congruence) :- 233 phrase(rebuild([]), [egraph-[a-X, b-Y]], Out), 234 Out =@= [egraph-[a-X, b-Y]]. 235 236test(duplicate_nodes_merge, true(X == Y)) :- 237 phrase(rebuild([]), [egraph-[a-X, a-Y]], Out), 238 Out =@= [egraph-[a-X]]. 239 240test(congruence_closure, true((X == Y, A == B))) :- 241 phrase(rebuild([]), [egraph-[a-X, a-Y, f(X)-A, f(Y)-B]], Out), 242 Out =@= [egraph-[a-X, f(X)-A]]. 243 244test(already_canonical) :- 245 phrase(rebuild([]), [egraph-[a-X, f(X)-A]], Out), 246 Out =@= [egraph-[a-X, f(X)-A]]. 247 248test(explicit_union_triggers_congruence, true((A == B, C == D))) :- 249 phrase(rebuild([A=B]), [egraph-[a-A, b-B, g(A)-C, g(B)-D]], Out), 250 Out =@= [egraph-[a-A, b-A, g(A)-C]]. 251 252:- end_tests(emt_rebuild). 253 254:- begin_tests(emt_match). 255 256test(match_repeated_var, true((Right =@= [c-C], Unifs =@= [A=C]))) :- 257 EGraph = [a-A, b-_B], 258 match(EGraph, emt, a_c, Right-Unifs, []-[]). 259 260test(match_ac, true(EGraph =@= [egraph-[a-A,b-B,c-C,D+C-E,A+B-D,A+C-F,A+G-E,B+A-D,B+C-G,B+F-E,C+D-E,C+A-F,C+B-G,F+B-E,G+A-E]])) :- 261 phrase(( 262 add_term(a+b+c, _ABC), 263 emt:saturate([comm, assoc], 10) 264 ), [egraph-[]], EGraph). 265 266:- end_tests(emt_match).