(number-subtrees x)returns the number of distinct subtrees of X, in the
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
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.