10 #ifndef CPROVER_UTIL_EXPR_UTIL_H 11 #define CPROVER_UTIL_EXPR_UTIL_H 55 #endif // CPROVER_UTIL_EXPR_UTIL_H The type of an expression.
exprt boolean_negate(const exprt &)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Operator to update elements in structs and arrays.
exprt make_binary(const exprt &)
splits an expression with >=3 operands into nested binary expressions
The trinary if-then-else operator.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
if_exprt lift_if(const exprt &, std::size_t operand_number)
lift up an if_exprt one level
void make_next_state(exprt &)
with_exprt make_with_expr(const update_exprt &)
converts an update expr into a (possibly nested) with expression
Base class for all expressions.
Operator to update elements in structs and arrays.
bool has_subexpr(const exprt &, const irep_idt &)
returns true if the expression has a subexpression with given ID
Expression to hold a symbol (variable)
exprt is_not_zero(const exprt &, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans