Add smt_termt visitor

Because this will be used to implement term to string/output stream
conversion. Use of a visitor will allow this printing code to be
separated from the data structure.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_terms.cpp

@@ -141,3 +141,26 @@ smt_function_application_termt::arguments() const
     return std::cref(static_cast<const smt_termt &>(argument));
   });
 }
+
+template <typename visitort>
+void accept(const smt_termt &term, const irep_idt &id, visitort &&visitor)
+{
+#define TERM_ID(the_id)                                                        \
+  if(id == ID_smt_##the_id##_term)                                             \
+    return visitor.visit(static_cast<const smt_##the_id##_termt &>(term));
+// 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_terms.def> // NOLINT(build/include)
+#undef TERM_ID
+  UNREACHABLE;
+}
+
+void smt_termt::accept(smt_term_const_downcast_visitort &visitor) const
+{
+  ::accept(*this, id(), visitor);
+}
+
+void smt_termt::accept(smt_term_const_downcast_visitort &&visitor) const
+{
+  ::accept(*this, id(), std::move(visitor));
+}

src/solvers/smt2_incremental/smt_terms.def

@@ -4,6 +4,8 @@
 /// set of terms 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 term classes.
+///  * The member functions of the `smt_term_const_downcast_visitort` class.
+///  * The type of term checks required to implement `smt_termt::accept`.
 TERM_ID(bool_literal)
 TERM_ID(not)
 TERM_ID(identifier)

src/solvers/smt2_incremental/smt_terms.h

@@ -11,6 +11,7 @@
 class BigInt;
 using mp_integer = BigInt;
 
+class smt_term_const_downcast_visitort;
 class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
 {
 public:
@@ -25,6 +26,9 @@ class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
 
   const smt_sortt &get_sort() const;
 
+  void accept(smt_term_const_downcast_visitort &) const;
+  void accept(smt_term_const_downcast_visitort &&) const;
+
 protected:
   smt_termt(irep_idt id, smt_sortt sort);
 };
@@ -89,4 +93,12 @@ class smt_function_application_termt : public smt_termt
   std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
 };
 
+class smt_term_const_downcast_visitort
+{
+public:
+#define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
+#include "smt_terms.def"
+#undef TERM_ID
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H

unit/solvers/smt2_incremental/smt_terms.cpp

@@ -84,3 +84,120 @@ TEST_CASE("smt_termt equality.", "[core][smt2_incremental]")
   CHECK_FALSE(not_false == not_true);
   CHECK(not_false == smt_not_termt{smt_bool_literal_termt{false}});
 }
+
+template <typename expected_termt>
+class term_visit_type_checkert final : public smt_term_const_downcast_visitort
+{
+public:
+  bool expected_term_visited = false;
+  bool unexpected_term_visited = false;
+
+  void visit(const smt_bool_literal_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_bool_literal_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_not_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_not_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_identifier_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_identifier_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_bit_vector_constant_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_bit_vector_constant_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+
+  void visit(const smt_function_application_termt &) override
+  {
+    if(std::is_same<expected_termt, smt_function_application_termt>::value)
+    {
+      expected_term_visited = true;
+    }
+    else
+    {
+      unexpected_term_visited = true;
+    }
+  }
+};
+
+template <typename term_typet>
+term_typet make_test_term();
+
+template <>
+smt_bool_literal_termt make_test_term<smt_bool_literal_termt>()
+{
+  return smt_bool_literal_termt{false};
+}
+
+template <>
+smt_not_termt make_test_term<smt_not_termt>()
+{
+  return smt_not_termt{smt_bool_literal_termt{false}};
+}
+
+template <>
+smt_identifier_termt make_test_term<smt_identifier_termt>()
+{
+  return smt_identifier_termt{"foo", smt_bool_sortt{}};
+}
+
+template <>
+smt_bit_vector_constant_termt make_test_term<smt_bit_vector_constant_termt>()
+{
+  return smt_bit_vector_constant_termt{0, 32};
+}
+
+template <>
+smt_function_application_termt make_test_term<smt_function_application_termt>()
+{
+  return smt_function_application_termt{
+    smt_identifier_termt{"bar", smt_bool_sortt{}}, {}};
+}
+
+TEMPLATE_TEST_CASE(
+  "smt_termt::accept(visitor)",
+  "[core][smt2_incremental]",
+  smt_bool_literal_termt,
+  smt_not_termt,
+  smt_identifier_termt,
+  smt_bit_vector_constant_termt,
+  smt_function_application_termt)
+{
+  term_visit_type_checkert<TestType> checker;
+  make_test_term<TestType>().accept(checker);
+  CHECK(checker.expected_term_visited);
+  CHECK_FALSE(checker.unexpected_term_visited);
+}