API to expression classes for bitvectors.
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
virtual bvt convert_popcount(const popcount_exprt &expr)
virtual std::size_t boolbv_width(const typet &type) const
static bvt zero_extension(const bvt &bv, std::size_t new_size)
bvt popcount(const bvt &bv)
Symbolic implementation of popcount (count of 1 bits in a bit vector) Based on the pop0 algorithm fro...
typet & type()
Return the type of the expression.
The popcount (counting the number of bits set to 1) expression.
std::vector< literalt > bvt