This module contains the implementation of a bitblaster for BitVec
expressions (BVExpr
).
That is, expressions that evaluate to BitVec
again. Its used as a building block in bitblasting
general BitVec
problems with boolean substructure.
@[inline]
Equations
Instances For
@[irreducible]