cprover
smt_sorts.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
6
7#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
8#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
9
10#include <util/irep.h>
11#include <util/optional.h>
12
13#include <type_traits>
14
16
17class smt_sortt : protected irept
18{
19public:
20 // smt_sortt does not support the notion of an empty / null state. Use
21 // optionalt<smt_sortt> instead if an empty sort is required.
22 smt_sortt() = delete;
23
24 using irept::pretty;
25
26 bool operator==(const smt_sortt &) const;
27 bool operator!=(const smt_sortt &) const;
28
31
37 template <typename derivedt>
38 class storert
39 {
40 protected:
42 static irept upcast(smt_sortt sort);
43 static const smt_sortt &downcast(const irept &);
44 };
45
46 template <typename sub_classt>
47 const sub_classt *cast() const &;
48
49 template <typename sub_classt>
50 optionalt<sub_classt> cast() &&;
51
52protected:
53 using irept::irept;
54};
55
56template <typename derivedt>
58{
59 static_assert(
60 std::is_base_of<irept, derivedt>::value &&
61 std::is_base_of<storert<derivedt>, derivedt>::value,
62 "Only irept based classes need to upcast smt_sortt to store it.");
63}
64
65template <typename derivedt>
67{
68 return static_cast<irept &&>(std::move(sort));
69}
70
71template <typename derivedt>
73{
74 return static_cast<const smt_sortt &>(irep);
75}
76
77class smt_bool_sortt final : public smt_sortt
78{
79public:
81};
82
83class smt_bit_vector_sortt final : public smt_sortt
84{
85public:
86 explicit smt_bit_vector_sortt(std::size_t bit_width);
87 std::size_t bit_width() const;
88};
89
91{
92public:
93#define SORT_ID(the_id) virtual void visit(const smt_##the_id##_sortt &) = 0;
94#include "smt_sorts.def"
95#undef SORT_ID
96};
97
98#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
Class for adding the ability to up and down cast smt_sortt to and from irept.
Definition: smt_sorts.h:39
static irept upcast(smt_sortt sort)
Definition: smt_sorts.h:66
static const smt_sortt & downcast(const irept &)
Definition: smt_sorts.h:72
bool operator==(const smt_sortt &) const
Definition: smt_sorts.cpp:36
const sub_classt * cast() const &
bool operator!=(const smt_sortt &) const
Definition: smt_sorts.cpp:41
smt_sortt()=delete
void accept(smt_sort_const_downcast_visitort &) const
Definition: smt_sorts.cpp:76
nonstd::optional< T > optionalt
Definition: optional.h:35