cprover
Loading...
Searching...
No Matches
simplify_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
17class array_exprt;
18class namespacet;
19
20bool sort_operands(exprt::operandst &operands);
21
22bool join_operands(exprt &expr);
23
24bool sort_and_join(exprt &expr);
25
26// bit-level conversions
27std::optional<exprt> bits2expr(
28 const std::string &bits,
29 const typet &type,
30 bool little_endian,
31 const namespacet &ns);
32
33std::optional<std::string>
34expr2bits(const exprt &, bool little_endian, const namespacet &ns);
35
48std::optional<std::reference_wrapper<const array_exprt>>
49try_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:1560
exprt
Base class for all expressions.
Definition expr.h:57
exprt::operandst
std::vector< exprt > operandst
Definition expr.h:59
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
typet
The type of an expression, extends irept.
Definition type.h:29
bits
const std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::bits
Definition sharing_map.h:1467
sort_and_join
bool sort_and_join(exprt &expr)
Definition simplify_utils.cpp:186
expr2bits
std::optional< std::string > expr2bits(const exprt &, bool little_endian, const namespacet &ns)
Definition simplify_utils.cpp:414
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
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
Definition simplify_utils.cpp:196
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
join_operands
bool join_operands(exprt &expr)
Definition simplify_utils.cpp:191