cprover
smt2_format.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "smt2_format.h"
10
11#include <util/arith_tools.h>
13#include <util/ieee_float.h>
14
15std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
16{
17 if(type.id() == ID_unsignedbv)
18 out << "(_ BitVec " << to_unsignedbv_type(type).get_width() << ')';
19 else if(type.id() == ID_bool)
20 out << "Bool";
21 else if(type.id() == ID_integer)
22 out << "Int";
23 else if(type.id() == ID_real)
24 out << "Real";
25 else if(type.id() == ID_array)
26 {
27 const auto &array_type = to_array_type(type);
28 out << "(Array " << smt2_format(array_type.size().type()) << ' '
29 << smt2_format(array_type.element_type()) << ')';
30 }
31 else if(type.id() == ID_floatbv)
32 {
33 const auto &floatbv_type = to_floatbv_type(type);
34 // the width of the mantissa needs to be increased by one to
35 // include the hidden bit
36 out << "(_ FloatingPoint " << floatbv_type.get_e() << ' '
37 << floatbv_type.get_f() + 1 << ')';
38 }
39 else
40 out << "? " << type.id();
41
42 return out;
43}
44
45std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
46{
47 if(expr.id() == ID_constant)
48 {
49 const auto &constant_expr = to_constant_expr(expr);
50 const auto &value = constant_expr.get_value();
51 const typet &expr_type = expr.type();
52
53 if(expr_type.id() == ID_unsignedbv)
54 {
55 const std::size_t width = to_unsignedbv_type(expr_type).get_width();
56
57 const auto int_value = numeric_cast_v<mp_integer>(constant_expr);
58
59 out << "(_ bv" << int_value << " " << width << ")";
60 }
61 else if(expr_type.id() == ID_bool)
62 {
63 if(expr.is_true())
64 out << "true";
65 else if(expr.is_false())
66 out << "false";
67 else
68 DATA_INVARIANT(false, "unknown Boolean constant");
69 }
70 else if(expr_type.id() == ID_integer)
71 {
72 // negative numbers need to be encoded using a unary minus expression
73 auto int_value = numeric_cast_v<mp_integer>(constant_expr);
74 if(int_value < 0)
75 out << "(- " << -int_value << ')';
76 else
77 out << int_value;
78 }
79 else if(expr_type.id() == ID_string)
80 {
81 out << '"';
82
83 for(const auto &c : value)
84 {
85 // " is the only escape sequence
86 if(c == '"')
87 out << '"' << '"';
88 else
89 out << c;
90 }
91
92 out << '"';
93 }
94 else if(expr_type.id() == ID_floatbv)
95 {
96 const ieee_floatt v = ieee_floatt(constant_expr);
97 const size_t e = v.spec.e;
98 const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit
99
100 if(v.is_NaN())
101 {
102 out << "(_ NaN " << e << " " << f << ")";
103 }
104 else if(v.is_infinity())
105 {
106 if(v.get_sign())
107 out << "(_ -oo " << e << " " << f << ")";
108 else
109 out << "(_ +oo " << e << " " << f << ")";
110 }
111 else
112 {
113 // Zero, normal or subnormal
114
115 mp_integer binary = v.pack();
116 std::string binaryString(integer2binary(v.pack(), v.spec.width()));
117
118 out << "(fp "
119 << "#b" << binaryString.substr(0, 1) << " "
120 << "#b" << binaryString.substr(1, e) << " "
121 << "#b" << binaryString.substr(1 + e, f - 1) << ")";
122 }
123 }
124 else
125 DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string());
126 }
127 else if(expr.id() == ID_symbol)
128 {
129 const auto &identifier = to_symbol_expr(expr).get_identifier();
130 if(expr.get_bool("#quoted"))
131 {
132 out << '|';
133 out << identifier;
134 out << '|';
135 }
136 else
137 out << identifier;
138 }
139 else if(expr.id() == ID_with && expr.type().id() == ID_array)
140 {
141 const auto &with_expr = to_with_expr(expr);
142 out << "(store " << smt2_format(with_expr.old()) << ' '
143 << smt2_format(with_expr.where()) << ' '
144 << smt2_format(with_expr.new_value()) << ')';
145 }
146 else if(expr.id() == ID_array_list)
147 {
148 const auto &array_list_expr = to_multi_ary_expr(expr);
149
150 for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
151 out << "(store ";
152
153 out << "((as const " << smt2_format(expr.type()) << ")) "
154 << smt2_format(
156 << ')';
157
158 for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
159 {
161 i < array_list_expr.operands().size() - 1,
162 "array_list has even number of operands");
163 out << ' ' << smt2_format(array_list_expr.operands()[i]) << ' '
164 << smt2_format(array_list_expr.operands()[i + 1]) << ')';
165 }
166 }
167 else
168 out << "? " << expr.id();
169
170 return out;
171}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
std::size_t get_width() const
Definition: std_types.h:864
Base class for all expressions.
Definition: expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
std::size_t f
Definition: ieee_float.h:27
std::size_t width() const
Definition: ieee_float.h:51
std::size_t e
Definition: ieee_float.h:27
ieee_float_spect spec
Definition: ieee_float.h:135
bool is_NaN() const
Definition: ieee_float.h:249
bool get_sign() const
Definition: ieee_float.h:248
bool is_infinity() const
Definition: ieee_float.h:250
mp_integer pack() const
Definition: ieee_float.cpp:374
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The type of an expression, extends irept.
Definition: type.h:29
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
std::ostream & smt2_format_rec(std::ostream &out, const typet &type)
Definition: smt2_format.cpp:15
static smt2_format_containert< T > smt2_format(const T &_o)
Definition: smt2_format.h:28
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:899
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832