NUMBER-SUBTREES

(number-subtrees x) returns the number of distinct subtrees of X, in the sense of equal
Major Section:  HONS-AND-MEMOIZATION

This documentation topic relates to the experimental extension of ACL2 supporting hash cons, fast alists, and memoization; see hons-and-memoization.

In the logic, number-subtrees is defined as the length of cons-subtrees.

Under the hood, we first hons-copy X to obtain a normed version, then count the number of unique conses in X using an EQ hash table.