Refactor smt_not_term into core theory

For consistency with how the functions for the bit vector theory are
defined. Note that the factory is called `make_not` rather than `not`,
because not is a keyword in C++ which is equivalent to the `!` operator.

Author: thomasspriggs

src/solvers/Makefile

@@ -194,6 +194,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2irep.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
+      smt2_incremental/smt_core_theory.cpp \
       smt2_incremental/smt_logics.cpp \
       smt2_incremental/smt_options.cpp \
       smt2_incremental/smt_sorts.cpp \

src/solvers/smt2_incremental/smt_core_theory.cpp

@@ -0,0 +1,23 @@
+// Author: Diffblue Ltd.
+
+#include <solvers/smt2_incremental/smt_core_theory.h>
+
+const char *smt_core_theoryt::nott::identifier()
+{
+  return "not";
+}
+
+smt_sortt smt_core_theoryt::nott::return_sort(const smt_termt &operand)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_core_theoryt::nott::validate(const smt_termt &operand)
+{
+  INVARIANT(
+    operand.get_sort() == smt_bool_sortt{},
+    "\"not\" may only be applied to terms which have bool sort.");
+}
+
+const smt_function_application_termt::factoryt<smt_core_theoryt::nott>
+  smt_core_theoryt::make_not{};

src/solvers/smt2_incremental/smt_core_theory.h

@@ -0,0 +1,20 @@
+// Author: Diffblue Ltd.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H
+
+#include <solvers/smt2_incremental/smt_terms.h>
+
+class smt_core_theoryt
+{
+public:
+  struct nott final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &operand);
+    static void validate(const smt_termt &operand);
+  };
+  static const smt_function_application_termt::factoryt<nott> make_not;
+};
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H

src/solvers/smt2_incremental/smt_terms.cpp

@@ -48,20 +48,6 @@ bool smt_bool_literal_termt::value() const
   return get_bool(ID_value);
 }
 
-smt_not_termt::smt_not_termt(smt_termt operand)
-  : smt_termt{ID_smt_not_term, smt_bool_sortt{}}
-{
-  INVARIANT(
-    operand.get_sort() == smt_bool_sortt{},
-    "smt_not_termt may only be applied to terms which have bool sort.");
-  get_sub().push_back(std::move(operand));
-}
-
-const smt_termt &smt_not_termt::operand() const
-{
-  return static_cast<const smt_termt &>(get_sub().at(0));
-}
-
 static bool is_valid_smt_identifier(irep_idt identifier)
 {
   static const std::regex valid{R"(^[^\|\\]*$)"};

src/solvers/smt2_incremental/smt_terms.def

@@ -7,7 +7,6 @@
 ///  * 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)
 TERM_ID(bit_vector_constant)
 TERM_ID(function_application)

src/solvers/smt2_incremental/smt_terms.h

@@ -75,13 +75,6 @@ class smt_bool_literal_termt : public smt_termt
   bool value() const;
 };
 
-class smt_not_termt : public smt_termt
-{
-public:
-  explicit smt_not_termt(smt_termt operand);
-  const smt_termt &operand() const;
-};
-
 /// Stores identifiers in unescaped and unquoted form. Any escaping or quoting
 /// required should be performed during printing.
 class smt_identifier_termt : public smt_termt

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -102,7 +102,6 @@ class smt_term_to_string_convertert : private smt_term_const_downcast_visitort
   smt_term_to_string_convertert() = default;
 
   void visit(const smt_bool_literal_termt &bool_literal) override;
-  void visit(const smt_not_termt &not_term) override;
   void visit(const smt_identifier_termt &identifier_term) override;
   void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override;
   void
@@ -171,11 +170,6 @@ void smt_term_to_string_convertert::visit(
   push_output(bool_literal.value() ? "true" : "false");
 }
 
