44 (sub_expr.
id() == ID_mult || sub_expr.
id() == ID_div) &&
45 (expr.
id() == ID_plus || expr.
id() == ID_minus))
50 (sub_expr.
id() == ID_equal || sub_expr.
id() == ID_notequal ||
51 sub_expr.
id() == ID_lt || sub_expr.
id() == ID_gt ||
52 sub_expr.
id() == ID_le || sub_expr.
id() == ID_ge) &&
53 (expr.
id() == ID_and || expr.
id() == ID_or))
70 os <<
' ' << src.
id() <<
' ';
97 if(src.
id() == ID_not)
99 else if(src.
id() == ID_unary_minus)
102 return os << src.
pretty();
105 return os <<
'(' <<
format(src.
op0()) <<
')';
113 auto type = src.
type().
id();
120 return os <<
"false";
122 return os << src.
pretty();
124 else if(type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool)
125 return os << *numeric_cast<mp_integer>(src);
126 else if(type == ID_integer)
128 else if(type == ID_string)
130 else if(type == ID_floatbv)
132 else if(type == ID_pointer && src.
is_zero())
135 return os << src.
pretty();
143 if(s.first != ID_type)
144 os <<
' ' << s.first <<
"=\"" << s.second.id() <<
'"';
151 for(
const auto &op : expr.
operands())
172 const auto &
id = expr.
id();
174 if(
id == ID_plus ||
id == ID_mult ||
id == ID_and ||
id == ID_or)
177 id == ID_lt ||
id == ID_gt ||
id == ID_ge ||
id == ID_le ||
178 id == ID_minus ||
id == ID_implies ||
id == ID_equal ||
id == ID_notequal)
180 else if(
id == ID_not ||
id == ID_unary_minus)
182 else if(
id == ID_constant)
184 else if(
id == ID_typecast)
187 else if(
id == ID_member)
190 else if(
id == ID_symbol)
192 else if(
id == ID_index)
195 return os <<
format(index_expr.array()) <<
'[' <<
format(index_expr.index())
198 else if(
id == ID_type)
200 else if(
id == ID_forall ||
id == ID_exists)
204 else if(
id == ID_let)
208 else if(
id == ID_array ||
id == ID_struct)
214 for(
const auto &op : expr.
operands())
229 return os <<
format(if_expr.cond()) <<
'?' <<
format(if_expr.true_case())
230 <<
':' <<
format(if_expr.false_case());
232 else if(
id == ID_code)
234 const auto &code =
to_code(expr);
235 const irep_idt &statement = code.get_statement();
237 if(statement == ID_assign)
240 else if(statement == ID_block)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
const std::string & id2string(const irep_idt &d)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & get_identifier() const
const irep_idt & get_value() const
A constant literal expression.
const let_exprt & to_let_expr(const exprt &expr)
Cast a generic exprt to a let_exprt.
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
A generic base class for binary expressions.
API to expression classes.
Generic base class for unary expressions.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast a generic exprt to a quantifier_exprt.
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.
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 a generic exprt to a constant_exprt.
bool has_operands() const
named_subt & get_named_sub()
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast a generic exprt to a multi_ary_exprt.
Base class for all expressions.
irep_idt get_component_name() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const codet & to_code(const exprt &expr)
const code_blockt & to_code_block(const codet &code)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
A generic base class for multi-ary expressions.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.