This addresses a major performance shortcoming in the recent cvc5 proof signatures.
This PR ensures we apply weak head reduction (whr()) on definitions eagerly when they are added to the symbol table (note that nearly every term in the cvc5 signature is an application of an annotated lambda). This ensures that new copies are not generated on demand whenever whr() needs to be computed, e.g. within defeq().
This addresses a major performance shortcoming in the recent cvc5 proof signatures.
This PR ensures we apply weak head reduction (
whr()) on definitions eagerly when they are added to the symbol table (note that nearly every term in the cvc5 signature is an application of an annotated lambda). This ensures that new copies are not generated on demand wheneverwhr()needs to be computed, e.g. withindefeq().