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;
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 
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