-void smt_term_to_string_convertert::visit(const smt_not_termt &not_term)
-{
-  push_outputs("(not ", not_term.operand(), ")");
-}
-
 void smt_term_to_string_convertert::visit(
   const smt_identifier_termt &identifier_term)
 {

unit/Makefile

@@ -87,6 +87,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2/smt2_conv.cpp \
        solvers/smt2_incremental/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/smt_commands.cpp \
+       solvers/smt2_incremental/smt_core_theory.cpp \
        solvers/smt2_incremental/smt_sorts.cpp \
        solvers/smt2_incremental/smt_terms.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \

unit/solvers/smt2_incremental/smt_commands.cpp

@@ -3,6 +3,7 @@
 #include <testing-utils/use_catch.h>
 
 #include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
 
 TEST_CASE("Test smt_commandt.pretty is accessible.", "[core][smt2_incremental]")
 {
@@ -32,11 +33,13 @@ TEST_CASE("smt_declare_function_commandt getters", "[core][smt2_incremental]")
 
 TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]")
 {
+  const auto not_x =
+    smt_core_theoryt::make_not(smt_identifier_termt{"x", smt_bool_sortt{}});
   const smt_define_function_commandt function_definition{
     "not first",
     {smt_identifier_termt{"x", smt_bool_sortt{}},
      smt_identifier_termt{"y", smt_bool_sortt{}}},
-    smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}}};
+    not_x};
   CHECK(
     function_definition.identifier() ==
     smt_identifier_termt{"not first", smt_bool_sortt{}});
@@ -46,9 +49,7 @@ TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]")
   CHECK(
     function_definition.parameters()[1].get() ==
     smt_identifier_termt{"y", smt_bool_sortt{}});
-  CHECK(
-    function_definition.definition() ==
-    smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}});
+  CHECK(function_definition.definition() == not_x);
 }
 
 TEST_CASE("smt_get_value_commandt getter", "[core][smt2_incremental]")

unit/solvers/smt2_incremental/smt_terms.cpp

@@ -33,19 +33,6 @@ TEST_CASE(
   REQUIRE_FALSE(smt_bool_literal_termt{false}.value());
 }
 
-TEST_CASE("smt_not_termt sort.", "[core][smt2_incremental]")
-{
-  REQUIRE(
-    smt_not_termt{smt_bool_literal_termt{true}}.get_sort() == smt_bool_sortt{});
-}
-
-TEST_CASE("smt_not_termt operand getter.", "[core][smt2_incremental]")
-{
-  const smt_bool_literal_termt bool_term{true};
-  const smt_not_termt not_term{bool_term};
-  REQUIRE(not_term.operand() == bool_term);
-}
-
 TEST_CASE("smt_identifier_termt construction", "[core][smt2_incremental]")
 {
   cbmc_invariants_should_throwt invariants_throw;
@@ -78,11 +65,6 @@ TEST_CASE("smt_termt equality.", "[core][smt2_incremental]")
   CHECK(
     smt_bit_vector_constant_termt{42, 8} !=
     smt_bit_vector_constant_termt{12, 8});
-  smt_termt not_false = smt_not_termt{smt_bool_literal_termt{false}};
-  smt_termt not_true = smt_not_termt{smt_bool_literal_termt{true}};
-  CHECK_FALSE(not_false == true_term);
-  CHECK_FALSE(not_false == not_true);
-  CHECK(not_false == smt_not_termt{smt_bool_literal_termt{false}});
 }
 
 template <typename expected_termt>
@@ -104,18 +86,6 @@ class term_visit_type_checkert final : public smt_term_const_downcast_visitort
     }
   }
 
-  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)
@@ -162,12 +132,6 @@ 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>()
 {
@@ -191,7 +155,6 @@ 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)

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -16,13 +16,6 @@ TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]")
   CHECK(smt_to_smt2_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)");
 }
 
-TEST_CASE("Test smt_not_termt to string conversion", "[core][smt2_incremental]")
-{
-  CHECK(
-    smt_to_smt2_string(smt_not_termt{
-      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(not |foo|)");
-}
-
 TEST_CASE(
   "Test smt_bit_vector_constant_termt to string conversion",
   "[core][smt2_incremental]")