Term visitor test

Author: thomasspriggs

unit/solvers/smt2_incremental/smt_terms.cpp

@@ -6,6 +6,8 @@
 
 #include <util/mp_arith.h>
 
+#include <type_traits>
+
 TEST_CASE("smt_bool_literal_termt upcasts.", "[core][smt2_incremental]")
 {
   smt_termt term{smt_bool_literal_termt{true}};
@@ -100,3 +102,119 @@ 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_value();
+
+template <>
+smt_bool_literal_termt make_test_value<smt_bool_literal_termt>()
+{
+  return smt_bool_literal_termt{false};
+}
+
+template <>
+smt_not_termt make_test_value<smt_not_termt>()
+{
+  return smt_not_termt{smt_bool_literal_termt{false}};
+}
+
+template <>
+smt_identifier_termt make_test_value<smt_identifier_termt>()
+{
+  return smt_identifier_termt{"foo", smt_bool_sortt{}};
+}
+
+template <>
+smt_bit_vector_constant_termt make_test_value<smt_bit_vector_constant_termt>()
+{
+  return smt_bit_vector_constant_termt{0, 32};
+}
+
+template <>
+smt_function_application_termt make_test_value<smt_function_application_termt>()
+{
+  return smt_function_application_termt{smt_bool_sortt{}, "bar", {}};
+}
+
+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_value<TestType>().accept(checker);
+  CHECK(checker.expected_term_visited);
+  CHECK_FALSE(checker.unexpected_term_visited);
+}