cprover
smt_to_smt2_string.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
10
11#include <util/range.h>
12#include <util/string_utils.h>
13
14#include <functional>
15#include <iostream>
16#include <sstream>
17#include <stack>
18#include <string>
19
21{
22protected:
23 std::ostream &os;
24
25public:
26 explicit smt_sort_output_visitort(std::ostream &os) : os(os)
27 {
28 }
29
30 void visit(const smt_bool_sortt &) override
31 {
32 os << "Bool";
33 }
34
35 void visit(const smt_bit_vector_sortt &bit_vec) override
36 {
37 os << "(_ BitVec " << bit_vec.bit_width() << ")";
38 }
39};
40
41std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
42{
44 return os;
45}
46
47std::string smt_to_smt2_string(const smt_sortt &sort)
48{
49 std::stringstream ss;
50 ss << sort;
51 return ss.str();
52}
53
70{
71private:
72 using output_functiont = std::function<void(std::ostream &)>;
73 std::stack<output_functiont> output_stack;
74
75 static output_functiont make_output_function(const std::string &output);
79 const std::vector<std::reference_wrapper<const smt_termt>> &output);
80
82 template <typename outputt>
83 void push_output(outputt &&output);
84
86 void push_outputs();
87
99 template <typename outputt, typename... outputst>
100 void push_outputs(outputt &&output, outputst &&... outputs);
101
103
104 void visit(const smt_bool_literal_termt &bool_literal) override;
105 void visit(const smt_identifier_termt &identifier_term) override;
106 void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override;
107 void
108 visit(const smt_function_application_termt &function_application) override;
109
110public:
114 static std::ostream &convert(std::ostream &os, const smt_termt &term);
115};
116
119{
120 // `output` must be captured by value to avoid dangling references.
121 return [output](std::ostream &os) { os << output; };
122}
123
126{
127 return [=](std::ostream &os) { os << output; };
128}
129
132{
133 return [=](std::ostream &os) { output.accept(*this); };
134}
135
138 const std::vector<std::reference_wrapper<const smt_termt>> &outputs)
139{
140 return [=](std::ostream &os) {
141 for(const auto &output : make_range(outputs.rbegin(), outputs.rend()))
142 {
143 push_outputs(" ", output.get());
144 }
145 };
146}
147
148template <typename outputt>
150{
151 output_stack.push(make_output_function(std::forward<outputt>(output)));
152}
153
155{
156}
157
158template <typename outputt, typename... outputst>
160 outputt &&output,
161 outputst &&... outputs)
162{
163 push_outputs(std::forward<outputst>(outputs)...);
164 push_output(std::forward<outputt>(output));
165}
166
168 const smt_bool_literal_termt &bool_literal)
169{
170 push_output(bool_literal.value() ? "true" : "false");
171}
172
174 const smt_identifier_termt &identifier_term)
175{
177 "|", smt2_convt::convert_identifier(identifier_term.identifier()), "|");
178}
179
181 const smt_bit_vector_constant_termt &bit_vector_constant)
182{
183 auto value = integer2string(bit_vector_constant.value());
184 auto bit_width = std::to_string(bit_vector_constant.get_sort().bit_width());
185 push_outputs("(_ bv", std::move(value), " ", std::move(bit_width), ")");
186}
187
189 const smt_function_application_termt &function_application)
190{
191 const auto &id = function_application.function_identifier();
192 auto arguments = function_application.arguments();
193 push_outputs("(", id, std::move(arguments), ")");
194}
195
196std::ostream &
198{
200 term.accept(converter);
201 while(!converter.output_stack.empty())
202 {
203 auto output_function = std::move(converter.output_stack.top());
204 converter.output_stack.pop();
205 output_function(os);
206 }
207 return os;
208}
209
210std::ostream &operator<<(std::ostream &os, const smt_termt &term)
211{
213}
214
215std::string smt_to_smt2_string(const smt_termt &term)
216{
217 std::stringstream ss;
218 ss << term;
219 return ss.str();
220}
221
224{
225protected:
226 std::ostream &os;
227
228public:
229 explicit smt_option_to_string_convertert(std::ostream &os) : os(os)
230 {
231 }
232
233 void visit(const smt_option_produce_modelst &produce_models) override
234 {
235 os << ":produce-models " << (produce_models.setting() ? "true" : "false");
236 }
237};
238
239std::ostream &operator<<(std::ostream &os, const smt_optiont &option)
240{
242 return os;
243}
244
245std::string smt_to_smt2_string(const smt_optiont &option)
246{
247 std::stringstream ss;
248 ss << option;
249 return ss.str();
250}
251
253{
254protected:
255 std::ostream &os;
256
257public:
258 explicit smt_logic_to_string_convertert(std::ostream &os) : os(os)
259 {
260 }
261
262#define LOGIC_ID(the_id, the_name) \
263 void visit(const smt_logic_##the_id##t &) override \
264 { \
265 os << #the_name; \
266 }
267#include "smt_logics.def"
268#undef LOGIC_ID
269};
270
271std::ostream &operator<<(std::ostream &os, const smt_logict &logic)
272{
274 return os;
275}
276
277std::string smt_to_smt2_string(const smt_logict &logic)
278{
279 std::stringstream ss;
280 ss << logic;
281 return ss.str();
282}
283
286{
287protected:
288 std::ostream &os;
289
290public:
291 explicit smt_command_to_string_convertert(std::ostream &os) : os(os)
292 {
293 }
294
295 void visit(const smt_assert_commandt &assert) override
296 {
297 os << "(assert " << assert.condition() << ")";
298 }
299
300 void visit(const smt_check_sat_commandt &check_sat) override
301 {
302 os << "(check-sat)";
303 }
304
306 {
307 os << "(declare-fun " << declare_function.identifier() << " (";
308 const auto parameter_sorts = declare_function.parameter_sorts();
309 join_strings(os, parameter_sorts.begin(), parameter_sorts.end(), ' ');
310 os << ") " << declare_function.return_sort() << ")";
311 }
312
313 void visit(const smt_define_function_commandt &define_function) override
314 {
315 os << "(define-fun " << define_function.identifier() << " (";
316 const auto parameters = define_function.parameters();
318 os,
319 parameters.begin(),
320 parameters.end(),
321 " ",
322 [](const smt_identifier_termt &identifier) {
323 return "(" + smt_to_smt2_string(identifier) + " " +
324 smt_to_smt2_string(identifier.get_sort()) + ")";
325 });
326 os << ") " << define_function.return_sort() << " "
327 << define_function.definition() << ")";
328 }
329
330 void visit(const smt_exit_commandt &exit) override
331 {
332 os << "(exit)";
333 }
334
335 void visit(const smt_get_value_commandt &get_value) override
336 {
337 os << "(get-value (" << get_value.descriptor() << "))";
338 }
339
340 void visit(const smt_pop_commandt &pop) override
341 {
342 os << "(pop " << pop.levels() << ")";
343 }
344
345 void visit(const smt_push_commandt &push) override
346 {
347 os << "(push " << push.levels() << ")";
348 }
349
350 void visit(const smt_set_logic_commandt &set_logic) override
351 {
352 os << "(set-logic " << set_logic.logic() << ")";
353 }
354
355 void visit(const smt_set_option_commandt &set_option) override
356 {
357 os << "(set-option " << set_option.option() << ")";
358 }
359};
360
361std::ostream &operator<<(std::ostream &os, const smt_commandt &command)
362{
364 return os;
365}
366
367std::string smt_to_smt2_string(const smt_commandt &command)
368{
369 std::stringstream ss;
370 ss << command;
371 return ss.str();
372}
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:878
const smt_termt & condition() const
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:103
mp_integer value() const
Definition: smt_terms.cpp:98
std::size_t bit_width() const
Definition: smt_sorts.cpp:60
bool value() const
Definition: smt_terms.cpp:46
void visit(const smt_declare_function_commandt &declare_function) override
smt_command_to_string_convertert(std::ostream &os)
void visit(const smt_pop_commandt &pop) override
void visit(const smt_assert_commandt &assert) override
void visit(const smt_exit_commandt &exit) override
void visit(const smt_get_value_commandt &get_value) override
void visit(const smt_define_function_commandt &define_function) override
void visit(const smt_set_option_commandt &set_option) override
void visit(const smt_set_logic_commandt &set_logic) override
void visit(const smt_push_commandt &push) override
void visit(const smt_check_sat_commandt &check_sat) override
void accept(smt_command_const_downcast_visitort &) const
const smt_termt & definition() const
const smt_identifier_termt & identifier() const
std::vector< std::reference_wrapper< const smt_identifier_termt > > parameters() const
const smt_sortt & return_sort() const
const smt_identifier_termt & function_identifier() const
Definition: smt_terms.cpp:124
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:130
const smt_termt & descriptor() const
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
irep_idt identifier() const
Definition: smt_terms.cpp:72
smt_logic_to_string_convertert(std::ostream &os)
void accept(smt_logic_const_downcast_visitort &) const
Definition: smt_logics.cpp:34
void visit(const smt_option_produce_modelst &produce_models) override
smt_option_to_string_convertert(std::ostream &os)
void accept(smt_option_const_downcast_visitort &) const
Definition: smt_options.cpp:49
size_t levels() const
size_t levels() const
const smt_logict & logic() const
const smt_optiont & option() const
smt_sort_output_visitort(std::ostream &os)
void visit(const smt_bit_vector_sortt &bit_vec) override
void visit(const smt_bool_sortt &) override
void accept(smt_sort_const_downcast_visitort &) const
Definition: smt_sorts.cpp:76
void visit(const smt_bool_literal_termt &bool_literal) override
void push_output(outputt &&output)
Single argument version of push_outputs.
std::function< void(std::ostream &)> output_functiont
static output_functiont make_output_function(const std::string &output)
void push_outputs()
Base case for the recursive push_outputs function template below.
std::stack< output_functiont > output_stack
static std::ostream & convert(std::ostream &os, const smt_termt &term)
This function is complete the external interface to this class.
void accept(smt_term_const_downcast_visitort &) const
Definition: smt_terms.cpp:150
static auxiliary_symbolt declare_function(const irep_idt &function_name, const mathematical_function_typet &type, symbol_table_baset &symbol_table)
Declare a function with the given name and type.
Definition: java_utils.cpp:361
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
Data structure for smt sorts.
std::ostream & operator<<(std::ostream &os, const smt_sortt &sort)
std::string smt_to_smt2_string(const smt_sortt &sort)
Streaming SMT data structures to a string based output stream.
void output_function(std::ostream &os, const statement_list_parse_treet::functiont &function)
Prints the given Statement List function in a human-readable form to the given output stream.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Stream & join_strings(Stream &&os, const It b, const It e, const Delimiter &delimiter, TransformFunc &&transform_func)
Prints items to an stream, separated by a constant delimiter.
Definition: string_utils.h:62