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 */
bool has_byte_operator(const exprt &src)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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...
exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
Lower a popcount_exprt to arithmetic and logic expressions.
Definition: popcount.cpp:16
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4815
Base class for all expressions.
Definition: expr.h:54
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
TO_BE_DOCUMENTED.