10 #ifndef CPROVER_UTIL_EXPR_UTIL_H 11 #define CPROVER_UTIL_EXPR_UTIL_H 69 const std::function<
bool(
const typet &)> &pred,
100 #endif // CPROVER_UTIL_EXPR_UTIL_H The type of an expression, extends irept.
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Determine whether an expression is constant.
Operator to update elements in structs and arrays.
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
bool has_subexpr(const exprt &, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
The trinary if-then-else operator.
if_exprt lift_if(const exprt &, std::size_t operand_number)
lift up an if_exprt one level
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Operator to update elements in structs and arrays.
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Expression to hold a symbol (variable)
exprt is_not_zero(const exprt &, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans