7#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
8#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H
37 template <
typename derivedt>
46 template <
typename sub_
classt>
47 const sub_classt *
cast() const &;
49 template <typename sub_classt>
56template <typename derivedt>
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.");
65template <
typename derivedt>
68 return static_cast<irept &&
>(std::move(sort));
71template <
typename derivedt>
74 return static_cast<const smt_sortt &
>(irep);
103#define SORT_ID(the_id) virtual void visit(const smt_##the_id##_sortt &) = 0;
104#include "smt_sorts.def"
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const smt_sortt & element_sort() const
const smt_sortt & index_sort() const
smt_array_sortt(const smt_sortt &index_sort, const smt_sortt &element_sort)
std::size_t bit_width() const
smt_bit_vector_sortt(std::size_t bit_width)
static irept upcast(smt_sortt sort)
static const smt_sortt & downcast(const irept &)
bool operator==(const smt_sortt &) const
irept(const irep_idt &_id)
const sub_classt * cast() const &
bool operator!=(const smt_sortt &) const
void accept(smt_sort_const_downcast_visitort &) const