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