Go to the documentation of this file.
16 if(type.
id() == ID_unsignedbv)
18 else if(type.
id() == ID_bool)
20 else if(type.
id() == ID_integer)
22 else if(type.
id() == ID_real)
24 else if(type.
id() == ID_array)
27 out <<
"(Array " <<
smt2_format(array_type.size().type()) <<
' '
30 else if(type.
id() == ID_floatbv)
35 out <<
"(_ FloatingPoint " << floatbv_type.get_e() <<
' '
36 << floatbv_type.get_f() + 1 <<
')';
39 out <<
"? " << type.
id();
46 if(expr.
id() == ID_constant)
49 const auto &value = constant_expr.get_value();
52 if(expr_type.
id() == ID_unsignedbv)
56 const auto int_value = numeric_cast_v<mp_integer>(constant_expr);
58 out <<
"(_ bv" << int_value <<
" " << width <<
")";
60 else if(expr_type.
id() == ID_bool)
69 else if(expr_type.
id() == ID_integer)
72 auto int_value = numeric_cast_v<mp_integer>(constant_expr);
74 out <<
"(- " << -int_value <<
')';
78 else if(expr_type.
id() == ID_string)
82 for(
const auto &c : value)
93 else if(expr_type.
id() == ID_floatbv)
100 else if(expr.
id() == ID_symbol)
112 else if(expr.
id() == ID_with && expr.
type().
id() == ID_array)
115 out <<
"(store " <<
smt2_format(with_expr.old()) <<
' '
119 else if(expr.
id() == ID_array_list)
123 for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
129 for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
132 i < array_list_expr.operands().size() - 1,
133 "array_list has even number of operands");
134 out <<
' ' <<
smt2_format(array_list_expr.operands()[i]) <<
' '
135 <<
smt2_format(array_list_expr.operands()[i + 1]) <<
')';
139 out <<
"? " << expr.
id();
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const typet & subtype() const
The type of an expression, extends irept.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
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
#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
Pre-defined bitvector types.
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 multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.