CBMC
Loading...
Searching...
No Matches
boolbv_popcount.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Michael Tautschnig
6
7\*******************************************************************/
8
10
11#include "boolbv.h"
12
14{
15 const std::size_t width = boolbv_width(expr.type());
16
17 bvt op = convert_bv(expr.op());
18
19 return bv_utils.zero_extension(bv_utils.popcount(op), width);
20}
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...
Definition boolbv.cpp:39
virtual bvt convert_popcount(const popcount_exprt &expr)
bv_utilst bv_utils
Definition boolbv.h:119
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:104
static bvt zero_extension(const bvt &bv, std::size_t new_size)
Definition bv_utils.h:187
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.
Definition expr.h:85
The popcount (counting the number of bits set to 1) expression.
const exprt & op() const
Definition std_expr.h:391
std::vector< literalt > bvt
Definition literal.h:201