Eliminate constants
This CIF to CIF transformation eliminates constants.
Supported specifications
This transformation supports a subset of CIF specifications. The following restrictions apply:
Component definitions and component instantiations are not supported.
Preprocessing
No preprocessing is currently performed by this CIF to CIF transformation. To increase the subset of specifications that can be transformed, apply the following CIF to CIF transformations (in the given order):
Implementation details
All uses of constants (for instance in guards, invariants, etc), are replaced by their values. The constants themselves are removed. For instance, the following specification:
const int x = 1;
const int z = y;
const int y = x + 1;
invariant x + y + z > 0;is transformed to the following specification:
invariant 1 + 2 + 2 > 0;Size considerations
Since constants are shortcuts for values, eliminating them could result in an increase of the size of the specification. Constants may be defined in terms of other constants. Therefore, in the worst case, the increase is exponential.
Optimality
For an assignment x := 1 + y, where y is a constant that is eliminated, and where y has value 5, the resulting assignment is x := 1 + 5. The result is not simplified any further. To further simplify the result, apply additional CIF to CIF transformations, such as Simplify values.