(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.
