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 }
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:876
const smt_termt & condition() const
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:97
mp_integer value() const
Definition: smt_terms.cpp:92
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:118
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:124
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:66
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:144
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