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;

Renaming

n/a

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.

Annotations

This transformation does not process or add any annotations. As this transformation removes all constants from the specification, their annotations are removed as well.