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
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
41
43 smt_identifier_termt identifier,
44 std::vector<smt_sortt> parameter_sorts)
46{
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()),
53 return sort_storert::upcast(std::move(parameter_sort));
54 });
55}
56
62
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
79
81 irep_idt identifier,
82 std::vector<smt_identifier_termt> parameters,
83 smt_termt definition)
85{
86 set(
89 std::transform(
90 std::make_move_iterator(parameters.begin()),
91 std::make_move_iterator(parameters.end()),
92 std::back_inserter(get_sub()),
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 &>(
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
118
123
129
134
140
142{
143 return get_size_t(ID_value);
144}
145
151
153{
154 return get_size_t(ID_value);
155}
156
162
164{
165 return downcast(find(ID_value));
166}
167
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
196
198{
199 ::accept(*this, id(), std::move(visitor));
200}
201
210
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
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));
242 {
243 INVARIANT(
245 parameter_sort_argument_pair.second.get_sort(),
246 "Sort of argument must have the same sort as the parameter.");
247 }
248}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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