[Refactor] New SMT backend: Remove X-macro implementation from smt_bit_vector_theory

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -19,26 +19,189 @@ 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()
+{
+  return "bvult";
+}
+
+smt_sortt smt_bit_vector_theoryt::unsigned_less_thant::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::unsigned_less_thant::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::unsigned_less_thant>
+  smt_bit_vector_theoryt::unsigned_less_than{};
+
+const char *smt_bit_vector_theoryt::unsigned_less_than_or_equalt::identifier()
+{
+  return "bvule";
+}
+
+smt_sortt smt_bit_vector_theoryt::unsigned_less_than_or_equalt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::unsigned_less_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::unsigned_less_than_or_equalt>
+  smt_bit_vector_theoryt::unsigned_less_than_or_equal{};
+
+const char *smt_bit_vector_theoryt::unsigned_greater_thant::identifier()
+{
+  return "bvugt";
+}
+
+smt_sortt smt_bit_vector_theoryt::unsigned_greater_thant::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::unsigned_greater_thant::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::unsigned_greater_thant>
+  smt_bit_vector_theoryt::unsigned_greater_than{};
+
+const char *
+smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::identifier()
+{
+  return "bvuge";
+}
+
+smt_sortt smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::unsigned_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::unsigned_greater_than_or_equalt>
+  smt_bit_vector_theoryt::unsigned_greater_than_or_equal{};
+
+const char *smt_bit_vector_theoryt::signed_less_thant::identifier()
+{
+  return "bvslt";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_less_thant::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::signed_less_thant::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_less_thant>
+  smt_bit_vector_theoryt::signed_less_than{};
+
+const char *smt_bit_vector_theoryt::signed_less_than_or_equalt::identifier()
+{
+  return "bvsle";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_less_than_or_equalt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::signed_less_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_less_than_or_equalt>
+  smt_bit_vector_theoryt::signed_less_than_or_equal{};
+
+const char *smt_bit_vector_theoryt::signed_greater_thant::identifier()
+{
+  return "bvsgt";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_greater_thant::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return smt_bool_sortt{};
+}
+
+void smt_bit_vector_theoryt::signed_greater_thant::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_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.h

@@ -8,18 +8,82 @@
 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
+  {
+    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<unsigned_less_thant>
+    unsigned_less_than;
+
+  struct unsigned_less_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<
+    unsigned_less_than_or_equalt>
+    unsigned_less_than_or_equal;
+
+  struct unsigned_greater_thant 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<unsigned_greater_thant>
+    unsigned_greater_than;
+
+  struct unsigned_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<
+    unsigned_greater_than_or_equalt>
+    unsigned_greater_than_or_equal;
+
+  struct signed_less_thant 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_less_thant>
+    signed_less_than;
+
+  struct signed_less_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_less_than_or_equalt>
+    signed_less_than_or_equal;
+
+  struct signed_greater_thant 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_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