Go to the documentation of this file.
9 #ifndef CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
10 #define CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
bool has_byte_operator(const exprt &src)
Base class for all expressions.
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
The popcount (counting the number of bits set to 1) expression.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...