cprover
expr_lowering.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Lower expressions to arithmetic and logic expressions
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
10 #define CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H
11 
12 #include <util/expr.h>
13 
14 class byte_extract_exprt;
15 class byte_update_exprt;
16 class namespacet;
17 class popcount_exprt;
18 
27 
36 
43 exprt lower_byte_operators(const exprt &src, const namespacet &ns);
44 
45 bool has_byte_operator(const exprt &src);
46 
51 exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
52 
53 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */
byte_update_exprt
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Definition: byte_operators.h:81
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:2302
exprt
Base class for all expressions.
Definition: expr.h:53
expr.h
lower_byte_extract
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
Rewrite a byte extract expression to more fundamental operations.
Definition: byte_operators.cpp:999
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
lower_popcount
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:16
lower_byte_update
exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
Rewrite a byte update expression to more fundamental operations.
Definition: byte_operators.cpp:2256
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4308
lower_byte_operators
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
Definition: byte_operators.cpp:2317