CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
smt_index.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "smt_index.h"
4
5// Define the irep_idts for kinds of index.
6const irep_idt ID_smt_numeral_index{"smt_numeral_index"};
7const irep_idt ID_smt_symbol_index{"smt_symbol_index"};
8
9bool smt_indext::operator==(const smt_indext &other) const
10{
11 return irept::operator==(other);
12}
13
14bool smt_indext::operator!=(const smt_indext &other) const
15{
16 return !(*this == other);
17}
18
19template <>
20const smt_numeral_indext *smt_indext::cast<smt_numeral_indext>() const &
21{
22 return id() == ID_smt_numeral_index
23 ? static_cast<const smt_numeral_indext *>(this)
24 : nullptr;
25}
26
27template <>
28const smt_symbol_indext *smt_indext::cast<smt_symbol_indext>() const &
29{
30 return id() == ID_smt_symbol_index
31 ? static_cast<const smt_symbol_indext *>(this)
32 : nullptr;
33}
34
36{
37 if(const auto numeral = this->cast<smt_numeral_indext>())
38 return visitor.visit(*numeral);
39 if(const auto symbol = this->cast<smt_symbol_indext>())
40 return visitor.visit(*symbol);
42}
43
49
50std::size_t smt_numeral_indext::value() const
51{
52 return get_size_t(ID_value);
53}
54
61
virtual bool visit(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from trace t Depending on the instruction type it may com...
Definition ai.cpp:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool empty() const
Definition dstring.h:89
bool operator==(const irept &other) const
Definition irep.cpp:133
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:67
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:82
const irep_idt & id() const
Definition irep.h:388
For implementation of indexed identifiers.
Definition smt_index.h:14
bool operator!=(const smt_indext &) const
Definition smt_index.cpp:14
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_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
const irep_idt ID_smt_symbol_index
Definition smt_index.cpp:7
const irep_idt ID_smt_numeral_index
Definition smt_index.cpp:6
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463