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
18
exprt
lower_byte_extract
(
const
byte_extract_exprt
&src,
const
namespacet
&ns);
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
solvers
lowering
expr_lowering.h
Generated by
1.8.17