CBMC
enum_encoding.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
5 
6 #include <util/expr.h>
7 
14 exprt lower_enum(exprt expr, const namespacet &ns);
15 
16 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_ENUM_ENCODING_H
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
lower_enum
exprt lower_enum(exprt expr, const namespacet &ns)
Function to lower expr and its sub-expressions containing enum types.
Definition: enum_encoding.cpp:37