Did you know ... Search Documentation:
Pack egraph -- prolog/emt.pl
PublicShow source

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.

Undocumented predicates

The following predicates are exported, but not or incorrectly documented.

 lookup(Arg1, Arg2)
 add_term(Arg1, Arg2, Arg3, Arg4)
 add_node(Arg1, Arg2, Arg3, Arg4, Arg5)
 rebuild(Arg1, Arg2, Arg3)
 with_theory(Arg1, Arg2, Arg3, Arg4)
 add_terms(Arg1, Arg2, Arg3, Arg4)
 congruence_closure(Arg1, Arg2, Arg3, Arg4)