Skip to content

Commit d5c12a3

Browse files
committed
Add smt_sortt::storer as a way add storage of sorts
So that instances of `smt_sortt` can be stored in other `irept` derived classes without enabling upcasting of `smt_sortt` to `irept` from outside of the heirarchy of `irept` based classes.
1 parent 45ef48e commit d5c12a3

File tree

1 file changed

+37
-0
lines changed

1 file changed

+37
-0
lines changed

src/solvers/smt2_incremental/smt_sorts.h

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99

1010
#include <util/irep.h>
1111

12+
#include <type_traits>
13+
1214
class smt_sort_const_downcast_visitort;
1315

1416
class smt_sortt : protected irept
@@ -26,10 +28,45 @@ class smt_sortt : protected irept
2628
void accept(smt_sort_const_downcast_visitort &) const;
2729
void accept(smt_sort_const_downcast_visitort &&) const;
2830

31+
/// \brief Class for adding the ability to up and down cast smt_sortt to and
32+
/// from irept. These casts are required by other irept derived classes in
33+
/// order to store instances of smt_sortt inside them.
34+
/// \tparam derivedt The type of class which derives from this class and from
35+
/// irept.
36+
template <typename derivedt>
37+
class storert
38+
{
39+
protected:
40+
storert();
41+
static irept upcast(smt_sortt sort);
42+
static const smt_sortt &downcast(const irept &);
43+
};
44+
2945
protected:
3046
using irept::irept;
3147
};
3248

49+
template <typename derivedt>
50+
smt_sortt::storert<derivedt>::storert()
51+
{
52+
static_assert(
53+
std::is_base_of<irept, derivedt>::value &&
54+
std::is_base_of<storert<derivedt>, derivedt>::value,
55+
"Only irept based classes need to upcast smt_sortt to store it.");
56+
}
57+
58+
template <typename derivedt>
59+
irept smt_sortt::storert<derivedt>::upcast(smt_sortt sort)
60+
{
61+
return static_cast<irept &&>(std::move(sort));
62+
}
63+
64+
template <typename derivedt>
65+
const smt_sortt &smt_sortt::storert<derivedt>::downcast(const irept &irep)
66+
{
67+
return static_cast<const smt_sortt &>(irep);
68+
}
69+
3370
class smt_bool_sortt final : public smt_sortt
3471
{
3572
public:

0 commit comments

Comments
 (0)