cprover
Loading...
Searching...
No Matches
smt_commands.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 commands.
8#define COMMAND_ID(the_id) \
9 const irep_idt ID_smt_##the_id##_command{"smt_" #the_id "_command"};
10#include <solvers/smt2_incremental/smt_commands.def>
11#undef COMMAND_ID
12
13bool smt_commandt::operator==(const smt_commandt &other) const
14{
15 return irept::operator==(other);
16}
17
18bool smt_commandt::operator!=(const smt_commandt &other) const
19{
20 return !(*this == other);
21}
22
24 : smt_commandt{ID_smt_assert_command}
25{
28 "Only terms with boolean sorts can be asserted.");
29 set(ID_cond, upcast(std::move(condition)));
30}
31
33{
34 return downcast(find(ID_cond));
35}
36
38 : smt_commandt{ID_smt_check_sat_command}
39{
40}
41
43 smt_identifier_termt identifier,
44 std::vector<smt_sortt> parameter_sorts)
45 : smt_commandt{ID_smt_declare_function_command}
46{
47 set(ID_identifier, term_storert::upcast(std::move(identifier)));
48 std::transform(
49 std::make_move_iterator(parameter_sorts.begin()),
50 std::make_move_iterator(parameter_sorts.end()),
51 std::back_inserter(get_sub()),
52 [](smt_sortt &&parameter_sort) {
53 return sort_storert::upcast(std::move(parameter_sort));
54 });
55}
56
58{
59 return static_cast<const smt_identifier_termt &>(
60 term_storert::downcast(find(ID_identifier)));
61}
62
64{
65 return identifier().get_sort();
66}
67
68std::vector<std::reference_wrapper<const smt_sortt>>
70{
71 return make_range(get_sub()).map([](const irept &parameter_sort) {
72 return std::cref(sort_storert::downcast(parameter_sort));
73 });
74}
75
77{
78}
79
81 irep_idt identifier,
82 std::vector<smt_identifier_termt> parameters,
83 smt_termt definition)
84 : smt_commandt{ID_smt_define_function_command}
85{
86 set(
87 ID_identifier,
89 std::transform(
90 std::make_move_iterator(parameters.begin()),
91 std::make_move_iterator(parameters.end()),
92 std::back_inserter(get_sub()),
93 [](smt_identifier_termt &&parameter) {
94 return upcast(std::move(parameter));
95 });
96 set(ID_code, upcast(std::move(definition)));
97}
98
100{
101 return static_cast<const smt_identifier_termt &>(
102 downcast(find(ID_identifier)));
103}
104
105std::vector<std::reference_wrapper<const smt_identifier_termt>>
107{
108 return make_range(get_sub()).map([](const irept &parameter) {
109 return std::cref(
110 static_cast<const smt_identifier_termt &>(downcast((parameter))));
111 });
112}
113
115{
116 return definition().get_sort();
117}
118
120{
121 return downcast(find(ID_code));
122}
123
125 : smt_commandt{ID_smt_get_value_command}
126{
127 set(ID_value, upcast(std::move(descriptor)));
128}
129
131{
132 return downcast(find(ID_value));
133}
134
136 : smt_commandt(ID_smt_push_command)
137{
138 set_size_t(ID_value, levels);
139}
140
142{
143 return get_size_t(ID_value);
144}
145
147 : smt_commandt(ID_smt_pop_command)
148{
149 set_size_t(ID_value, levels);
150}
151
153{
154 return get_size_t(ID_value);
155}
156
158 : smt_commandt(ID_smt_set_logic_command)
159{
160 set(ID_value, upcast(std::move(logic)));
161}
162
164{
165 return downcast(find(ID_value));
166}
167
169 : smt_commandt(ID_smt_set_option_command)
170{
171 set(ID_value, upcast(std::move(option)));
172}
173
175{
176 return downcast(find(ID_value));
177}
178
179template <typename visitort>
180void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
181{
182#define COMMAND_ID(the_id) \
183 if(id == ID_smt_##the_id##_command) \
184 return visitor.visit(static_cast<const smt_##the_id##_commandt &>(command));
185// The include below is marked as nolint because including the same file
186// multiple times is required as part of the x macro pattern.
187#include <solvers/smt2_incremental/smt_commands.def> // NOLINT(build/include)
188#undef COMMAND_ID
190}
191
193{
194 ::accept(*this, id(), visitor);
195}
196
198{
199 ::accept(*this, id(), std::move(visitor));
200}
201
203 const smt_declare_function_commandt &function_declaration)
204 : _identifier(function_declaration.identifier())
205{
206 const auto sort_references = function_declaration.parameter_sorts();
208 make_range(sort_references).collect<decltype(parameter_sorts)>();
209}
210
212 const smt_define_function_commandt &function_definition)
213 : _identifier{function_definition.identifier()}
214{
215 const auto parameters = function_definition.parameters();
217 make_range(parameters)
218 .map([](const smt_termt &term) { return term.get_sort(); })
219 .collect<decltype(parameter_sorts)>();
220}
221
223{
224 return _identifier.identifier();
225}
226
228 const std::vector<smt_termt> &arguments) const
229{
230 return _identifier.get_sort();
231}
232
234 const std::vector<smt_termt> &arguments) const
235{
236 INVARIANT(
237 parameter_sorts.size() == arguments.size(),
238 "Number of parameters and number of arguments must be the same.");
239 const auto parameter_sort_arguments =
240 make_range(parameter_sorts).zip(make_range(arguments));
241 for(const auto &parameter_sort_argument_pair : parameter_sort_arguments)
242 {
243 INVARIANT(
244 parameter_sort_argument_pair.first ==
245 parameter_sort_argument_pair.second.get_sort(),
246 "Sort of argument must have the same sort as the parameter.");
247 }
248}
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
std::size_t get_size_t(const irep_idt &name) const
Definition irep.cpp:68
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
void set_size_t(const irep_idt &name, const std::size_t value)
Definition irep.cpp:87
subt & get_sub()
Definition irep.h:456
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
bool operator==(const smt_commandt &) const
bool operator!=(const smt_commandt &) const
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:81
irep_idt identifier() const
Definition smt_terms.cpp:72
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 &)
Definition smt_sorts.h:72
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
void accept(const smt_commandt &command, const irep_idt &id, visitort &&visitor)
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423