cprover
simplify_expr.h File Reference
#include <util/optional.h>
+ Include dependency graph for simplify_expr.h:

Go to the source code of this file.

Functions

bool simplify (exprt &expr, const namespacet &ns)
 
exprt simplify_expr (exprt src, const namespacet &ns)
 
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. More...
 

Function Documentation

◆ simplify()

bool simplify ( exprt expr,
const namespacet ns 
)
Returns
returns true if expression unchanged; returns false if changed

Definition at line 2693 of file simplify_expr.cpp.

◆ simplify_expr()

exprt simplify_expr ( exprt  src,
const namespacet ns 
)

Definition at line 2698 of file simplify_expr.cpp.

◆ 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.

If content is of the form &id[e], where id is an array-typed symbol expression (and e is any expression), return the value of the symbol id (as given by the value field of the symbol in the namespace ns); otherwise return an empty optional.

Parameters
contentcontent field of a refined string expression
nsnamespace
Returns
array expression representing the char sequence which forms the content of the refined string expression, empty optional if the content cannot be determined

Definition at line 1837 of file simplify_expr.cpp.