cprover
Loading...
Searching...
No Matches
smt_options.h
Go to the documentation of this file.
1
// Author: Diffblue Ltd.
2
3
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
4
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
5
6
#include <
util/irep.h
>
7
8
class
smt_option_const_downcast_visitort
;
9
10
class
smt_optiont
:
protected
irept
11
{
12
public
:
13
// smt_optiont does not support the notion of an empty / null state. Use
14
// std::optional<smt_optiont> instead if an empty option is required.
15
smt_optiont
() =
delete
;
16
17
using
irept::pretty
;
18
19
bool
operator==
(
const
smt_optiont
&)
const
;
20
bool
operator!=
(
const
smt_optiont
&)
const
;
21
22
void
accept
(
smt_option_const_downcast_visitort
&)
const
;
23
void
accept
(
smt_option_const_downcast_visitort
&&)
const
;
24
30
template
<
typename
derivedt>
31
class
storert
32
{
33
protected
:
34
storert
();
35
static
irept
upcast
(
smt_optiont
option);
36
static
const
smt_optiont
&
downcast
(
const
irept
&);
37
};
38
39
protected
:
40
explicit
smt_optiont
(
irep_idt
id
);
41
};
42
43
template
<
typename
derivedt>
44
smt_optiont::storert<derivedt>::storert
()
45
{
46
static_assert
(
47
std::is_base_of<irept, derivedt>::value &&
48
std::is_base_of<storert<derivedt>, derivedt>::value,
49
"Only irept based classes need to upcast smt_termt to store it."
);
50
}
51
52
template
<
typename
derivedt>
53
irept
smt_optiont::storert<derivedt>::upcast
(
smt_optiont
option)
54
{
55
return
static_cast<
irept
&&
>
(std::move(option));
56
}
57
58
template
<
typename
derivedt>
59
const
smt_optiont
&
smt_optiont::storert<derivedt>::downcast
(
const
irept
&irep)
60
{
61
return
static_cast<
const
smt_optiont
&
>
(irep);
62
}
63
64
class
smt_option_produce_modelst
:
public
smt_optiont
65
{
66
public
:
67
explicit
smt_option_produce_modelst
(
bool
setting
);
68
bool
setting
()
const
;
69
};
70
71
class
smt_option_const_downcast_visitort
72
{
73
public
:
74
#define OPTION_ID(the_id) \
75
virtual void visit(const smt_option_##the_id##t &) = 0;
76
#include "smt_options.def"
77
#undef OPTION_ID
78
};
79
80
#endif
// CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_OPTIONS_H
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition
irep.cpp:482
irept::irept
irept(const irep_idt &_id)
Definition
irep.h:377
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::storert::downcast
static const smt_optiont & downcast(const irept &)
Definition
smt_options.h:59
smt_optiont::storert::upcast
static irept upcast(smt_optiont option)
Definition
smt_options.h:53
smt_optiont::storert::storert
storert()
Definition
smt_options.h:44
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
irep.h
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
solvers
smt2_incremental
ast
smt_options.h
Generated by
1.13.2