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>
13#define SORT_ID(the_id) \
15 const smt_##the_id##_sortt *smt_sortt::cast<smt_##the_id##_sortt>() const & \
17 return id() == ID_smt_##the_id##_sort \
18 ? static_cast<const smt_##the_id##_sortt *>(this) \
21#include <solvers/smt2_incremental/smt_sorts.def>
24#define SORT_ID(the_id) \
26 optionalt<smt_##the_id##_sortt> smt_sortt::cast<smt_##the_id##_sortt>() && \
28 if(id() == ID_smt_##the_id##_sort) \
29 return {std::move(*static_cast<const smt_##the_id##_sortt *>(this))}; \
33#include <solvers/smt2_incremental/smt_sorts.def>
43 return !(*
this == other);
55 "The definition of SMT2 bit vector theory requires the number of "
56 "bits to be greater than 0.");
65template <
typename visitort>
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"
83 ::accept(*
this,
id(), std::move(visitor));
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool operator==(const irept &other) const
std::size_t get_size_t(const irep_idt &name) const
void set_size_t(const irep_idt &name, const std::size_t value)
std::size_t bit_width() const
smt_bit_vector_sortt(std::size_t bit_width)
bool operator==(const smt_sortt &) const
bool operator!=(const smt_sortt &) const
void accept(smt_sort_const_downcast_visitort &) const
void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
Data structure for smt sorts.
#define UNREACHABLE
This should be used to mark dead code.