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_core_theory.cpp

@@ -0,0 +1,23 @@
+// Author: Diffblue Ltd.
+
+#include <testing-utils/use_catch.h>
+
+#include <solvers/smt2_incremental/smt_core_theory.h>
+#include <solvers/smt2_incremental/smt_terms.h>
+
+#include <util/mp_arith.h>
+
+TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]")
+{
+  const smt_bool_literal_termt operand{true};
+  const auto not_term = smt_core_theoryt::make_not(operand);
+
+  CHECK(not_term.get_sort() == smt_bool_sortt{});
+  CHECK(
+    not_term.function_identifier() ==
+    smt_identifier_termt{"not", smt_bool_sortt{}});
+  REQUIRE(not_term.arguments().size() == 1);
+  REQUIRE(not_term.arguments()[0].get() == operand);
+  cbmc_invariants_should_throwt invariants_throw;
+  CHECK_THROWS(smt_core_theoryt::make_not(smt_bit_vector_constant_termt{0, 1}));
+}