cprover
Loading...
Searching...
No Matches
smt_responses.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
5#include <util/range.h>
6
7// Define the irep_idts for responses.
8#define RESPONSE_ID(the_id, the_base) \
9 const irep_idt ID_smt_##the_id##_response{"smt_" #the_id "_response"};
10#include <solvers/smt2_incremental/smt_responses.def>
11#undef RESPONSE_ID
12
14{
15 return irept::operator==(other);
16}
17
19{
20 return !(*this == other);
21}
22
23#define RESPONSE_ID(the_id, the_base) \
24 template <> \
25 const smt_##the_id##_responset *the_base::cast<smt_##the_id##_responset>() \
26 const & \
27 { \
28 return id() == ID_smt_##the_id##_response \
29 ? static_cast<const smt_##the_id##_responset *>(this) \
30 : nullptr; \
31 }
32#include <solvers/smt2_incremental/smt_responses.def> // NOLINT(build/include)
33#undef RESPONSE_ID
34
35template <typename sub_classt>
36const sub_classt *smt_responset::cast() const &
37{
38 return nullptr;
39}
40
43{
44 return irept::operator==(other);
45}
46
49{
50 return !(*this == other);
51}
52
54 : smt_responset{ID_smt_success_response}
55{
56}
57
59 : smt_check_sat_response_kindt{ID_smt_sat_response}
62
64 : smt_check_sat_response_kindt{ID_smt_unsat_response}
65{
66}
67
69 : smt_check_sat_response_kindt{ID_smt_unknown_response}
70{
71}
72
73template <typename derivedt>
75{
76 static_assert(
77 std::is_base_of<irept, derivedt>::value &&
78 std::is_base_of<storert<derivedt>, derivedt>::value,
79 "Only irept based classes need to upcast smt_termt to store it.");
80}
81
82template <typename derivedt>
84 smt_check_sat_response_kindt check_sat_response_kind)
85{
86 return static_cast<irept &&>(std::move(check_sat_response_kind));
87}
88
89template <typename derivedt>
92{
93 return static_cast<const smt_check_sat_response_kindt &>(irep);
94}
95
98 : smt_responset{ID_smt_check_sat_response}
99{
100 set(ID_value, upcast(std::move(kind)));
101}
102
104{
105 return downcast(find(ID_value));
106}
107
109 smt_termt descriptor,
110 smt_termt value)
111{
112 INVARIANT(
114 "SMT valuation pair must have matching sort for the descriptor and value.");
115 get_sub().push_back(upcast(std::move(descriptor)));
116 get_sub().push_back(upcast(std::move(value)));
117}
118
120 irep_idt descriptor,
121 const smt_termt &value)
122 : valuation_pairt(smt_identifier_termt{descriptor, value.get_sort()}, value)
123{
124}
125
127{
128 return downcast(get_sub().at(0));
129}
130
132{
133 return downcast(get_sub().at(1));
134}
135
138{
139 return irept::operator==(other);
140}
141
144{
145 return !(*this == other);
146}
147
149 std::vector<valuation_pairt> pairs)
150 : smt_responset(ID_smt_get_value_response)
151{
152 // SMT-LIB standard version 2.6 requires one or more pairs.
153 // See page 47, figure 3.9: Command responses.
154 INVARIANT(
155 !pairs.empty(), "Get value response must contain one or more pairs.");
156 for(auto &pair : pairs)
157 {
158 get_sub().push_back(std::move(pair));
159 }
160}
161
162std::vector<
163 std::reference_wrapper<const smt_get_value_responset::valuation_pairt>>
165{
166 return make_range(get_sub()).map([](const irept &pair) {
167 return std::cref(static_cast<const valuation_pairt &>(pair));
168 });
169}
170
172 : smt_responset{ID_smt_unsupported_response}
173{
174}
175
177 : smt_responset{ID_smt_error_response}
178{
179 set(ID_value, message);
180}
181
183{
184 return get(ID_value);
185}
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 operator==(const irept &other) const
Definition: irep.cpp:146
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
subt & get_sub()
Definition: irep.h:456
static irept upcast(smt_check_sat_response_kindt check_sat_response_kind)
static const smt_check_sat_response_kindt & downcast(const irept &)
bool operator==(const smt_check_sat_response_kindt &) const
bool operator!=(const smt_check_sat_response_kindt &) const
smt_check_sat_responset(smt_check_sat_response_kindt kind)
const smt_check_sat_response_kindt & kind() const
const irep_idt & message() const
smt_error_responset(irep_idt message)
bool operator==(const valuation_pairt &) const
bool operator!=(const valuation_pairt &) const
smt_get_value_responset(std::vector< valuation_pairt > pairs)
std::vector< std::reference_wrapper< const valuation_pairt > > pairs() const
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
bool operator!=(const smt_responset &) const
bool operator==(const smt_responset &) const
const sub_classt * cast() const &
static irept upcast(smt_termt term)
Definition: smt_terms.h:60
static const smt_termt & downcast(const irept &)
Definition: smt_terms.h:66
const smt_sortt & get_sort() const
Definition: smt_terms.cpp:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423