cprover
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 
36 bool smt_sortt::operator==(const smt_sortt &other) const
37 {
38  return irept::operator==(other);
39 }
40 
41 bool smt_sortt::operator!=(const smt_sortt &other) const
42 {
43  return !(*this == other);
44 }
45 
47 {
48 }
49 
50 smt_bit_vector_sortt::smt_bit_vector_sortt(const std::size_t bit_width)
51  : smt_sortt{ID_smt_bit_vector_sort}
52 {
53  INVARIANT(
54  bit_width > 0,
55  "The definition of SMT2 bit vector theory requires the number of "
56  "bits to be greater than 0.");
57  set_size_t(ID_width, bit_width);
58 }
59 
61 {
62  return get_size_t(ID_width);
63 }
64 
65 template <typename visitort>
66 void 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 
77 {
78  ::accept(*this, id(), visitor);
79 }
80 
82 {
83  ::accept(*this, id(), std::move(visitor));
84 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
smt_sortt::operator!=
bool operator!=(const smt_sortt &) const
Definition: smt_sorts.cpp:41
smt_bit_vector_sortt::smt_bit_vector_sortt
smt_bit_vector_sortt(std::size_t bit_width)
Definition: smt_sorts.cpp:50
accept
void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
Definition: smt_sorts.cpp:66
invariant.h
smt_bool_sortt::smt_bool_sortt
smt_bool_sortt()
Definition: smt_sorts.cpp:46
smt_bit_vector_sortt::bit_width
std::size_t bit_width() const
Definition: smt_sorts.cpp:60
smt_sortt::accept
void accept(smt_sort_const_downcast_visitort &) const
Definition: smt_sorts.cpp:76
smt_sorts.h
Data structure for smt sorts.
smt_sortt::operator==
bool operator==(const smt_sortt &) const
Definition: smt_sorts.cpp:36
smt_sortt
Definition: smt_sorts.h:18
smt_sort_const_downcast_visitort
Definition: smt_sorts.h:91
irept::operator==
bool operator==(const irept &other) const
Definition: irep.cpp:146
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:68
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423