CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
smt_options.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "smt_options.h"
4
5// Define the irep_idts for options.
6#define OPTION_ID(the_id) \
7 const irep_idt ID_smt_option_##the_id{"smt_option_" #the_id};
8#include "smt_options.def"
9
10#undef OPTION_ID
11
13{
14}
15
16bool smt_optiont::operator==(const smt_optiont &other) const
17{
18 return irept::operator==(other);
19}
20
21bool smt_optiont::operator!=(const smt_optiont &other) const
22{
23 return !(*this == other);
24}
25
31
33{
34 return get_bool(ID_value);
35}
36
37template <typename visitort>
38void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
39{
40#define OPTION_ID(the_id) \
41 if(id == ID_smt_option_##the_id) \
42 return visitor.visit(static_cast<const smt_option_##the_id##t &>(option));
43// The include below is marked as nolint because including the same file
44// multiple times is required as part of the x macro pattern.
45#include "smt_options.def" // NOLINT(build/include)
46#undef OPTION_ID
48}
49
54
56{
57 ::accept(*this, id(), std::move(visitor));
58}
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
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
bool operator==(const irept &other) const
Definition irep.cpp:133
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
smt_option_produce_modelst(bool setting)
void accept(smt_option_const_downcast_visitort &) const
bool operator==(const smt_optiont &) const
smt_optiont()=delete
bool operator!=(const smt_optiont &) const
void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525