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 namespacet;
16 class popcount_exprt;
17 
19 
20 exprt lower_byte_operators(const exprt &src, const namespacet &ns);
21 
22 bool has_byte_operator(const exprt &src);
23 
28 exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns);
29 
30 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:630
exprt
Base class for all expressions.
Definition: expr.h:54
expr.h
lower_byte_extract
exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
rewrite byte extraction from an array to byte extraction from a concatenation of array index expressi...
Definition: byte_operators.cpp:166
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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
byte_extract_exprt
TO_BE_DOCUMENTED.
Definition: byte_operators.h:25
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4815
lower_byte_operators
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Definition: byte_operators.cpp:645