cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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
12
smt_optiont::smt_optiont
(
const
irep_idt
id
) :
irept
(
id
)
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
26
smt_option_produce_modelst::smt_option_produce_modelst
(
bool
setting
)
27
:
smt_optiont
{ID_smt_option_produce_models}
28
{
29
set
(ID_value,
setting
);
30
}
31
32
bool
smt_option_produce_modelst::setting
()
const
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
47
UNREACHABLE
;
48
}
49
50
void
smt_optiont::accept
(
smt_option_const_downcast_visitort
&visitor)
const
51
{
52
::accept
(*
this
,
id
(), visitor);
53
}
54
55
void
smt_optiont::accept
(
smt_option_const_downcast_visitort
&&visitor)
const
56
{
57
::accept
(*
this
,
id
(), std::move(visitor));
58
}
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition
irep.cpp:57
irept::operator==
bool operator==(const irept &other) const
Definition
irep.cpp:133
irept::irept
irept(const irep_idt &_id)
Definition
irep.h:377
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition
irep.h:412
irept::id
const irep_idt & id() const
Definition
irep.h:388
smt_option_const_downcast_visitort
Definition
smt_options.h:72
smt_option_produce_modelst::setting
bool setting() const
Definition
smt_options.cpp:32
smt_option_produce_modelst::smt_option_produce_modelst
smt_option_produce_modelst(bool setting)
Definition
smt_options.cpp:26
smt_optiont
Definition
smt_options.h:11
smt_optiont::accept
void accept(smt_option_const_downcast_visitort &) const
Definition
smt_options.cpp:50
smt_optiont::operator==
bool operator==(const smt_optiont &) const
Definition
smt_options.cpp:16
smt_optiont::smt_optiont
smt_optiont()=delete
smt_optiont::operator!=
bool operator!=(const smt_optiont &) const
Definition
smt_options.cpp:21
smt_options.h
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition
invariant.h:525
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
solvers
smt2_incremental
ast
smt_options.cpp
Generated by
1.17.0