We describe an algorithm for simplifying a class of symbolic
expressions that arises in the symbolic execution of formal state
machine models. These expressions are compositions of state
access and change functions and if-then-else expressions, laced
together with local variable bindings (e.g., lambda
applications). The algorithm may be used in a stand-alone way,
but is designed to be part of a larger system employing a mix of
other strategies. The algorithm generalizes to a rewriting
algorithm that can be characterized as outside-in or lazy, with
respect both to variable instantiation and equality replacement.
The algorithm exploits memoization or caching. The algorithm is
being used in the formal verification of industrial
microprocessor models.
