cprover
expr_util.cpp File Reference
#include "expr_util.h"
#include <unordered_set>
#include "expr.h"
#include "expr_iterator.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "std_expr.h"
#include "symbol.h"
#include "namespace.h"
#include "arith_tools.h"
Include dependency graph for expr_util.cpp:

Go to the source code of this file.

Functions

exprt make_binary (const exprt &expr)
 splits an expression with >=3 operands into nested binary expressions More...
 
with_exprt make_with_expr (const update_exprt &src)
 converts an update expr into a (possibly nested) with expression More...
 
exprt is_not_zero (const exprt &src, const namespacet &ns)
 converts a scalar/float expression to C/C++ Booleans More...
 
exprt boolean_negate (const exprt &src)
 negate a Boolean expression, possibly removing a not_exprt, and swapping false and true More...
 
bool has_subexpr (const exprt &expr, const std::function< bool(const exprt &)> &pred)
 returns true if the expression has a subexpression that satisfies pred More...
 
bool has_subexpr (const exprt &src, const irep_idt &id)
 returns true if the expression has a subexpression with given ID More...
 
bool has_subtype (const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
 returns true if any of the contained types satisfies pred More...
 
bool has_subtype (const typet &type, const irep_idt &id, const namespacet &ns)
 returns true if any of the contained types is id More...
 
if_exprt lift_if (const exprt &src, std::size_t operand_number)
 lift up an if_exprt one level More...
 

Function Documentation

◆ boolean_negate()

◆ has_subexpr() [1/2]

bool has_subexpr ( const exprt expr,
const std::function< bool(const exprt &)> &  pred 
)

◆ has_subexpr() [2/2]

bool has_subexpr ( const exprt src,
const irep_idt id 
)

returns true if the expression has a subexpression with given ID

Definition at line 133 of file expr_util.cpp.

References has_subexpr(), and irept::id().

◆ has_subtype() [1/2]

bool has_subtype ( const typet type,
const std::function< bool(const typet &)> &  pred,
const namespacet ns 
)

returns true if any of the contained types satisfies pred

Parameters
typea type
preda predicate
nsnamespace for symbol type lookups
Returns
true if one of the subtype of type satisfies predicate pred. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc... For instance in the type t defined by { int a; char[] b; double * c; { bool d} e}, int, char, double and bool are subtypes of t.

Definition at line 139 of file expr_util.cpp.

References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), stack, typet::subtypes(), to_c_enum_tag_type(), and to_struct_union_type().

Referenced by add_string_equation_to_symbol_resolution(), has_char_pointer_subtype(), has_subtype(), and string_identifiers_resolution_from_equations().

◆ has_subtype() [2/2]

bool has_subtype ( const typet type,
const irep_idt id,
const namespacet ns 
)

returns true if any of the contained types is id

Definition at line 179 of file expr_util.cpp.

References has_subtype(), and irept::id().

◆ is_not_zero()

◆ lift_if()

◆ make_binary()

exprt make_binary ( const exprt expr)

◆ make_with_expr()

with_exprt make_with_expr ( const update_exprt src)

converts an update expr into a (possibly nested) with expression

Definition at line 53 of file expr_util.cpp.

References update_exprt::designator(), forall_expr, index_designatort::index(), with_exprt::new_value(), PRECONDITION, to_index_designator(), to_with_expr(), UNREACHABLE, and with_exprt::where().