CBMC
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 
16 bool smt_optiont::operator==(const smt_optiont &other) const
17 {
18  return irept::operator==(other);
19 }
20 
21 bool smt_optiont::operator!=(const smt_optiont &other) const
22 {
23  return !(*this == other);
24 }
25 
27  : smt_optiont{ID_smt_option_produce_models}
28 {
29  set(ID_value, setting);
30 }
31 
33 {
34  return get_bool(ID_value);
35 }
36 
37 template <typename visitort>
38 void 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 
51 {
52  ::accept(*this, id(), visitor);
53 }
54 
56 {
57  ::accept(*this, id(), std::move(visitor));
58 }
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)
Definition: smt_options.cpp:26
void accept(smt_option_const_downcast_visitort &) const
Definition: smt_options.cpp:50
bool operator==(const smt_optiont &) const
Definition: smt_options.cpp:16
smt_optiont()=delete
bool operator!=(const smt_optiont &) const
Definition: smt_options.cpp:21
void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
Definition: smt_options.cpp:38
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525