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 <solvers/smt2_incremental/smt_sorts.def>
11#undef SORT_ID
12
13#define SORT_ID(the_id) \
14 template <> \
15 const smt_##the_id##_sortt *smt_sortt::cast<smt_##the_id##_sortt>() const & \
16 { \
17 return id() == ID_smt_##the_id##_sort \
18 ? static_cast<const smt_##the_id##_sortt *>(this) \
19 : nullptr; \
20 }
21#include <solvers/smt2_incremental/smt_sorts.def> // NOLINT(build/include)
22#undef SORT_ID
23
24#define SORT_ID(the_id) \
25 template <> \
26 optionalt<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() && \
27 { \
28 if(id() == ID_smt_##the_id##_sort) \
29 return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))}; \
30 else \
31 return {}; \
32 }
33#include <solvers/smt2_incremental/smt_sorts.def> // NOLINT(build/include)
34#undef SORT_ID
35
36bool smt_sortt::operator==(const smt_sortt &other) const
37{
38 return irept::operator==(other);
39}
40
41bool smt_sortt::operator!=(const smt_sortt &other) const
42{
43 return !(*this == other);
44}
45
49
52{
54 bit_width > 0,
55 "The definition of SMT2 bit vector theory requires the number of "
56 "bits to be greater than 0.");
58}
59
61{
62 return get_size_t(ID_width);
63}
64
65template <typename visitort>
66void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
67{
68#define SORT_ID(the_id) \
69 if(id == ID_smt_##the_id##_sort) \
70 return visitor.visit(static_cast<const smt_##the_id##_sortt &>(sort));
71#include "smt_sorts.def"
72#undef SORT_ID
74}
75
80
82{
83 ::accept(*this, id(), std::move(visitor));
84}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool operator==(const irept &other) const
Definition irep.cpp:146
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:68
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:87
std::size_t bit_width() const
Definition smt_sorts.cpp:60
smt_bit_vector_sortt(std::size_t bit_width)
Definition smt_sorts.cpp:50
bool operator==(const smt_sortt &) const
Definition smt_sorts.cpp:36
bool operator!=(const smt_sortt &) const
Definition smt_sorts.cpp:41
void accept(smt_sort_const_downcast_visitort &) const
Definition smt_sorts.cpp:76
void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
Definition smt_sorts.cpp:66
Data structure for smt sorts.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423