Add operator== to smt_sortt

Author: thomasspriggs

src/solvers/smt2_incremental/smt_sorts.cpp

@@ -10,6 +10,16 @@
 #include <solvers/smt2_incremental/smt_sorts.def>
 #undef SORT_ID
 
+bool smt_sortt::operator==(const smt_sortt &other) const
+{
+  return irept::operator==(other);
+}
+
+bool smt_sortt::operator!=(const smt_sortt &other) const
+{
+  return !(*this == other);
+}
+
 smt_bool_sortt::smt_bool_sortt() : smt_sortt{ID_smt_bool_sort}
 {
 }

src/solvers/smt2_incremental/smt_sorts.h

@@ -20,6 +20,9 @@ class smt_sortt : protected irept
 
   using irept::pretty;
 
+  bool operator==(const smt_sortt &) const;
+  bool operator!=(const smt_sortt &) const;
+
   void accept(smt_sort_const_downcast_visitort &) const;
   void accept(smt_sort_const_downcast_visitort &&) const;
 

unit/solvers/smt2_incremental/smt_sorts.cpp

@@ -77,3 +77,16 @@ TEST_CASE("Visiting smt_bit_vec_sortt.", "[core][smt2_incremental]")
   REQUIRE_FALSE(visitor.bool_visited);
   REQUIRE(visitor.bit_vec_visited);
 }
+
+TEST_CASE("smt_sortt equality", "[core][smt2_incremental]")
+{
+  const smt_bool_sortt bool_sort1;
+  CHECK(bool_sort1 == bool_sort1);
+  const smt_bool_sortt bool_sort2;
+  CHECK(bool_sort1 == bool_sort2);
+  const smt_bit_vector_sortt bit_vector8{8};
+  CHECK(bit_vector8 == bit_vector8);
+  CHECK(bit_vector8 != bool_sort1);
+  const smt_bit_vector_sortt bit_vector16{16};
+  CHECK(bit_vector8 != bit_vector16);
+}