cprover
Loading...
Searching...
No Matches
smt_options.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
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 <solvers/smt2_incremental/smt_options.def>
9#undef OPTION_ID
10
12{
13}
14
15bool smt_optiont::operator==(const smt_optiont &other) const
16{
17 return irept::operator==(other);
18}
19
20bool smt_optiont::operator!=(const smt_optiont &other) const
21{
22 return !(*this == other);
23}
24
26 : smt_optiont{ID_smt_option_produce_models}
27{
28 set(ID_value, setting);
29}
30
32{
33 return get_bool(ID_value);
34}
35
36template <typename visitort>
37void accept(const smt_optiont &option, const irep_idt &id, visitort &&visitor)
38{
39#define OPTION_ID(the_id) \
40 if(id == ID_smt_option_##the_id) \
41 return visitor.visit(static_cast<const smt_option_##the_id##t &>(option));
42// The include below is marked as nolint because including the same file
43// multiple times is required as part of the x macro pattern.
44#include <solvers/smt2_incremental/smt_options.def> // NOLINT(build/include)
45#undef OPTION_ID
47}
48
50{
51 ::accept(*this, id(), visitor);
52}
53
55{
56 ::accept(*this, id(), std::move(visitor));
57}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
bool get_bool(const irep_idt &name) const
Definition irep.cpp:58
bool operator==(const irept &other) const
Definition irep.cpp:146
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
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:503