cprover
Loading...
Searching...
No Matches
simplify_state_expr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Simplify State Expression
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_CPROVER_SIMPLIFY_STATE_EXPR_H
13#define CPROVER_CPROVER_SIMPLIFY_STATE_EXPR_H
14
15#include <util/std_expr.h> // IWYU pragma: keep
16
17#include <unordered_set>
18
19class namespacet;
20
21exprt simplify_state_expr(
22 exprt,
23 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
24 const namespacet &);
25
26exprt simplify_state_expr_node(
27 exprt,
28 const std::unordered_set<symbol_exprt, irep_hash> &address_taken,
29 const namespacet &);
30
31#endif // CPROVER_CPROVER_PROPAGATE_H
address_taken
std::unordered_set< symbol_exprt, irep_hash > address_taken(const std::vector< exprt > &src)
Definition address_taken.cpp:51
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
simplify_state_expr_node
exprt simplify_state_expr_node(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition simplify_state_expr.cpp:961
simplify_state_expr
exprt simplify_state_expr(exprt, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const namespacet &)
Definition simplify_state_expr.cpp:1087
std_expr.h
API to expression classes.