Go to the documentation of this file.
17 if(type.
id() == ID_unsignedbv)
19 else if(type.
id() == ID_bool)
21 else if(type.
id() == ID_integer)
23 else if(type.
id() == ID_real)
25 else if(type.
id() == ID_array)
28 out <<
"(Array " <<
smt2_format(array_type.size().type()) <<
' '
31 else if(type.
id() == ID_floatbv)
36 out <<
"(_ FloatingPoint " << floatbv_type.get_e() <<
' '
37 << floatbv_type.get_f() + 1 <<
')';
40 out <<
"? " << type.
id();
47 if(expr.
id() == ID_constant)
50 const auto &value = constant_expr.get_value();
53 if(expr_type.
id() == ID_unsignedbv)
57 const auto int_value = numeric_cast_v<mp_integer>(constant_expr);
59 out <<
"(_ bv" << int_value <<
" " << width <<
")";
61 else if(expr_type.
id() == ID_bool)
70 else if(expr_type.
id() == ID_integer)
74 else if(expr_type.
id() == ID_string)
78 for(
const auto &c : value)
89 else if(expr_type.
id() == ID_floatbv)
96 else if(expr.
id() == ID_symbol)
108 else if(expr.
id() == ID_with && expr.
type().
id() == ID_array)
111 out <<
"(store " <<
smt2_format(with_expr.old()) <<
' '
115 else if(expr.
id() == ID_array_list)
119 for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
125 for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
128 i < array_list_expr.operands().size() - 1,
129 "array_list has even number of operands");
130 out <<
' ' <<
smt2_format(array_list_expr.operands()[i]) <<
' '
131 <<
smt2_format(array_list_expr.operands()[i + 1]) <<
')';
135 out <<
"? " << expr.
id();
const typet & subtype() const
The type of an expression, extends irept.
Base class for all expressions.
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.
bool get_bool(const irep_namet &name) const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const irep_idt & get_identifier() const
const std::string & id_string() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
std::size_t get_width() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.