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 
15 #include <string>
16 
17 class array_exprt;
18 class namespacet;
19 
20 bool sort_operands(exprt::operandst &operands);
21 
22 bool join_operands(exprt &expr);
23 
24 bool sort_and_join(exprt &expr);
25 
26 // bit-level conversions
27 std::optional<exprt> bits2expr(
28  const std::string &bits,
29  const typet &type,
30  bool little_endian,
31  const namespacet &ns);
32 
33 std::optional<std::string>
34 expr2bits(const exprt &, bool little_endian, const namespacet &ns);
35 
48 std::optional<std::reference_wrapper<const array_exprt>>
49 try_get_string_data_array(const exprt &content, const namespacet &ns);
50 
51 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1621
exprt
Base class for all expressions.
Definition: expr.h:56
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:58
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
typet
The type of an expression, extends irept.
Definition: type.h:29
expr2bits
std::optional< std::string > expr2bits(const exprt &, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:414
sort_and_join
bool sort_and_join(exprt &expr)
Definition: simplify_utils.cpp:186
sort_operands
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
Definition: simplify_utils.cpp:28
try_get_string_data_array
std::optional< 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:489
bits2expr
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition: simplify_utils.cpp:196
join_operands
bool join_operands(exprt &expr)
Definition: simplify_utils.cpp:191