3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
25 template <
typename sub_
classt>
26 const sub_classt *
cast() const &;
35 template <typename derivedt>
48template <
typename derivedt>
52 std::is_base_of<irept, derivedt>::value &&
53 std::is_base_of<storert<derivedt>, derivedt>::value,
54 "Only irept based classes need to upcast smt_sortt to store it.");
57template <
typename derivedt>
60 return static_cast<irept &&
>(std::move(index));
63template <
typename derivedt>
73 std::size_t
value()
const;
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
irept(const irep_idt &_id)
virtual void visit(const smt_symbol_indext &)=0
virtual void visit(const smt_numeral_indext &)=0
static irept upcast(smt_indext index)
static const smt_indext & downcast(const irept &)
bool operator!=(const smt_indext &) const
const sub_classt * cast() const &
irept(const irep_idt &_id)
bool operator==(const smt_indext &) const
void accept(smt_index_const_downcast_visitort &) const
smt_numeral_indext(std::size_t value)
std::size_t value() const
smt_symbol_indext(irep_idt identifier)
irep_idt identifier() const