cprover
simplify_expr.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#ifndef CPROVER_UTIL_SIMPLIFY_EXPR_H
11
#define CPROVER_UTIL_SIMPLIFY_EXPR_H
12
13
class
array_exprt
;
14
class
exprt
;
15
class
namespacet
;
16
class
refined_string_exprt
;
17
18
#include <
util/optional.h
>
19
20
//
21
// simplify an expression
22
//
23
// true: did nothing
24
// false: simplified something
25
//
26
27
bool
simplify
(
28
exprt
&expr,
29
const
namespacet
&ns);
30
31
// this is the preferred interface
32
exprt
simplify_expr
(
exprt
src,
const
namespacet
&ns);
33
46
optionalt<std::reference_wrapper<const array_exprt>
>
47
try_get_string_data_array
(
const
exprt
&
content
,
const
namespacet
&ns);
48
49
#endif // CPROVER_UTIL_SIMPLIFY_EXPR_H
try_get_string_data_array
optionalt< std::reference_wrapper< const array_exprt > > try_get_string_data_array(const exprt &content, const namespacet &ns)
Get char sequence from content field of a refined string expression.
Definition:
simplify_expr.cpp:1837
optional.h
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition:
simplify_expr.cpp:2698
exprt
Base class for all expressions.
Definition:
expr.h:53
refined_string_exprt
Definition:
string_expr.h:109
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
optionalt
nonstd::optional< T > optionalt
Definition:
optional.h:35
refined_string_exprt::content
const exprt & content() const
Definition:
string_expr.h:138
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition:
simplify_expr.cpp:2693
array_exprt
Array constructor from list of elements.
Definition:
std_expr.h:1432
util
simplify_expr.h
Generated by
1.8.20