#include <rewrite_stack.h>

Detailed Description

This is an exception that is thrown when the rewrite stack must be resized. As the rewrite stack is a vector this invalidates all references and iterators in it, and that means that when resizing is necessary, the current term must be resized. When this exception is thrown, the current substitution must also be restored.

Note that the vector leaves terms on the stack as protected members when the stack is decreased. This is done intentionally because the stack is intensively used by the rewriters, and destroying and creating elements in the vector is a relatively expensive operation.

Definition at line 46 of file rewrite_stack.h.

The documentation for this struct was generated from the following file:

data/include/mcrl2/data/detail/rewrite/rewrite_stack.h