cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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:57
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition
namespace.h:91
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
expr.h
solvers
smt2_incremental
encoding
enum_encoding.h
Generated by
1.17.0