cprover
Loading...
Searching...
No Matches
smt_index.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
5
6#include <util/irep.h>
7
9
13class smt_indext : protected irept
14{
15public:
16 // smt_indext does not support the notion of an empty / null state. Use
17 // std::optional<smt_indext> instead if an empty index is required.
18 smt_indext() = delete;
19
20 using irept::pretty;
21
22 bool operator==(const smt_indext &) const;
23 bool operator!=(const smt_indext &) const;
24
25 template <typename sub_classt>
26 const sub_classt *cast() const &;
27
29
35 template <typename derivedt>
36 class storert
37 {
38 protected:
40 static irept upcast(smt_indext index);
41 static const smt_indext &downcast(const irept &);
42 };
43
44protected:
45 using irept::irept;
46};
47
48template <typename derivedt>
50{
51 static_assert(
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.");
55}
56
57template <typename derivedt>
59{
60 return static_cast<irept &&>(std::move(index));
61}
62
63template <typename derivedt>
65{
66 return static_cast<const smt_indext &>(irep);
67}
68
70{
71public:
72 explicit smt_numeral_indext(std::size_t value);
73 std::size_t value() const;
74};
75
77{
78public:
80 irep_idt identifier() const;
81};
82
84{
85public:
86 virtual void visit(const smt_numeral_indext &) = 0;
87 virtual void visit(const smt_symbol_indext &) = 0;
88};
89
90#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INDEX_H
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
irept(const irep_idt &_id)
Definition irep.h:377
virtual void visit(const smt_symbol_indext &)=0
virtual void visit(const smt_numeral_indext &)=0
static irept upcast(smt_indext index)
Definition smt_index.h:58
static const smt_indext & downcast(const irept &)
Definition smt_index.h:64
bool operator!=(const smt_indext &) const
Definition smt_index.cpp:14
const sub_classt * cast() const &
irept(const irep_idt &_id)
Definition irep.h:377
bool operator==(const smt_indext &) const
Definition smt_index.cpp:9
void accept(smt_index_const_downcast_visitort &) const
Definition smt_index.cpp:35
smt_indext()=delete
smt_numeral_indext(std::size_t value)
Definition smt_index.cpp:44
std::size_t value() const
Definition smt_index.cpp:50
smt_symbol_indext(irep_idt identifier)
Definition smt_index.cpp:55
irep_idt identifier() const
Definition smt_index.cpp:62
dstringt irep_idt