9 #ifndef CPROVER_UTIL_EXPR_H 10 #define CPROVER_UTIL_EXPR_H 20 #define forall_operands(it, expr) \ 21 if((expr).has_operands()) \ 22 for(exprt::operandst::const_iterator it=(expr).operands().begin(), \ 23 it##_end=(expr).operands().end(); \ 26 #define Forall_operands(it, expr) \ 27 if((expr).has_operands()) \ 28 for(exprt::operandst::iterator it=(expr).operands().begin(); \ 29 it!=(expr).operands().end(); ++it) 31 #define forall_expr(it, expr) \ 32 for(exprt::operandst::const_iterator it=(expr).begin(); \ 33 it!=(expr).end(); ++it) 35 #define Forall_expr(it, expr) \ 36 for(exprt::operandst::iterator it=(expr).begin(); \ 37 it!=(expr).end(); ++it) 71 return static_cast<const typet &>(
find(ID_type));
111 DEPRECATED(
"use add_to_operands(std::move(expr)) instead")
118 "use
add_to_operands(std::move(e1), std::move(e2), std::move(e3)) instead")
139 operands().push_back(std::move(expr));
149 op.reserve(op.size() + 2);
170 op.reserve(op.size() + 2);
172 op.push_back(std::move(e1));
173 op.push_back(std::move(e2));
193 op.reserve(op.size() + 3);
208 op.reserve(op.size() + 3);
210 op.push_back(std::move(e1));
211 op.push_back(std::move(e2));
212 op.push_back(std::move(e3));
230 return static_cast<const source_locationt &>(
find(ID_C_source_location));
235 return static_cast<source_locationt &>(
add(ID_C_source_location));
296 return static_cast<exprt &>(
add(name));
301 return static_cast<const exprt &>(
find(name));
335 #endif // CPROVER_UTIL_EXPR_H The type of an expression, extends irept.
virtual void operator()(const exprt &)
const_unique_depth_iteratort unique_depth_cbegin() const
bool is_boolean() const
Return whether the expression represents a Boolean.
static void validate_full(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Check that the expression is well-formed (full check, including checks of all subexpressions and the ...
void validate_expr(const exprt &)
Called after casting.
const_depth_iteratort depth_cbegin() const
void check_expr(const exprt &expr, const validation_modet vm)
Check that the given expression is well-formed (shallow checks only, i.e., subexpressions and its typ...
const exprt & op3() const
const exprt & op2() const
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
bool is_false() const
Return whether the expression is a constant representing false.
exprt(const irep_idt &_id)
void add_to_operands(exprt &&e1, exprt &&e2)
Add the given arguments to the end of exprt's operands.
const exprt & find_expr(const irep_idt &name) const
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
unsignedbv_typet size_type()
depth_iteratort depth_begin()
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
void add_to_operands(const exprt &e1, const exprt &e2)
Add the given arguments to the end of exprt's operands.
void copy_to_operands(const exprt &e1, const exprt &e2)
Copy the given arguments to the end of exprt's operands.
void visit(class expr_visitort &visitor)
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
Copy the given arguments to the end of exprt's operands.
void add_to_operands(exprt &&expr)
Add the given argument to the end of exprt's operands.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
exprt(const irep_idt &_id, const typet &_type)
const operandst & operands() const
Base class for tree-like data structures with sharing.
const typet & type() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void add_to_operands(exprt &&e1, exprt &&e2, exprt &&e3)
Add the given arguments to the end of exprt's operands.
bool has_operands() const
Return true if there is at least one operand.
bool is_constant() const
Return whether the expression is a constant.
std::vector< exprt > operandst
const_unique_depth_iteratort unique_depth_cend() const
const exprt & op1() const
const exprt & op0() const
Base class for all expressions.
void add_to_operands(const exprt &e1, const exprt &e2, const exprt &e3)
Add the given arguments to the end of exprt's operands.
static void check(const exprt &, const validation_modet)
Check that the expression is well-formed (shallow checks only, i.e., subexpressions and its type are ...
static void validate(const exprt &expr, const namespacet &, const validation_modet vm=validation_modet::INVARIANT)
Check that the expression is well-formed, assuming that its subexpressions and type have all ready be...
virtual void operator()(exprt &)
const source_locationt & source_location() const
const_depth_iteratort depth_cend() const
irept & add(const irep_namet &name)
bool is_zero() const
Return whether the expression is a constant representing 0.
source_locationt & add_source_location()
const_unique_depth_iteratort unique_depth_begin() const
depth_iteratort depth_end()
exprt & add_expr(const irep_idt &name)
virtual ~const_expr_visitort()
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
const irept & find(const irep_namet &name) const
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
const_unique_depth_iteratort unique_depth_end() const
void reserve_operands(operandst::size_type n)
Defines typet, type_with_subtypet and type_with_subtypest.
bool is_one() const
Return whether the expression is a constant representing 1.