Add conversion of SMT_sortt into strings

So that they can be sent to an SMT2 solver using a string based
interface.

Author: thomasspriggs

src/solvers/Makefile

@@ -193,6 +193,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2_tokenizer.cpp \
       smt2/smt2irep.cpp \
       smt2_incremental/smt_sorts.cpp \
+      smt2_incremental/smt_to_string.cpp \
       smt2_incremental/smt2_incremental_decision_procedure.cpp \
       # Empty last line
 

src/solvers/smt2_incremental/smt_to_string.cpp

@@ -0,0 +1,43 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_to_string.h>
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
+{
+protected:
+  std::ostream &os;
+
+public:
+  explicit smt_sort_output_visitort(std::ostream &os) : os(os)
+  {
+  }
+
+  void visit(const smt_bool_sortt &) override
+  {
+    os << "Bool";
+  }
+
+  void visit(const smt_bit_vector_sortt &bit_vec) override
+  {
+    os << "(_ BitVec " << bit_vec.bit_width() << ")";
+  }
+};
+
+std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
+{
+  sort.accept(smt_sort_output_visitort{os});
+  return os;
+}
+
+std::string smt_to_string(const smt_sortt &sort)
+{
+  std::stringstream ss;
+  ss << sort;
+  return ss.str();
+}

src/solvers/smt2_incremental/smt_to_string.h

@@ -0,0 +1,18 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Streaming SMT data structures to a string based output stream.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H
+
+class smt_sortt;
+
+#include <iosfwd>
+#include <string>
+
+std::ostream &operator<<(std::ostream &os, const smt_sortt &sort);
+
+std::string smt_to_string(const smt_sortt &sort);
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_STRING_H

unit/Makefile

@@ -77,6 +77,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/sat/satcheck_cadical.cpp \
        solvers/sat/satcheck_minisat2.cpp \
        solvers/smt2_incremental/smt_sorts.cpp \
+       solvers/smt2_incremental/smt_to_string.cpp \
        solvers/strings/array_pool/array_pool.cpp \
        solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \

unit/solvers/smt2_incremental/smt_to_string.cpp

@@ -0,0 +1,12 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_sorts.h>
+#include <solvers/smt2_incremental/smt_to_string.h>
+
+TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
+{
+  CHECK(smt_to_string(smt_bool_sortt{}) == "Bool");
+  CHECK(smt_to_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
+}