Remove macro-definition of signed_greater_than_or_equal from X-macro.

Given that this was the last macro definition in `smt_bit_vector_theory.def`,
also delete that file along with its usages in the header and implementation
file.

Author: NlightNFotis

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -19,30 +19,6 @@ static void validate_bit_vector_predicate_arguments(
     "Left and right operands must have the same bit width.");
 }
 
-#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name)               \
-  void smt_bit_vector_theoryt::the_name##t::validate(                          \
-    const smt_termt &left, const smt_termt &right)                             \
-  {                                                                            \
-    validate_bit_vector_predicate_arguments(left, right);                      \
-  }                                                                            \
-                                                                               \
-  smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort(                  \
-    const smt_termt &, const smt_termt &)                                      \
-  {                                                                            \
-    return smt_bool_sortt{};                                                   \
-  }                                                                            \
-                                                                               \
-  const char *smt_bit_vector_theoryt::the_name##t::identifier()                \
-  {                                                                            \
-    return #the_identifier;                                                    \
-  }                                                                            \
-                                                                               \
-  const smt_function_application_termt::factoryt<                              \
-    smt_bit_vector_theoryt::the_name##t>                                       \
-    smt_bit_vector_theoryt::the_name{};
-#include "smt_bit_vector_theory.def"
-#undef SMT_BITVECTOR_THEORY_PREDICATE
-
 // Relational operator definitions
 
 const char *smt_bit_vector_theoryt::unsigned_less_thant::identifier()
@@ -206,3 +182,26 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::signed_greater_thant>
   smt_bit_vector_theoryt::signed_greater_than{};
+
+const char *smt_bit_vector_theoryt::signed_greater_than_or_equalt::identifier()
+{
+  return "bvsge";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_greater_than_or_equalt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_predicate_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::signed_greater_than_or_equalt>
+  smt_bit_vector_theoryt::signed_greater_than_or_equal{};

src/solvers/smt2_incremental/smt_bit_vector_theory.def

@@ -8,19 +8,6 @@
 class smt_bit_vector_theoryt
 {
 public:
-#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name)               \
-  /* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */  \
-  struct the_name##t final                                                     \
-  {                                                                            \
-    static const char *identifier();                                           \
-    static smt_sortt                                                           \
-    return_sort(const smt_termt &left, const smt_termt &right);                \
-    static void validate(const smt_termt &left, const smt_termt &right);       \
-  };                                                                           \
-  static const smt_function_application_termt::factoryt<the_name##t> the_name;
-#include "smt_bit_vector_theory.def"
-#undef SMT_BITVECTOR_THEORY_PREDICATE
-
   // Relational operator class declarations
   struct unsigned_less_thant final
   {
@@ -87,6 +74,16 @@ class smt_bit_vector_theoryt
   };
   static const smt_function_application_termt::factoryt<signed_greater_thant>
     signed_greater_than;
+
+  struct signed_greater_than_or_equalt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<
+    signed_greater_than_or_equalt>
+    signed_greater_than_or_equal;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H