Remove macro-definition of unsigned_less_than_or_equalt from X-macro.

And substitute it with a concrete class implementation.

Author: NlightNFotis

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -43,6 +43,8 @@ static void validate_bit_vector_predicate_arguments(
 #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";
@@ -65,3 +67,26 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(
 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{};

src/solvers/smt2_incremental/smt_bit_vector_theory.def

@@ -3,7 +3,6 @@
 /// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
 /// set of bitvector theory functions which are implemented and it is used to
 /// automate repetitive parts of the implementation.
-SMT_BITVECTOR_THEORY_PREDICATE(bvule, unsigned_less_than_or_equal)
 SMT_BITVECTOR_THEORY_PREDICATE(bvugt, unsigned_greater_than)
 SMT_BITVECTOR_THEORY_PREDICATE(bvuge, unsigned_greater_than_or_equal)
 SMT_BITVECTOR_THEORY_PREDICATE(bvslt, signed_less_than)

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -21,6 +21,7 @@ class smt_bit_vector_theoryt
 #include "smt_bit_vector_theory.def"
 #undef SMT_BITVECTOR_THEORY_PREDICATE
 
+  // Relational operator class declarations
   struct unsigned_less_thant final
   {
     static const char *identifier();
@@ -29,6 +30,16 @@ class smt_bit_vector_theoryt
   };
   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;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H