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 {
22 protected:
23  std::ostream &os;
24 
25 public:
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 
41 std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
42 {
44  return os;
45 }
46 
47 std::string smt_to_smt2_string(const smt_sortt &sort)
48 {
49  std::stringstream ss;
50  ss << sort;
51  return ss.str();
52 }
53 
70 {
71 private:
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);
76  static output_functiont make_output_function(const smt_sortt &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 
110 public:
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 
148 template <typename outputt>
150 {
151  output_stack.push(make_output_function(std::forward<outputt>(output)));
152 }
153 
155 {
156 }
157 
158 template <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 {
176  push_outputs(
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 
196 std::ostream &
197 smt_term_to_string_convertert::convert(std::ostream &os, const smt_termt &term)
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 
210 std::ostream &operator<<(std::ostream &os, const smt_termt &term)
211 {
213 }
214 
215 std::string smt_to_smt2_string(const smt_termt &term)
216 {
217  std::stringstream ss;
218  ss << term;
219  return ss.str();
220 }
221 
224 {
225 protected:
226  std::ostream &os;
227 
228 public:
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 
239 std::ostream &operator<<(std::ostream &os, const smt_optiont &option)
240 {
242  return os;
243 }
244 
245 std::string smt_to_smt2_string(const smt_optiont &option)
246 {
247  std::stringstream ss;
248  ss << option;
249  return ss.str();
250 }
251 
253 {
254 protected:
255  std::ostream &os;
256 
257 public:
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 
271 std::ostream &operator<<(std::ostream &os, const smt_logict &logic)
272 {
274  return os;
275 }
276 
277 std::string smt_to_smt2_string(const smt_logict &logic)
278 {
279  std::stringstream ss;
280  ss << logic;
281  return ss.str();
282 }
283 
286 {
287 protected:
288  std::ostream &os;
289 
290 public:
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();
317  join_strings(
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 
361 std::ostream &operator<<(std::ostream &os, const smt_commandt &command)
362 {
364  return os;
365 }
366 
367 std::string smt_to_smt2_string(const smt_commandt &command)
368 {
369  std::stringstream ss;
370  ss << command;
371  return ss.str();
372 }
smt_command_to_string_convertert::visit
void visit(const smt_define_function_commandt &define_function) override
Definition: smt_to_smt2_string.cpp:313
smt_command_to_string_convertert::visit
void visit(const smt_exit_commandt &exit) override
Definition: smt_to_smt2_string.cpp:330
smt_option_produce_modelst
Definition: smt_options.h:65
smt_push_commandt
Definition: smt_commands.h:95
smt_set_logic_commandt
Definition: smt_commands.h:111
smt2_conv.h
smt_define_function_commandt::return_sort
const smt_sortt & return_sort() const
Definition: smt_commands.cpp:114
operator<<
std::ostream & operator<<(std::ostream &os, const smt_sortt &sort)
Definition: smt_to_smt2_string.cpp:41
smt_function_application_termt::function_identifier
const smt_identifier_termt & function_identifier() const
Definition: smt_terms.cpp:118
smt_identifier_termt
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
smt_pop_commandt::levels
size_t levels() const
Definition: smt_commands.cpp:152
smt_option_to_string_convertert
Definition: smt_to_smt2_string.cpp:224
string_utils.h
smt_define_function_commandt::definition
const smt_termt & definition() const
Definition: smt_commands.cpp:119
smt_logic_const_downcast_visitort
Definition: smt_logics.h:75
smt_termt
Definition: smt_terms.h:16
smt_set_option_commandt
Definition: smt_commands.h:120
smt_command_to_string_convertert::visit
void visit(const smt_pop_commandt &pop) override
Definition: smt_to_smt2_string.cpp:340
smt_bit_vector_sortt
Definition: smt_sorts.h:84
smt_term_to_string_convertert::make_output_function
static output_functiont make_output_function(const std::string &output)
Definition: smt_to_smt2_string.cpp:118
smt_sort_output_visitort::os
std::ostream & os
Definition: smt_to_smt2_string.cpp:23
smt_define_function_commandt
Definition: smt_commands.h:67
smt_get_value_commandt::descriptor
const smt_termt & descriptor() const
Definition: smt_commands.cpp:130
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
smt_define_function_commandt::parameters
std::vector< std::reference_wrapper< const smt_identifier_termt > > parameters() const
Definition: smt_commands.cpp:106
smt_bit_vector_constant_termt::value
mp_integer value() const
Definition: smt_terms.cpp:92
smt_commandt::accept
void accept(smt_command_const_downcast_visitort &) const
Definition: smt_commands.cpp:192
smt_term_to_string_convertert::output_functiont
std::function< void(std::ostream &)> output_functiont
Definition: smt_to_smt2_string.cpp:72
smt_set_option_commandt::option
const smt_optiont & option() const
Definition: smt_commands.cpp:174
smt_logic_to_string_convertert::smt_logic_to_string_convertert
smt_logic_to_string_convertert(std::ostream &os)
Definition: smt_to_smt2_string.cpp:258
smt_term_to_string_convertert::push_output
void push_output(outputt &&output)
Single argument version of push_outputs.
Definition: smt_to_smt2_string.cpp:149
smt_bool_literal_termt::value
bool value() const
Definition: smt_terms.cpp:46
smt_bit_vector_sortt::bit_width
std::size_t bit_width() const
Definition: smt_sorts.cpp:60
smt_command_to_string_convertert::visit
void visit(const smt_set_logic_commandt &set_logic) override
Definition: smt_to_smt2_string.cpp:350
smt_define_function_commandt::identifier
const smt_identifier_termt & identifier() const
Definition: smt_commands.cpp:99
smt_sortt::accept
void accept(smt_sort_const_downcast_visitort &) const
Definition: smt_sorts.cpp:76
smt_sorts.h
Data structure for smt sorts.
smt_exit_commandt
Definition: smt_commands.h:81
smt2_convt::convert_identifier
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:876
smt_option_to_string_convertert::smt_option_to_string_convertert
smt_option_to_string_convertert(std::ostream &os)
Definition: smt_to_smt2_string.cpp:229
smt_option_produce_modelst::setting
bool setting() const
Definition: smt_options.cpp:31
smt_declare_function_commandt
Definition: smt_commands.h:50
smt_sort_output_visitort::smt_sort_output_visitort
smt_sort_output_visitort(std::ostream &os)
Definition: smt_to_smt2_string.cpp:26
smt_termt::accept
void accept(smt_term_const_downcast_visitort &) const
Definition: smt_terms.cpp:144
smt_command_const_downcast_visitort
Definition: smt_commands.h:127
smt_logict::accept
void accept(smt_logic_const_downcast_visitort &) const
Definition: smt_logics.cpp:34
smt_check_sat_commandt
Definition: smt_commands.h:41
smt_pop_commandt
Definition: smt_commands.h:102
smt_term_to_string_convertert
Definition: smt_to_smt2_string.cpp:70
join_strings
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
smt_sortt
Definition: smt_sorts.h:18
smt_bool_sortt
Definition: smt_sorts.h:78
smt_sort_const_downcast_visitort
Definition: smt_sorts.h:91
smt_optiont::accept
void accept(smt_option_const_downcast_visitort &) const
Definition: smt_options.cpp:49
smt_assert_commandt::condition
const smt_termt & condition() const
Definition: smt_commands.cpp:32
smt_logic_to_string_convertert::os
std::ostream & os
Definition: smt_to_smt2_string.cpp:255
smt_identifier_termt::identifier
irep_idt identifier() const
Definition: smt_terms.cpp:66
smt_command_to_string_convertert::visit
void visit(const smt_get_value_commandt &get_value) override
Definition: smt_to_smt2_string.cpp:335
smt_option_to_string_convertert::os
std::ostream & os
Definition: smt_to_smt2_string.cpp:226
smt_commandt
Definition: smt_commands.h:14
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
smt_command_to_string_convertert::visit
void visit(const smt_set_option_commandt &set_option) override
Definition: smt_to_smt2_string.cpp:355
smt_term_to_string_convertert::visit
void visit(const smt_bool_literal_termt &bool_literal) override
Definition: smt_to_smt2_string.cpp:167
smt_sort_output_visitort::visit
void visit(const smt_bit_vector_sortt &bit_vec) override
Definition: smt_to_smt2_string.cpp:35
smt_logic_to_string_convertert
Definition: smt_to_smt2_string.cpp:253
declare_function
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
smt_command_to_string_convertert::visit
void visit(const smt_declare_function_commandt &declare_function) override
Definition: smt_to_smt2_string.cpp:305
smt_term_to_string_convertert::smt_term_to_string_convertert
smt_term_to_string_convertert()=default
smt_term_to_string_convertert::convert
static std::ostream & convert(std::ostream &os, const smt_termt &term)
This function is complete the external interface to this class.
Definition: smt_to_smt2_string.cpp:197
smt_command_to_string_convertert::visit
void visit(const smt_push_commandt &push) override
Definition: smt_to_smt2_string.cpp:345
smt_function_application_termt
Definition: smt_terms.h:115
smt_commands.h
smt_logics.h
smt_get_value_commandt
Definition: smt_commands.h:88
smt_option_const_downcast_visitort
Definition: smt_options.h:72
smt_to_smt2_string
std::string smt_to_smt2_string(const smt_sortt &sort)
Definition: smt_to_smt2_string.cpp:47
smt_command_to_string_convertert::os
std::ostream & os
Definition: smt_to_smt2_string.cpp:288
smt_command_to_string_convertert::smt_command_to_string_convertert
smt_command_to_string_convertert(std::ostream &os)
Definition: smt_to_smt2_string.cpp:291
smt_assert_commandt
Definition: smt_commands.h:34
smt_bit_vector_constant_termt::get_sort
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:97
smt_bool_literal_termt
Definition: smt_terms.h:72
smt_option_to_string_convertert::visit
void visit(const smt_option_produce_modelst &produce_models) override
Definition: smt_to_smt2_string.cpp:233
smt_term_to_string_convertert::push_outputs
void push_outputs()
Base case for the recursive push_outputs function template below.
Definition: smt_to_smt2_string.cpp:154
smt_command_to_string_convertert::visit
void visit(const smt_check_sat_commandt &check_sat) override
Definition: smt_to_smt2_string.cpp:300
smt_logict
Definition: smt_logics.h:11
smt_command_to_string_convertert
Definition: smt_to_smt2_string.cpp:286
smt_term_to_string_convertert::output_stack
std::stack< output_functiont > output_stack
Definition: smt_to_smt2_string.cpp:73
smt_function_application_termt::arguments
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:124
smt_sort_output_visitort::visit
void visit(const smt_bool_sortt &) override
Definition: smt_to_smt2_string.cpp:30
output_function
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.
Definition: statement_list_parse_tree_io.cpp:94
smt_term_const_downcast_visitort
Definition: smt_terms.h:155
smt_bit_vector_constant_termt
Definition: smt_terms.h:99
smt_set_logic_commandt::logic
const smt_logict & logic() const
Definition: smt_commands.cpp:163
smt_to_smt2_string.h
Streaming SMT data structures to a string based output stream.
smt_push_commandt::levels
size_t levels() const
Definition: smt_commands.cpp:141
smt_command_to_string_convertert::visit
void visit(const smt_assert_commandt &assert) override
Definition: smt_to_smt2_string.cpp:295
smt_terms.h
smt_sort_output_visitort
Definition: smt_to_smt2_string.cpp:21
smt_optiont
Definition: smt_options.h:11
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103