cprover
expr_util.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_EXPR_UTIL_H
11 #define CPROVER_UTIL_EXPR_UTIL_H
12 
20 #include "irep.h"
21 
22 #include <functional>
23 
24 class exprt;
25 class symbol_exprt;
26 class update_exprt;
27 class with_exprt;
28 class if_exprt;
29 class symbolt;
30 class typet;
31 class namespacet;
32 
34 exprt make_binary(const exprt &);
35 
38 
40 exprt is_not_zero(const exprt &, const namespacet &ns);
41 
44 exprt boolean_negate(const exprt &);
45 
47 bool has_subexpr(const exprt &, const std::function<bool(const exprt &)> &pred);
48 
50 bool has_subexpr(const exprt &, const irep_idt &);
51 
64 bool has_subtype(
65  const typet &type,
66  const std::function<bool(const typet &)> &pred,
67  const namespacet &ns);
68 
70 bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
71 
73 if_exprt lift_if(const exprt &, std::size_t operand_number);
74 
75 #endif // CPROVER_UTIL_EXPR_UTIL_H
The type of an expression.
Definition: type.h:22
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:113
Operator to update elements in structs and arrays.
Definition: std_expr.h:3672
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:22
bool has_subexpr(const exprt &, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:125
The trinary if-then-else operator.
Definition: std_expr.h:3361
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
if_exprt lift_if(const exprt &, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:185
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:53
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
Definition: expr_util.cpp:139
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Base class for all expressions.
Definition: expr.h:42
Operator to update elements in structs and arrays.
Definition: std_expr.h:3461
Expression to hold a symbol (variable)
Definition: std_expr.h:90
exprt is_not_zero(const exprt &, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:84