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#include "optional.h"
15
16#include <string>
17
18class array_exprt;
19class namespacet;
20
21bool sort_operands(exprt::operandst &operands);
22
23bool join_operands(exprt &expr);
24
25bool 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
35expr2bits(const exprt &, bool little_endian, const namespacet &ns);
36
50try_get_string_data_array(const exprt &content, const namespacet &ns);
51
52#endif // CPROVER_UTIL_SIMPLIFY_UTILS_H
Array constructor from list of elements.
Definition: std_expr.h:1476
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
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
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< exprt > bits2expr(const std::string &bits, const typet &type, bool little_endian, const namespacet &ns)
bool sort_and_join(exprt &expr)
optionalt< 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<
bool join_operands(exprt &expr)
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.