CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
smt_logics.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "smt_logics.h"
4
5// Define the irep_idts for logics.
6#define LOGIC_ID(the_id, the_name) \
7 const irep_idt ID_smt_logic_##the_id{"smt_logic_" #the_id};
8#include "smt_logics.def"
9
10#undef LOGIC_ID
11
12bool smt_logict::operator==(const smt_logict &other) const
13{
14 return irept::operator==(other);
15}
16
17bool smt_logict::operator!=(const smt_logict &other) const
18{
19 return !(*this == other);
20}
21
22template <typename visitort>
23void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
24{
25#define LOGIC_ID(the_id, the_name) \
26 if(id == ID_smt_logic_##the_id) \
27 return visitor.visit(static_cast<const smt_logic_##the_id##t &>(logic));
28// The include below is marked as nolint because including the same file
29// multiple times is required as part of the x macro pattern.
30#include "smt_logics.def" // NOLINT(build/include)
31#undef LOGIC_ID
33}
34
39
41{
42 ::accept(*this, id(), std::move(visitor));
43}
44
45#define LOGIC_ID(the_id, the_name) \
46 smt_logic_##the_id##t::smt_logic_##the_id##t() \
47 : smt_logict{ID_smt_logic_##the_id} \
48 { \
49 }
50#include "smt_logics.def"
51#undef LOGIC_ID
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 operator==(const irept &other) const
Definition irep.cpp:133
void accept(smt_logic_const_downcast_visitort &) const
bool operator==(const smt_logict &) const
bool operator!=(const smt_logict &) const
void accept(const smt_logict &logic, const irep_idt &id, visitort &&visitor)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525