cprover
expr_lowering.h File Reference
#include <util/expr.h>
Include dependency graph for expr_lowering.h:
This graph shows which files directly or indirectly include this file:

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...
 

Function Documentation

◆ lower_popcount()

exprt lower_popcount ( const popcount_exprt expr,
const namespacet ns 
)

Lower a popcount_exprt to arithmetic and logic expressions.

Parameters
exprInput expression to be translated
nsNamespace for type lookups
Returns
Semantically equivalent expression

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().