31 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
39 op.reserve(op.size()+2);
41 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
43 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
51 op.reserve(op.size()+3);
53 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
55 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
57 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
70 op.reserve(op.size()+2);
83 op.reserve(op.size()+3);
92 exprt new_expr(ID_typecast);
95 new_expr.
set(ID_type, _type);
115 if(
id()==ID_not &&
operands().size()==1)
130 return id()==ID_constant;
137 get(ID_value)!=ID_false;
144 get(ID_value)==ID_false;
150 set(ID_value, value?ID_true:ID_false);
156 set(ID_value, ID_true);
162 set(ID_value, ID_false);
175 const irep_idt &value=
get(ID_value);
177 if(type_id==ID_integer)
181 else if(type_id==ID_unsignedbv)
187 else if(type_id==ID_signedbv)
193 else if(type_id==ID_fixedbv)
199 else if(type_id==ID_floatbv)
202 ieee_float_value.
negate();
203 *
this=ieee_float_value.
to_expr();
213 if(
id()==ID_unary_minus)
217 "Unary minus must have one operand");
233 return type().
id()==ID_bool;
243 if(type_id==ID_integer || type_id==ID_natural)
247 else if(type_id==ID_rational)
254 else if(type_id==ID_unsignedbv ||
255 type_id==ID_signedbv ||
260 else if(type_id==ID_fixedbv)
265 else if(type_id==ID_floatbv)
270 else if(type_id==ID_pointer)
284 const std::string &value=
get_string(ID_value);
287 if(type_id==ID_integer || type_id==ID_natural)
293 else if(type_id==ID_rational)
298 return rat_value.
is_one();
300 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
306 else if(type_id==ID_fixedbv)
311 else if(type_id==ID_floatbv)
330 if(type_id==ID_integer || type_id==ID_natural)
337 else if(type_id==ID_rational)
347 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
355 else if(type_id==ID_fixedbv)
363 else if(type_id==ID_floatbv)
383 if(type_id==ID_integer || type_id==ID_natural)
390 else if(type_id==ID_rational)
400 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
409 else if(type_id==ID_fixedbv)
416 else if(type_id==ID_floatbv)
437 if(type_id==ID_integer || type_id==ID_natural)
444 else if(type_id==ID_rational)
450 set(ID_value, a_minus_b.
get_string(ID_value));
454 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
485 std::stack<exprt *>
stack;
489 while(!
stack.empty())
503 std::stack<const exprt *>
stack;
507 while(!
stack.empty())
const irept & get_nil_irep()
The type of an expression.
const std::string & id2string(const irep_idt &d)
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
constant_exprt to_expr() const
unsigned unsafe_string2unsigned(const std::string &str, int base)
void copy_to_operands(const exprt &expr)
void move_to_operands(exprt &expr)
const irep_idt & get_value() const
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
A constant literal expression.
void make_bool(bool value)
#define CHECK_RETURN(CONDITION)
bool value_is_zero_string() const
const irep_idt & id() const
void visit(class expr_visitort &visitor)
The boolean constant true.
const source_locationt & find_source_location() const
API to expression classes.
#define forall_operands(it, expr)
constant_exprt to_expr() const
The boolean constant false.
std::vector< exprt > operandst
bool mul(const exprt &expr)
Base class for all expressions.
const source_locationt & source_location() const
const std::string integer2binary(const mp_integer &n, std::size_t width)
const std::string & get_string(const irep_namet &name) const
bool subtract(const exprt &expr)
const std::string & id_string() const
#define Forall_operands(it, expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
#define DATA_INVARIANT(CONDITION, REASON)
bool sum(const exprt &expr)
void make_typecast(const typet &_type)
void set(const irep_namet &name, const irep_idt &value)