cprover
Loading...
Searching...
No Matches
smt_commands.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#include "smt_commands.h"
4
5#include <util/range.h>
6
7#include <algorithm>
8
9// Define the irep_idts for commands.
10#define COMMAND_ID(the_id) \
11 const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
12#include "smt_commands.def"
13#undef COMMAND_ID
14
15bool smt_commandt::operator==(const smt_commandt &other) const
16{
17 return irept::operator==(other);
18}
19
20bool smt_commandt::operator!=(const smt_commandt &other) const
21{
22 return !(*this == other);
23}
24
26 : smt_commandt{ID_smt_assert_command}
27{
29 condition.get_sort() == smt_bool_sortt{},
30 "Only terms with boolean sorts can be asserted.");
31 set(ID_cond, upcast(std::move(condition)));
32}
33
35{
36 return downcast(find(ID_cond));
37}
38
40 : smt_commandt{ID_smt_check_sat_command}
41{
42}
43
46 std::vector<smt_sortt> parameter_sorts)
47 : smt_commandt{ID_smt_declare_function_command}
48{
49 set(ID_identifier, term_storert::upcast(std::move(identifier)));
50 std::transform(
51 std::make_move_iterator(parameter_sorts.begin()),
52 std::make_move_iterator(parameter_sorts.end()),
53 std::back_inserter(get_sub()),
54 [](smt_sortt &&parameter_sort) {
55 return sort_storert::upcast(std::move(parameter_sort));
56 });
57}
58
60{
61 return static_cast<const smt_identifier_termt &>(
62 term_storert::downcast(find(ID_identifier)));
63}
64
69
70std::vector<std::reference_wrapper<const smt_sortt>>
72{
73 return make_range(get_sub()).map([](const irept &parameter_sort) {
74 return std::cref(sort_storert::downcast(parameter_sort));
75 });
76}
77
79{
80}
81
84 std::vector<smt_identifier_termt> parameters,
86 : smt_commandt{ID_smt_define_function_command}
87{
88 set(
89 ID_identifier,
90 upcast(smt_identifier_termt{std::move(identifier), definition.get_sort()}));
91 std::transform(
92 std::make_move_iterator(parameters.begin()),
93 std::make_move_iterator(parameters.end()),
94 std::back_inserter(get_sub()),
95 [](smt_identifier_termt &&parameter) {
96 return upcast(std::move(parameter));
97 });
98 set(ID_code, upcast(std::move(definition)));
99}
100
102{
103 return static_cast<const smt_identifier_termt &>(
104 downcast(find(ID_identifier)));
105}
106
107std::vector<std::reference_wrapper<const smt_identifier_termt>>
109{
110 return make_range(get_sub()).map([](const irept &parameter) {
111 return std::cref(
112 static_cast<const smt_identifier_termt &>(downcast((parameter))));
113 });
114}
115
120
122{
123 return downcast(find(ID_code));
124}
125
127 : smt_commandt{ID_smt_get_value_command}
128{
129 set(ID_value, upcast(std::move(descriptor)));
130}
131
133{
134 return downcast(find(ID_value));
135}
136
138 : smt_commandt(ID_smt_push_command)
139{
140 set_size_t(ID_value, levels);
141}
142
144{
145 return get_size_t(ID_value);
146}
147
149 : smt_commandt(ID_smt_pop_command)
150{
151 set_size_t(ID_value, levels);
152}
153
155{
156 return get_size_t(ID_value);
157}
158
160 : smt_commandt(ID_smt_set_logic_command)
161{
162 set(ID_value, upcast(std::move(logic)));
163}
164
166{
167 return downcast(find(ID_value));
168}
169
171 : smt_commandt(ID_smt_set_option_command)
172{
173 set(ID_value, upcast(std::move(option)));
174}
175
177{
178 return downcast(find(ID_value));
179}
180
181template <typename visitort>
182void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
183{
184#define COMMAND_ID(the_id) \
185 if(id == ID_smt_##the_id##_command) \
186 return visitor.visit(static_cast<const smt_##the_id##_commandt &>(command));
187// The include below is marked as nolint because including the same file
188// multiple times is required as part of the x macro pattern.
189#include "smt_commands.def" // NOLINT(build/include)
190#undef COMMAND_ID
192}
193
195{
196 ::accept(*this, id(), visitor);
197}
198
200{
201 ::accept(*this, id(), std::move(visitor));
202}
203
205 const smt_declare_function_commandt &function_declaration)
206 : _identifier(function_declaration.identifier())
207{
208 const auto sort_references = function_declaration.parameter_sorts();
210 make_range(sort_references).collect<decltype(parameter_sorts)>();
211}
212
214 const smt_define_function_commandt &function_definition)
215 : _identifier{function_definition.identifier()}
216{
217 const auto parameters = function_definition.parameters();
219 make_range(parameters)
220 .map([](const smt_termt &term) { return term.get_sort(); })
221 .collect<decltype(parameter_sorts)>();
222}
223
225{
226 return _identifier.identifier();
227}
228
230 const std::vector<smt_termt> &arguments) const
231{
232 return _identifier.get_sort();
233}
234
236 const std::vector<smt_termt> &arguments) const
237{
238 INVARIANT(
239 parameter_sorts.size() == arguments.size(),
240 "Number of parameters and number of arguments must be the same.");
241 const auto parameter_sort_arguments =
242 make_range(parameter_sorts).zip(make_range(arguments));
243 for(const auto &parameter_sort_argument_pair : parameter_sort_arguments)
244 {
245 INVARIANT(
246 parameter_sort_argument_pair.first ==
247 parameter_sort_argument_pair.second.get_sort(),
248 "Sort of argument must have the same sort as the parameter.");
249 }
250}
bool operator==(const irept &other) const
Definition irep.cpp:133
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:67
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:82
subt & get_sub()
Definition irep.h:448
smt_assert_commandt(smt_termt condition)
const smt_termt & condition() const
std::vector< smt_sortt > parameter_sorts
irep_idt identifier() const
smt_command_functiont(const smt_declare_function_commandt &function_declaration)
smt_sortt return_sort(const std::vector< smt_termt > &arguments) const
smt_identifier_termt _identifier
void validate(const std::vector< smt_termt > &arguments) const
void accept(smt_command_const_downcast_visitort &) const
irept(const irep_idt &_id)
Definition irep.h:377
bool operator==(const smt_commandt &) const
bool operator!=(const smt_commandt &) const
smt_commandt()=delete
const smt_identifier_termt & identifier() const
smt_declare_function_commandt(smt_identifier_termt identifier, std::vector< smt_sortt > parameter_sorts)
const smt_sortt & return_sort() const
std::vector< std::reference_wrapper< const smt_sortt > > parameter_sorts() const
const smt_termt & definition() const
const smt_identifier_termt & identifier() const
smt_define_function_commandt(irep_idt identifier, std::vector< smt_identifier_termt > parameters, smt_termt definition)
std::vector< std::reference_wrapper< const smt_identifier_termt > > parameters() const
const smt_sortt & return_sort() const
const smt_termt & descriptor() const
smt_get_value_commandt(smt_termt descriptor)
This constructor constructs the get-value command, such that it stores a single descriptor for which ...
Stores identifiers in unescaped and unquoted form.
Definition smt_terms.h:93
static const smt_logict & downcast(const irept &)
Definition smt_logics.h:59
static irept upcast(smt_logict logic)
Definition smt_logics.h:53
static const smt_optiont & downcast(const irept &)
Definition smt_options.h:59
static irept upcast(smt_optiont option)
Definition smt_options.h:53
size_t levels() const
smt_pop_commandt(std::size_t levels)
size_t levels() const
smt_push_commandt(std::size_t levels)
const smt_logict & logic() const
smt_set_logic_commandt(smt_logict logic)
smt_set_option_commandt(smt_optiont option)
const smt_optiont & option() const
static const smt_sortt & downcast(const irept &)
static irept upcast(smt_termt term)
Definition smt_terms.h:65
static const smt_termt & downcast(const irept &)
Definition smt_terms.h:71
const smt_sortt & get_sort() const
Definition smt_terms.cpp:36
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
dstringt irep_idt