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
namespacet
;
15
class
popcount_exprt
;
16
21
exprt
lower_popcount
(
const
popcount_exprt
&expr,
const
namespacet
&ns);
22
23
#endif
/* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */
namespacet
TO_BE_DOCUMENTED.
Definition:
namespace.h:74
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
popcount_exprt
The popcount (counting the number of bits set to 1) expression.
Definition:
std_expr.h:4890
exprt
Base class for all expressions.
Definition:
expr.h:42
expr.h
solvers
lowering
expr_lowering.h
Generated by
1.8.14