CBMC
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 constructor from list of elements.
Definition std_expr.h:1621
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
bool sort_and_join(exprt &expr)
std::optional< std::string > expr2bits(const exprt &, bool little_endian, const namespacet &ns)
bool sort_operands(exprt::operandst &operands)
sort operands of an expression according to ordering defined by operator<
std::optional< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
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.
bool join_operands(exprt &expr)