Add sort casting

For checking parameterised sorts.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_sorts.cpp

@@ -10,6 +10,29 @@
 #include <solvers/smt2_incremental/smt_sorts.def>
 #undef SORT_ID
 
+#define SORT_ID(the_id)                                                        \
+  template <>                                                                  \
+  const smt_##the_id##_sortt *smt_sortt::cast<smt_##the_id##_sortt>() const &  \
+  {                                                                            \
+    return id() == ID_smt_##the_id##_sort                                      \
+             ? static_cast<const smt_##the_id##_sortt *>(this)                 \
+             : nullptr;                                                        \
+  }
+#include <solvers/smt2_incremental/smt_sorts.def> // NOLINT(build/include)
+#undef SORT_ID
+
+#define SORT_ID(the_id)                                                        \
+  template <>                                                                  \
+  optionalt<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() &&   \
+  {                                                                            \
+    if(id() == ID_smt_##the_id##_sort)                                         \
+      return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))};    \
+    else                                                                       \
+      return {};                                                               \
+  }
+#include <solvers/smt2_incremental/smt_sorts.def> // NOLINT(build/include)
+#undef SORT_ID
+
 bool smt_sortt::operator==(const smt_sortt &other) const
 {
   return irept::operator==(other);

src/solvers/smt2_incremental/smt_sorts.h

@@ -8,6 +8,7 @@
 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
 
 #include <util/irep.h>
+#include <util/optional.h>
 
 #include <type_traits>
 
@@ -42,6 +43,12 @@ class smt_sortt : protected irept
     static const smt_sortt &downcast(const irept &);
   };
 
+  template <typename sub_classt>
+  const sub_classt *cast() const &;
+
+  template <typename sub_classt>
+  optionalt<sub_classt> cast() &&;
+
 protected:
   using irept::irept;
 };