cprover
|
#include <util/expr.h>
Go to the source code of this file.
Functions | |
exprt | lower_popcount (const popcount_exprt &expr, const namespacet &ns) |
Lower a popcount_exprt to arithmetic and logic expressions. More... | |
exprt lower_popcount | ( | const popcount_exprt & | expr, |
const namespacet & | ns | ||
) |
Lower a popcount_exprt to arithmetic and logic expressions.
expr | Input expression to be translated |
ns | Namespace for type lookups |
Definition at line 16 of file popcount.cpp.
References address_bits(), CHECK_RETURN, from_integer(), irept::id(), integer2size_t(), exprt::make_typecast(), unary_exprt::op(), pointer_offset_bits(), power(), and exprt::type().
Referenced by boolbvt::convert_bitvector(), and smt2_convt::convert_expr().