Add smt_command downcast visitor

Author: thomasspriggs

src/solvers/smt2_incremental/smt_commands.cpp

@@ -143,3 +143,26 @@ size_t smt_pop_commandt::levels() const
 {
   return get_size_t(ID_value);
 }
+
+template <typename visitort>
+void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
+{
+#define COMMAND_ID(the_id)                                                     \
+  if(id == ID_smt_##the_id##_command)                                          \
+    return visitor.visit(static_cast<const smt_##the_id##_commandt &>(command));
+// The include below is marked as nolint because including the same file
+// multiple times is required as part of the x macro pattern.
+#include <solvers/smt2_incremental/smt_commands.def> // NOLINT(build/include)
+#undef COMMAND_ID
+  UNREACHABLE;
+}
+
+void smt_commandt::accept(smt_command_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_commandt::accept(smt_command_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}

src/solvers/smt2_incremental/smt_commands.def

@@ -4,6 +4,8 @@
 /// set of commands which are implemented and it is used to automate repetitive
 /// parts of the implementation. These include -
 ///  * The constant `irep_idt`s used to identify each of the command classes.
+///  * The member functions of the `smt_command_const_downcast_visitort` class.
+///  * The type of command checks required to implement `smt_commandt::accept`.
 COMMAND_ID(assert)
 COMMAND_ID(check_sat)
 COMMAND_ID(declare_function)

src/solvers/smt2_incremental/smt_commands.h

@@ -6,6 +6,8 @@
 #include <solvers/smt2_incremental/smt_terms.h>
 #include <util/irep.h>
 
+class smt_command_const_downcast_visitort;
+
 class smt_commandt : protected irept
 {
 public:
@@ -18,6 +20,9 @@ class smt_commandt : protected irept
   bool operator==(const smt_commandt &) const;
   bool operator!=(const smt_commandt &) const;
 
+  void accept(smt_command_const_downcast_visitort &) const;
+  void accept(smt_command_const_downcast_visitort &&) const;
+
 protected:
   using irept::irept;
 };
@@ -103,4 +108,13 @@ class smt_set_option_commandt : public smt_commandt
 public:
 };
 
+class smt_command_const_downcast_visitort
+{
+public:
+#define COMMAND_ID(the_id)                                                     \
+  virtual void visit(const smt_##the_id##_commandt &) = 0;
+#include "smt_commands.def"
+#undef COMMAND_ID
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H