41 {ID_notequal, {
u8"\u2260"}},
42 {ID_and, {
u8"\u2227"}},
43 {ID_or, {
u8"\u2228"}},
44 {ID_xor, {
u8"\u2295"}},
45 {ID_implies, {
u8"\u21d2"}},
46 {ID_le, {
u8"\u2264"}},
47 {ID_ge, {
u8"\u2265"}},
68 (sub_expr.
id() == ID_mult || sub_expr.
id() == ID_div) &&
69 (expr.
id() == ID_plus || expr.
id() == ID_minus))
74 (sub_expr.
id() == ID_equal || sub_expr.
id() == ID_notequal ||
75 sub_expr.
id() == ID_lt || sub_expr.
id() == ID_gt ||
76 sub_expr.
id() == ID_le || sub_expr.
id() == ID_ge) &&
77 (expr.
id() == ID_and || expr.
id() == ID_or))
82 (sub_expr.
id() == ID_plus || sub_expr.
id() == ID_minus ||
83 sub_expr.
id() == ID_mult || sub_expr.
id() == ID_div) &&
84 (expr.
id() == ID_equal || expr.
id() == ID_notequal || expr.
id() == ID_lt ||
85 expr.
id() == ID_gt || expr.
id() == ID_le || expr.
id() == ID_ge))
103 operator_str =
u8"\u21d4";
109 operator_str = infix_map_it->second.rep;
112 for(
const auto &op : src.
operands())
117 os <<
' ' << operator_str <<
' ';
144 if(src.
id() == ID_not)
146 else if(src.
id() == ID_unary_minus)
148 else if(src.
id() == ID_count_leading_zeros)
150 else if(src.
id() == ID_count_trailing_zeros)
152 else if(src.
id() == ID_find_first_set)
155 return os << src.
pretty();
158 return os <<
'(' <<
format(src.
op()) <<
')';
174 auto type = src.
type().
id();
181 return os <<
"false";
183 return os << src.
pretty();
186 type == ID_unsignedbv || type == ID_signedbv || type == ID_c_bool ||
187 type == ID_c_bit_field)
188 return os << *numeric_cast<mp_integer>(src);
189 else if(type == ID_bv)
197 result.reserve(width + 2);
200 for(std::size_t i = 0; i < width; i++)
201 result +=
get_bvrep_bit(value, width, width - i - 1) ?
'1' :
'0';
205 else if(type == ID_integer || type == ID_natural || type == ID_range)
207 else if(type == ID_string)
209 else if(type == ID_floatbv)
211 else if(type == ID_pointer)
214 return os << ID_NULL;
218 return os <<
"INVALID-POINTER";
225 return os <<
"pointer(0x" <<
integer2string(int_value, 16) <<
", "
229 else if(type == ID_c_enum_tag)
234 return os << src.
pretty();
242 if(s.first != ID_type && s.first != ID_C_source_location)
243 os <<
' ' << s.first <<
"=\"" << s.second.id() <<
'"';
250 for(
const auto &op : expr.
operands())
275 std::function<std::ostream &(std::ostream &,
const exprt &)>;
276 using expr_mapt = std::unordered_map<irep_idt, formattert>;
295 auto multi_ary_expr =
296 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
306 auto binary_infix_expr =
307 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
311 expr_map[ID_lt] = binary_infix_expr;
312 expr_map[ID_gt] = binary_infix_expr;
313 expr_map[ID_ge] = binary_infix_expr;
314 expr_map[ID_le] = binary_infix_expr;
315 expr_map[ID_div] = binary_infix_expr;
316 expr_map[ID_minus] = binary_infix_expr;
317 expr_map[ID_implies] = binary_infix_expr;
318 expr_map[ID_equal] = binary_infix_expr;
319 expr_map[ID_notequal] = binary_infix_expr;
321 auto binary_prefix_expr =
322 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
328 expr_map[ID_ieee_float_equal] = binary_prefix_expr;
329 expr_map[ID_ieee_float_notequal] = binary_prefix_expr;
331 auto unary_expr = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
336 expr_map[ID_unary_minus] = unary_expr;
338 auto unary_with_parentheses_expr =
339 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
343 expr_map[ID_isnan] = unary_with_parentheses_expr;
344 expr_map[ID_isinf] = unary_with_parentheses_expr;
345 expr_map[ID_isfinite] = unary_with_parentheses_expr;
346 expr_map[ID_isnormal] = unary_with_parentheses_expr;
349 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
353 expr_map[ID_floatbv_plus] = ternary_expr;
354 expr_map[ID_floatbv_minus] = ternary_expr;
355 expr_map[ID_floatbv_mult] = ternary_expr;
356 expr_map[ID_floatbv_div] = ternary_expr;
357 expr_map[ID_floatbv_mod] = ternary_expr;
360 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
365 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
367 return os <<
"address_of(" <<
format(address_of.object()) <<
')';
370 expr_map[ID_annotated_pointer_constant] =
371 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
373 return os <<
format(annotated_pointer.symbolic_pointer());
377 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
379 <<
format(expr.type()) <<
')';
383 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
385 <<
", " <<
format(expr.type()) <<
')';
389 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
391 return os <<
"floatbv_typecast(" <<
format(floatbv_typecast_expr.op())
392 <<
", " <<
format(floatbv_typecast_expr.type()) <<
", "
393 <<
format(floatbv_typecast_expr.rounding_mode()) <<
')';
397 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
399 return os << expr.id() <<
'(' <<
format(byte_extract_expr.op()) <<
", "
400 <<
format(byte_extract_expr.offset()) <<
", "
401 <<
format(byte_extract_expr.type()) <<
')';
404 expr_map[ID_byte_extract_little_endian] = byte_extract;
405 expr_map[ID_byte_extract_big_endian] = byte_extract;
407 auto byte_update = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
409 return os << expr.id() <<
'(' <<
format(byte_update_expr.op()) <<
", "
410 <<
format(byte_update_expr.offset()) <<
", "
411 <<
format(byte_update_expr.value()) <<
", "
412 <<
format(byte_update_expr.type()) <<
')';
415 expr_map[ID_byte_update_little_endian] = byte_update;
416 expr_map[ID_byte_update_big_endian] = byte_update;
419 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
425 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
430 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
432 return os <<
format(index_expr.array()) <<
'[' <<
format(index_expr.index())
437 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
442 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
457 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
471 expr_map[ID_let] = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
478 const auto &values = let_expr.values();
479 auto values_it = values.begin();
480 for(
auto &v : let_expr.variables())
491 return os <<
" IN " <<
format(let_expr.where());
495 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
502 for(
auto &v : lambda_expr.variables())
512 return os <<
" . " <<
format(lambda_expr.where());
515 auto compound = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
520 for(
const auto &op : expr.operands())
537 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
539 return os <<
"array_of(" <<
format(array_of_expr.what()) <<
')';
542 expr_map[ID_if] = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
544 return os <<
'(' <<
format(if_expr.cond()) <<
" ? "
545 <<
format(if_expr.true_case()) <<
" : "
546 <<
format(if_expr.false_case()) <<
')';
550 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
551 return os <<
'"' << expr.get_string(ID_value) <<
'"';
555 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
557 os <<
format(function_application_expr.function()) <<
'(';
559 for(
auto &argument : function_application_expr.arguments())
572 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
575 if(dereference_expr.pointer().id() != ID_symbol)
576 os <<
'(' <<
format(dereference_expr.pointer()) <<
')';
578 os <<
format(dereference_expr.pointer());
583 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
585 return os <<
"saturating-(" <<
format(saturating_minus.lhs()) <<
", "
586 <<
format(saturating_minus.rhs()) <<
')';
590 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
592 return os <<
"saturating+(" <<
format(saturating_plus.lhs()) <<
", "
593 <<
format(saturating_plus.rhs()) <<
')';
597 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
599 return os <<
u8"\u275d" << object_address_expr.object_identifier()
604 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
606 return os <<
"object_size(" <<
format(object_size_expr.op()) <<
')';
610 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
612 return os <<
"pointer_offset(" <<
format(pointer_offset_expr.op()) <<
')';
616 [](std::ostream &os,
const exprt &expr) -> std::ostream & {
618 return os <<
format(field_address_expr.base()) <<
u8".\u275d"
619 << field_address_expr.component_name() <<
u8"\u275e";
622 fallback = [](std::ostream &os,
const exprt &expr) -> std::ostream & {
647 return formatter(os, expr);
API to expression classes for bitvectors.
const saturating_plus_exprt & to_saturating_plus_expr(const exprt &expr)
Cast an exprt to a saturating_plus_exprt.
const zero_extend_exprt & to_zero_extend_expr(const exprt &expr)
Cast an exprt to a zero_extend_exprt.
const saturating_minus_exprt & to_saturating_minus_expr(const exprt &expr)
Cast an exprt to a saturating_minus_exprt.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
A base class for binary expressions.
std::size_t get_width() const
A constant literal expression.
const irep_idt & get_value() const
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Base class for all expressions.
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
named_subt & get_named_sub()
const irep_idt & id() const
irep_idt get_component_name() const
A base class for multi-ary expressions Associativity is not specified.
const typet & base_type() const
The type of the data what we point to.
const irep_idt & get_identifier() const
An expression with three operands.
Generic base class for unary expressions.
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast an exprt to a function_application_exprt.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
API to expression classes for Pointers.
const object_size_exprt & to_object_size_expr(const exprt &expr)
Cast an exprt to a object_size_exprt.
const annotated_pointer_constant_exprt & to_annotated_pointer_constant_expr(const exprt &expr)
Cast an exprt to an annotated_pointer_constant_exprt.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const ternary_exprt & to_ternary_expr(const exprt &expr)
Cast an exprt to a ternary_exprt.
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
std::string escape(const std::string &s)
Generic escaping of strings; this is not meant to be a particular programming language.