This module contains the implementation of the pre processing pass for handling enum inductive types.
The implementation:
- generates mappings from enum inductives occurring in the goal to sufficiently large
BitVec
and replaces equality on the enum inductives with equality on these mapping functions. - Constant folds these mappings if appropriate.
- Adds bounds on the values returned by the mappings if the size of the enum inductive does not fit into a power of two.
- Handles applications of these mappings to
ite
,cond
and basic match statements.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Assuming that declName
is an enum inductive, construct a proof of
∀ (x y : declName) : x = y ↔ x.enumToBitVec = y.enumToBitVec
.
Equations
Instances For
Assuming that declName
is an enum inductive, construct a proof of
∀ (x : declName) : x.enumToBitVec ≤ domainSize - 1
where domainSize
is the amount of
constructors of declName
.
Equations
Instances For
Obtain a theorem that translates .match_x
applications on enum inductives to chains of cond
applications. If the specific .match_x
that this is being called on is unsupported throw an error.
Equations
Instances For
This simproc should be set up to trigger on expressions of the form EnumInductive.enumToBitVec x
.
It will check if x
is a constructor and if that is the case constant fold it to the corresponding
BitVec
value.