32 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
44 op.reserve(op.size()+2);
46 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
48 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
61 op.reserve(op.size()+3);
63 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
65 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
67 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
85 return id()==ID_constant;
94 get(ID_value)!=ID_false;
103 get(ID_value)==ID_false;
112 set(ID_value, value?ID_true:ID_false);
119 return type().
id()==ID_bool;
137 if(type_id==ID_integer || type_id==ID_natural)
141 else if(type_id==ID_rational)
149 type_id == ID_unsignedbv || type_id == ID_signedbv ||
150 type_id == ID_c_bool || type_id == ID_c_bit_field)
154 else if(type_id==ID_fixedbv)
159 else if(type_id==ID_floatbv)
164 else if(type_id==ID_pointer)
187 if(type_id==ID_integer || type_id==ID_natural)
194 else if(type_id==ID_rational)
199 return rat_value.
is_one();
201 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
209 else if(type_id==ID_fixedbv)
214 else if(type_id==ID_floatbv)
248 std::stack<exprt *>
stack;
252 while(!
stack.empty())
266 std::stack<const exprt *>
stack;
270 while(!
stack.empty())
const irept & get_nil_irep()
The type of an expression, extends irept.
Semantic type conversion.
const_unique_depth_iteratort unique_depth_cbegin() const
bool is_boolean() const
Return whether the expression represents a Boolean.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const_depth_iteratort depth_cbegin() const
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
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.
const irep_idt & get_value() const
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
depth_iteratort depth_begin()
A constant literal expression.
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
#define CHECK_RETURN(CONDITION)
Forward depth-first search iterators These iterators' copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
bool value_is_zero_string() const
const irep_idt & id() const
void visit(class expr_visitort &visitor)
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
API to expression classes.
#define forall_operands(it, expr)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
bool is_constant() const
Return whether the expression is a constant.
std::size_t get_width() const
std::vector< exprt > operandst
const_unique_depth_iteratort unique_depth_cend() const
Base class for all expressions.
const source_locationt & source_location() const
const_depth_iteratort depth_cend() const
const std::string & id_string() const
#define Forall_operands(it, expr)
bool is_zero() const
Return whether the expression is a constant representing 0.
const_unique_depth_iteratort unique_depth_begin() const
depth_iteratort depth_end()
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
const_unique_depth_iteratort unique_depth_end() const
bool is_one() const
Return whether the expression is a constant representing 1.