Go to the documentation of this file.
33 for(
const auto &op : ops)
39 count = op.bounded_size(count, limit);
55 return id()==ID_constant;
64 get(ID_value)!=ID_false;
73 get(ID_value)==ID_false;
80 return type().
id()==ID_bool;
98 if(type_id==ID_integer || type_id==ID_natural)
102 else if(type_id==ID_rational)
110 type_id == ID_unsignedbv || type_id == ID_signedbv ||
111 type_id == ID_c_bool || type_id == ID_c_bit_field)
115 else if(type_id==ID_fixedbv)
120 else if(type_id==ID_floatbv)
125 else if(type_id==ID_pointer)
148 if(type_id==ID_integer || type_id==ID_natural)
155 else if(type_id==ID_rational)
160 return rat_value.
is_one();
163 type_id == ID_unsignedbv || type_id == ID_signedbv ||
164 type_id == ID_c_bool || type_id == ID_c_bit_field)
172 else if(type_id==ID_fixedbv)
177 else if(type_id==ID_floatbv)
209 template <
typename T>
215 bool operands_pushed;
216 explicit stack_entryt(T *_e) : e(_e), operands_pushed(
false)
221 std::stack<stack_entryt> stack;
223 stack.emplace(_expr);
225 while(!stack.empty())
227 auto &top = stack.top();
228 if(top.operands_pushed)
236 top.operands_pushed =
true;
237 for(
auto &op : top.e->operands())
253 template <
typename T>
256 std::stack<T *> stack;
260 while(!stack.empty())
262 T &expr = *stack.top();
267 for(
auto &op : expr.operands())
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const_depth_iteratort depth_cbegin() const
depth_iteratort depth_begin()
#define CHECK_RETURN(CONDITION)
const mp_integer string2integer(const std::string &n, unsigned base)
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Pre-defined bitvector types.
std::size_t bounded_size(std::size_t limit) const
Amount of nodes in this expression tree approximately bounded by limit.
const std::string & id_string() const
void visit_post_template(std::function< void(T &)> visitor, T *_expr)
const irep_idt & id() const
static void visit_pre_template(std::function< void(T &)> visitor, T *_expr)
std::size_t get_width() const
bool is_zero() const
Return whether the expression is a constant representing 0.
Forward depth-first search iterators These iterators' copy operations are expensive,...
const irep_idt & get(const irep_namet &name) const
const_depth_iteratort depth_cend() const
bool value_is_zero_string() const
bool is_constant() const
Return whether the expression is a constant.
const_unique_depth_iteratort unique_depth_cend() const
void visit_pre(std::function< void(exprt &)>)
bool is_one() const
Return whether the expression is a constant representing 1.
const irept & get_nil_irep()
const_unique_depth_iteratort unique_depth_begin() const
const_unique_depth_iteratort unique_depth_cbegin() const
A constant literal expression.
const_unique_depth_iteratort unique_depth_end() const
depth_iteratort depth_end()
bool is_boolean() const
Return whether the expression represents a Boolean.
API to expression classes.
const irep_idt & get_value() const
const source_locationt & source_location() const
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.