Here is a sketch of the variable-substitution algorithm. It uses three user-specified complexity thresholds, whose purpose will become clear in the following description.
Given an expression [tex2html_wrap5822], compute its weight [tex2html_wrap5824]. Do not perform substitutions if [tex2html_wrap5826]. Otherwise, [tex2html_wrap5828] is a good candidate for variable substitution.
First try to substitute for the children of [tex2html_wrap5830]. Given children [tex2html_wrap5832], compute their weights [tex2html_wrap5834]. Substitute for a child [tex2html_wrap5836] if and only if its relative complexity is greater than *proportional-complexity-threshold*. Thus, for each [tex2html_wrap5838], if [tex2html_wrap5840], apply the algorithm recursively to [tex2html_wrap5842]. If no substitution can be performed on the descendants of [tex2html_wrap5844], replace [tex2html_wrap5846] itself.
If no substitution can be performed on any of the [tex2html_wrap5848] or their subexpressions, then substitute for [tex2html_wrap5850] provided that [tex2html_wrap5852] is not a top-level expression. Also do not substitute if [tex2html_wrap5854] is one of the sides of a relational.
Given a top level expression [tex2html_wrap5856] having weight [tex2html_wrap5858], this algorithm is called as follows:
[LVerbatim1677]
where (complexity-threshold e) is defined as:
[LVerbatim1680]
Instead of computing [tex2html_wrap5860], we initialize the algorithm with the threshold [tex2html_wrap5862], since [tex2html_wrap5864] remains constant throughout the algorithm.