cprover
Loading...
Searching...
No Matches
smt_sorts.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "smt_sorts.h"
4
5#include <util/invariant.h>
6
7// Define the irep_idts for sorts.
8#define SORT_ID(the_id) \
9 const irep_idt ID_smt_##the_id##_sort{"smt_" #the_id "_sort"};
10#include "smt_sorts.def"
11
12#undef SORT_ID
13
14#define SORT_ID(the_id) \
15 template <> \
16 const smt_##the_id##_sortt *smt_sortt::cast<smt_##the_id##_sortt>() const & \
17 { \
18 return id() == ID_smt_##the_id##_sort \
19 ? static_cast<const smt_##the_id##_sortt *>(this) \
20 : nullptr; \
21 }
22#include "smt_sorts.def" // NOLINT(build/include)
23#undef SORT_ID
24
25#define SORT_ID(the_id) \
26 template <> \
27 optionalt<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() && \
28 { \
29 if(id() == ID_smt_##the_id##_sort) \
30 return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))}; \
31 else \
32 return {}; \
33 }
34#include "smt_sorts.def" // NOLINT(build/include)
35#undef SORT_ID
36
37bool smt_sortt::operator==(const smt_sortt &other) const
38{
39 return irept::operator==(other);
40}
41
42bool smt_sortt::operator!=(const smt_sortt &other) const
43{
44 return !(*this == other);
45}
46
48{
49}
50
52 : smt_sortt{ID_smt_bit_vector_sort}
53{
55 bit_width > 0,
56 "The definition of SMT2 bit vector theory requires the number of "
57 "bits to be greater than 0.");
58 set_size_t(ID_width, bit_width);
59}
60
62{
63 return get_size_t(ID_width);
64}
65
67 const smt_sortt &index_sort,
68 const smt_sortt &element_sort)
69 : smt_sortt{ID_smt_array_sort}
70{
71 add(ID_index, index_sort);
72 add(ID_value, element_sort);
73}
74
76{
77 return static_cast<const smt_sortt &>(find(ID_index));
78}
79
81{
82 return static_cast<const smt_sortt &>(find(ID_value));
83}
84
85template <typename visitort>
86void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
87{
88#define SORT_ID(the_id) \
89 if(id == ID_smt_##the_id##_sort) \
90 return visitor.visit(static_cast<const smt_##the_id##_sortt &>(sort));
91#include "smt_sorts.def"
92#undef SORT_ID
94}
95
97{
98 ::accept(*this, id(), visitor);
99}
100
102{
103 ::accept(*this, id(), std::move(visitor));
104}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
bool operator==(const irept &other) const
Definition irep.cpp:141
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:67
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:86
irept & add(const irep_idt &name)
Definition irep.cpp:111
const smt_sortt & element_sort() const
Definition smt_sorts.cpp:80
const smt_sortt & index_sort() const
Definition smt_sorts.cpp:75
smt_array_sortt(const smt_sortt &index_sort, const smt_sortt &element_sort)
Definition smt_sorts.cpp:66
std::size_t bit_width() const
Definition smt_sorts.cpp:61
smt_bit_vector_sortt(std::size_t bit_width)
Definition smt_sorts.cpp:51
bool operator==(const smt_sortt &) const
Definition smt_sorts.cpp:37
bool operator!=(const smt_sortt &) const
Definition smt_sorts.cpp:42
void accept(smt_sort_const_downcast_visitort &) const
Definition smt_sorts.cpp:96
void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
Definition smt_sorts.cpp:86
Data structure for smt sorts.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423