Use smt_logics.def to define printed strings

So that additional logics can be added based solely on updating the
`.def` file.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_logics.cpp

@@ -3,7 +3,7 @@
 #include <solvers/smt2_incremental/smt_logics.h>
 
 // Define the irep_idts for logics.
-#define LOGIC_ID(the_id)                                                       \
+#define LOGIC_ID(the_id, the_name)                                             \
   const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
 #include <solvers/smt2_incremental/smt_logics.def>
 #undef LOGIC_ID
@@ -21,7 +21,7 @@ bool smt_logict::operator!=(const smt_logict &other) const
 template <typename visitort>
 void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
 {
-#define LOGIC_ID(the_id)                                                       \
+#define LOGIC_ID(the_id, the_name)                                             \
   if(id == ID_smt_logic_##the_id)                                              \
     return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
 // The include below is marked as nolint because including the same file
@@ -41,7 +41,7 @@ void smt_logict::accept(smt_logic_const_downcast_visitort &&visitor) const
   ::accept(*this, id(), std::move(visitor));
 }
 
-#define LOGIC_ID(the_id)                                                       \
+#define LOGIC_ID(the_id, the_name)                                             \
   smt_logic_##the_id##t::smt_logic_##the_id##t()                               \
     : smt_logict{ID_smt_logic_##the_id}                                        \
   {                                                                            \

src/solvers/smt2_incremental/smt_logics.def

@@ -6,4 +6,4 @@
 ///  * The constant `irep_idt`s used to identify each of the logic classes.
 ///  * The member functions of the `smt_logic_const_downcast_visitort` class.
 ///  * The type of option checks required to implement `smt_logict::accept`.
-LOGIC_ID(quantifier_free_bit_vectors)
+LOGIC_ID(quantifier_free_bit_vectors, QF_BV)

src/solvers/smt2_incremental/smt_logics.h

@@ -61,7 +61,7 @@ const smt_logict &smt_logict::storert<derivedt>::downcast(const irept &irep)
   return static_cast<const smt_logict &>(irep);
 }
 
-#define LOGIC_ID(the_id)                                                       \
+#define LOGIC_ID(the_id, the_name)                                             \
   /* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */  \
   class smt_logic_##the_id##t : public smt_logict                              \
   {                                                                            \
@@ -74,7 +74,8 @@ const smt_logict &smt_logict::storert<derivedt>::downcast(const irept &irep)
 class smt_logic_const_downcast_visitort
 {
 public:
-#define LOGIC_ID(the_id) virtual void visit(const smt_logic_##the_id##t &) = 0;
+#define LOGIC_ID(the_id, the_name)                                             \
+  virtual void visit(const smt_logic_##the_id##t &) = 0;
 #include "smt_logics.def"
 #undef LOGIC_ID
 };

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -265,10 +265,13 @@ class smt_logic_to_string_convertert : public smt_logic_const_downcast_visitort
   {
   }
 
-  void visit(const smt_logic_quantifier_free_bit_vectorst &) override
-  {
-    os << "QF_BV";
+#define LOGIC_ID(the_id, the_name)                                             \
+  void visit(const smt_logic_##the_id##t &) override                           \
+  {                                                                            \
+    os << #the_name;                                                           \
   }
+#include "smt_logics.def"
+#undef LOGIC_ID
 };
 
 std::ostream &operator<<(std::ostream &os, const smt_logict &logic)