CBMC
simplify_utils.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_UTILS_H
11 #define CPROVER_UTIL_SIMPLIFY_UTILS_H
12 
13 #include "expr.h"
14 #include "optional.h"
15 
16 #include <string>
17 
18 class array_exprt;
19 class namespacet;
20 
21 bool sort_operands(exprt::operandst &operands);
22 
23 bool join_operands(exprt &expr);
24 
25 bool sort_and_join(exprt &expr);
26 
27 // bit-level conversions
29  const std::string &bits,
30  const typet &type,
31  bool little_endian,
32  const namespacet &ns);
33 
35 expr2bits(const exprt &, bool little_endian, const namespacet &ns);
36 
50 try_get_string_data_array(const exprt &content, const namespacet &ns);
51 
52 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H
typet
The type of an expression, extends irept.
Definition: type.h:28
optional.h
exprt
Base class for all expressions.
Definition: expr.h:55
join_operands
bool join_operands(exprt &expr)
Definition: simplify_utils.cpp:189
expr2bits
optionalt< std::string > expr2bits(const exprt &, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:409
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
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_utils.cpp:484
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:58
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
sort_operands
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
Definition: simplify_utils.cpp:28
bits2expr
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:194
sort_and_join
bool sort_and_join(exprt &expr)
Definition: simplify_utils.cpp:184
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1562