25 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
33 op.reserve(op.size()+2);
35 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
37 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
45 op.reserve(op.size()+3);
47 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
49 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
51 op.push_back(static_cast<const exprt &>(
get_nil_irep()));
64 op.reserve(op.size()+2);
77 op.reserve(op.size()+3);
106 if(
id()==ID_not &&
operands().size()==1)
121 return id()==ID_constant;
128 get(ID_value)!=ID_false;
135 get(ID_value)==ID_false;
141 set(ID_value, value?ID_true:ID_false);
147 set(ID_value, ID_true);
153 set(ID_value, ID_false);
158 return type().
id()==ID_bool;
168 if(type_id==ID_integer || type_id==ID_natural)
172 else if(type_id==ID_rational)
179 else if(type_id==ID_unsignedbv ||
180 type_id==ID_signedbv ||
185 else if(type_id==ID_fixedbv)
190 else if(type_id==ID_floatbv)
195 else if(type_id==ID_pointer)
209 const std::string &value=
get_string(ID_value);
212 if(type_id==ID_integer || type_id==ID_natural)
218 else if(type_id==ID_rational)
223 return rat_value.
is_one();
225 else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
231 else if(type_id==ID_fixedbv)
236 else if(type_id==ID_floatbv)
265 std::stack<exprt *>
stack;
269 while(!
stack.empty())
283 std::stack<const exprt *>
stack;
287 while(!
stack.empty())
const irept & get_nil_irep()
The type of an expression.
const_unique_depth_iteratort unique_depth_cbegin() const
const mp_integer string2integer(const std::string &n, unsigned base)
const_depth_iteratort depth_cbegin() const
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
depth_iteratort depth_begin()
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)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
The boolean constant false.
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 & get_string(const irep_namet &name) const
const std::string & id_string() const
#define Forall_operands(it, expr)
const_unique_depth_iteratort unique_depth_begin() const
depth_iteratort depth_end()
void make_typecast(const typet &_type)
const_unique_depth_iteratort unique_depth_end() const