CBMC
smt_to_smt2_string.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #include <util/range.h>
4 #include <util/string_utils.h>
5 
13 
14 #include <functional>
15 #include <sstream> // IWYU pragma: keep
16 #include <stack>
17 #include <string>
18 
19 static std::string escape_identifier(const irep_idt &identifier)
20 {
21  return smt2_convt::convert_identifier(identifier);
22 }
23 
25 {
26 protected:
27  std::ostream &os;
28 
29 public:
30  explicit smt_index_output_visitort(std::ostream &os) : os(os)
31  {
32  }
33 
34  void visit(const smt_numeral_indext &numeral) override
35  {
36  os << numeral.value();
37  }
38 
39  void visit(const smt_symbol_indext &symbol) override
40  {
41  os << escape_identifier(symbol.identifier());
42  }
43 };
44 
45 std::ostream &operator<<(std::ostream &os, const smt_indext &index)
46 {
47  smt_index_output_visitort visitor{os};
48  index.accept(visitor);
49  return os;
50 }
51 
52 std::string smt_to_smt2_string(const smt_indext &index)
53 {
54  std::stringstream ss;
55  ss << index;
56  return ss.str();
57 }
58 
60 {
61 protected:
62  std::ostream &os;
63 
64 public:
65  explicit smt_sort_output_visitort(std::ostream &os) : os(os)
66  {
67  }
68 
69  void visit(const smt_bool_sortt &) override
70  {
71  os << "Bool";
72  }
73 
74  void visit(const smt_bit_vector_sortt &bit_vec) override
75  {
76  os << "(_ BitVec " << bit_vec.bit_width() << ")";
77  }
78 
79  void visit(const smt_array_sortt &array) override
80  {
81  os << "(Array " << array.index_sort() << " " << array.element_sort() << ")";
82  }
83 };
84 
85 std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
86 {
88  return os;
89 }
90 
91 std::string smt_to_smt2_string(const smt_sortt &sort)
92 {
93  std::stringstream ss;
94  ss << sort;
95  return ss.str();
96 }
97 
98 struct sorted_variablest final
99 {
100  std::vector<std::reference_wrapper<const smt_identifier_termt>> identifiers;
101 };
102 
119 {
120 private:
121  using output_functiont = std::function<void(std::ostream &)>;
122  std::stack<output_functiont> output_stack;
123 
124  static output_functiont make_output_function(const std::string &output);
125  static output_functiont make_output_function(const smt_indext &output);
126  static output_functiont make_output_function(const smt_sortt &output);
128  template <typename elementt>
130  const std::vector<std::reference_wrapper<const elementt>> &output);
132 
134  template <typename outputt>
135  void push_output(outputt &&output);
136 
138  void push_outputs();
139 
151  template <typename outputt, typename... outputst>
152  void push_outputs(outputt &&output, outputst &&... outputs);
153 
155 
156  void visit(const smt_bool_literal_termt &bool_literal) override;
157  void visit(const smt_identifier_termt &identifier_term) override;
158  void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override;
159  void
160  visit(const smt_function_application_termt &function_application) override;
161  void visit(const smt_forall_termt &forall) override;
162  void visit(const smt_exists_termt &exists) override;
163 
164 public:
168  static std::ostream &convert(std::ostream &os, const smt_termt &term);
169 };
170 
173 {
174  // `output` must be captured by value to avoid dangling references.
175  return [output](std::ostream &os) { os << output; };
176 }
177 
180 {
181  return [=](std::ostream &os) { os << output; };
182 }
183 
186 {
187  return [=](std::ostream &os) { os << output; };
188 }
189 
192 {
193  return [=](std::ostream &os) { output.accept(*this); };
194 }
195 
196 template <typename elementt>
199  const std::vector<std::reference_wrapper<const elementt>> &outputs)
200 {
201  return [=](std::ostream &os) {
202  for(const auto &output : make_range(outputs.rbegin(), outputs.rend()))
203  {
204  push_outputs(" ", output.get());
205  }
206  };
207 }
208 
211  const sorted_variablest &output)
212 {
213  return [=](std::ostream &os) {
214  const auto push_sorted_variable =
215  [&](const smt_identifier_termt &identifier) {
216  push_outputs("(", identifier, " ", identifier.get_sort(), ")");
217  };
218  for(const auto &bound_variable :
219  make_range(output.identifiers.rbegin(), --output.identifiers.rend()))
220  {
221  push_sorted_variable(bound_variable);
222  push_output(" ");
223  }
224  push_sorted_variable(output.identifiers.front());
225  };
226 }
227 
228 template <typename outputt>
230 {
231  output_stack.push(make_output_function(std::forward<outputt>(output)));
232 }
233 
235 {
236 }
237 
238 template <typename outputt, typename... outputst>
240  outputt &&output,
241  outputst &&... outputs)
242 {
243  push_outputs(std::forward<outputst>(outputs)...);
244  push_output(std::forward<outputt>(output));
245 }
246 
248  const smt_bool_literal_termt &bool_literal)
249 {
250  push_output(bool_literal.value() ? "true" : "false");
251 }
252 
254  const smt_identifier_termt &identifier_term)
255 {
256  auto indices = identifier_term.indices();
257  auto escaped_identifier = escape_identifier(identifier_term.identifier());
258  if(indices.empty())
259  {
260  push_outputs(std::move(escaped_identifier));
261  }
262  else
263  {
264  push_outputs("(_ ", std::move(escaped_identifier), std::move(indices), ")");
265  }
266 }
267 
269  const smt_bit_vector_constant_termt &bit_vector_constant)
270 {
271  auto value = integer2string(bit_vector_constant.value());
272  auto bit_width = std::to_string(bit_vector_constant.get_sort().bit_width());
273  push_outputs("(_ bv", std::move(value), " ", std::move(bit_width), ")");
274 }
275 
277  const smt_function_application_termt &function_application)
278 {
279  const auto &id = function_application.function_identifier();
280  auto arguments = function_application.arguments();
281  push_outputs("(", id, std::move(arguments), ")");
282 }
283 
285 {
286  sorted_variablest bound_variables{forall.bound_variables()};
287  auto predicate = forall.predicate();
288  push_outputs("(forall (", bound_variables, ") ", std::move(predicate), ")");
289 }
290 
292 {
293  sorted_variablest bound_variables{exists.bound_variables()};
294  auto predicate = exists.predicate();
295  push_outputs("(exists (", bound_variables, ") ", std::move(predicate), ")");
296 }
297 
298 std::ostream &
299 smt_term_to_string_convertert::convert(std::ostream &os, const smt_termt &term)
300 {
302  term.accept(converter);
303  while(!converter.output_stack.empty())
304  {
305  auto output_function = std::move(converter.output_stack.top());
306  converter.output_stack.pop();
307  output_function(os);
308  }
309  return os;
310 }
311 
312 std::ostream &operator<<(std::ostream &os, const smt_termt &term)
313 {
315 }
316 
317 std::string smt_to_smt2_string(const smt_termt &term)
318 {
319  std::stringstream ss;
320  ss << term;
321  return ss.str();
322 }
323 
326 {
327 protected:
328  std::ostream &os;
329 
330 public:
331  explicit smt_option_to_string_convertert(std::ostream &os) : os(os)
332  {
333  }
334 
335  void visit(const smt_option_produce_modelst &produce_models) override
336  {
337  os << ":produce-models " << (produce_models.setting() ? "true" : "false");
338  }
339 };
340 
341 std::ostream &operator<<(std::ostream &os, const smt_optiont &option)
342 {
344  return os;
345 }
346 
347 std::string smt_to_smt2_string(const smt_optiont &option)
348 {
349  std::stringstream ss;
350  ss << option;
351  return ss.str();
352 }
353 
355 {
356 protected:
357  std::ostream &os;
358 
359 public:
360  explicit smt_logic_to_string_convertert(std::ostream &os) : os(os)
361  {
362  }
363 
364 #define LOGIC_ID(the_id, the_name) \
365  void visit(const smt_logic_##the_id##t &) override \
366  { \
367  os << #the_name; \
368  }
369 #include "solvers/smt2_incremental/ast/smt_logics.def"
370 
371 #undef LOGIC_ID
372 };
373 
374 std::ostream &operator<<(std::ostream &os, const smt_logict &logic)
375 {
377  return os;
378 }
379 
380 std::string smt_to_smt2_string(const smt_logict &logic)
381 {
382  std::stringstream ss;
383  ss << logic;
384  return ss.str();
385 }
386 
389 {
390 protected:
391  std::ostream &os;
392 
393 public:
394  explicit smt_command_to_string_convertert(std::ostream &os) : os(os)
395  {
396  }
397 
398  void visit(const smt_assert_commandt &assert) override
399  {
400  os << "(assert " << assert.condition() << ")";
401  }
402 
403  void visit(const smt_check_sat_commandt &check_sat) override
404  {
405  os << "(check-sat)";
406  }
407 
409  {
410  os << "(declare-fun " << declare_function.identifier() << " (";
411  const auto parameter_sorts = declare_function.parameter_sorts();
412  join_strings(os, parameter_sorts.begin(), parameter_sorts.end(), ' ');
413  os << ") " << declare_function.return_sort() << ")";
414  }
415 
416  void visit(const smt_define_function_commandt &define_function) override
417  {
418  os << "(define-fun " << define_function.identifier() << " (";
419  const auto parameters = define_function.parameters();
420  join_strings(
421  os,
422  parameters.begin(),
423  parameters.end(),
424  " ",
425  [](const smt_identifier_termt &identifier) {
426  return "(" + smt_to_smt2_string(identifier) + " " +
427  smt_to_smt2_string(identifier.get_sort()) + ")";
428  });
429  os << ") " << define_function.return_sort() << " "
430  << define_function.definition() << ")";
431  }
432 
433  void visit(const smt_exit_commandt &exit) override
434  {
435  os << "(exit)";
436  }
437 
438  void visit(const smt_get_value_commandt &get_value) override
439  {
440  os << "(get-value (" << get_value.descriptor() << "))";
441  }
442 
443  void visit(const smt_pop_commandt &pop) override
444  {
445  os << "(pop " << pop.levels() << ")";
446  }
447 
448  void visit(const smt_push_commandt &push) override
449  {
450  os << "(push " << push.levels() << ")";
451  }
452 
453  void visit(const smt_set_logic_commandt &set_logic) override
454  {
455  os << "(set-logic " << set_logic.logic() << ")";
456  }
457 
458  void visit(const smt_set_option_commandt &set_option) override
459  {
460  os << "(set-option " << set_option.option() << ")";
461  }
462 };
463 
464 std::ostream &operator<<(std::ostream &os, const smt_commandt &command)
465 {
467  return os;
468 }
469 
470 std::string smt_to_smt2_string(const smt_commandt &command)
471 {
472  std::stringstream ss;
473  ss << command;
474  return ss.str();
475 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:1020
const smt_sortt & element_sort() const
Definition: smt_sorts.cpp:81
const smt_sortt & index_sort() const
Definition: smt_sorts.cpp:76
const smt_termt & condition() const
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:121
mp_integer value() const
Definition: smt_terms.cpp:116
std::size_t bit_width() const
Definition: smt_sorts.cpp:62
bool value() const
Definition: smt_terms.cpp:47
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_termt & predicate() const
Definition: smt_terms.cpp:176
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
Definition: smt_terms.cpp:182
const smt_identifier_termt & function_identifier() const
Definition: smt_terms.cpp:142
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:148
const smt_termt & descriptor() const
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:93
irep_idt identifier() const
Definition: smt_terms.cpp:81
std::vector< std::reference_wrapper< const smt_indext > > indices() const
Definition: smt_terms.cpp:87
void visit(const smt_numeral_indext &numeral) override
void visit(const smt_symbol_indext &symbol) override
smt_index_output_visitort(std::ostream &os)
For implementation of indexed identifiers.
Definition: smt_index.h:14
void accept(smt_index_const_downcast_visitort &) const
Definition: smt_index.cpp:35
smt_logic_to_string_convertert(std::ostream &os)
void accept(smt_logic_const_downcast_visitort &) const
Definition: smt_logics.cpp:35
std::size_t value() const
Definition: smt_index.cpp:50
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:50
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_array_sortt &array) override
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:97
irep_idt identifier() const
Definition: smt_index.cpp:62
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:236
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:358
mini_bddt exists(const mini_bddt &u, const unsigned var)
Definition: miniBDD.cpp:556
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:522
Data structure for smt sorts.
std::string smt_to_smt2_string(const smt_indext &index)
std::ostream & operator<<(std::ostream &os, const smt_indext &index)
static std::string escape_identifier(const irep_idt &identifier)
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.
void exit(int status)
Definition: stdlib.c:102
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:61
std::vector< std::reference_wrapper< const smt_identifier_termt > > identifiers