cprover
Loading...
Searching...
No Matches
smt_terms.h
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
5
6#include <util/irep.h>
7
10
11#include "smt_index.h"
12#include "smt_sorts.h"
13
14#include <functional>
15#include <utility>
16
17class BigInt; // IWYU pragma: keep
18using mp_integer = BigInt;
19
21class smt_termt : protected irept, private smt_sortt::storert<smt_termt>
22{
23public:
24 // smt_termt does not support the notion of an empty / null state. Use
25 // optionalt<smt_termt> instead if an empty term is required.
26 smt_termt() = delete;
27
28 using irept::pretty;
29
30 bool operator==(const smt_termt &) const;
31 bool operator!=(const smt_termt &) const;
32
33 const smt_sortt &get_sort() const;
34
37
43 template <typename derivedt>
44 class storert
45 {
46 protected:
48 static irept upcast(smt_termt term);
49 static const smt_termt &downcast(const irept &);
50 };
51
52protected:
54};
55
56template <typename derivedt>
58{
59 static_assert(
60 std::is_base_of<irept, derivedt>::value &&
61 std::is_base_of<storert<derivedt>, derivedt>::value,
62 "Only irept based classes need to upcast smt_termt to store it.");
63}
64
65template <typename derivedt>
67{
68 return static_cast<irept &&>(std::move(term));
69}
70
71template <typename derivedt>
73{
74 return static_cast<const smt_termt &>(irep);
75}
76
78{
79public:
80 explicit smt_bool_literal_termt(bool value);
81 bool value() const;
82};
83
93 private smt_indext::storert<smt_identifier_termt>
94{
95public:
111 smt_sortt sort,
112 std::vector<smt_indext> indices = {});
113 irep_idt identifier() const;
114 std::vector<std::reference_wrapper<const smt_indext>> indices() const;
115};
116
118{
119public:
121 smt_bit_vector_constant_termt(const mp_integer &value, std::size_t bit_width);
122 mp_integer value() const;
123
124 // This deliberately hides smt_termt::get_sort, because bit_vector terms
125 // always have bit_vector sorts. The same sort data is returned for both
126 // functions either way. Therefore this hiding is benign if the kind of sort
127 // is not important and useful for avoiding casts if the term is a known
128 // smt_bit_vector_constant_termt at compile time and the `bit_width()` is
129 // needed.
130 const smt_bit_vector_sortt &get_sort() const;
131};
132
134{
135private:
141 std::vector<smt_termt> arguments);
142
143 // This is used to detect if \p functiont has an `indicies` member function.
144 // It will resolve to std::true_type if it does or std::false type otherwise.
145 template <class functiont, class = void>
146 struct has_indicest : std::false_type
147 {
148 };
149
150 template <class functiont>
152 functiont,
153 void_t<decltype(std::declval<functiont>().indices())>> : std::true_type
154 {
155 };
156
158 template <class functiont>
159 static std::vector<smt_indext>
160 indices(const functiont &function, const std::false_type &has_indices)
161 {
162 return {};
163 }
164
166 template <class functiont>
167 static std::vector<smt_indext>
168 indices(const functiont &function, const std::true_type &has_indices)
169 {
170 return function.indices();
171 }
172
175 template <class functiont>
176 static std::vector<smt_indext> indices(const functiont &function)
177 {
178 return indices(function, has_indicest<functiont>{});
179 }
180
181public:
183 std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
184
185 template <typename functiont>
187 {
188 private:
190
191 public:
192 template <typename... function_type_argument_typest>
193 explicit factoryt(function_type_argument_typest &&...arguments) noexcept
194 : function{std::forward<function_type_argument_typest>(arguments)...}
195 {
196 }
197
198 template <typename... argument_typest>
200 operator()(argument_typest &&...arguments) const
201 {
202 function.validate(arguments...);
203 auto return_sort = function.return_sort(arguments...);
206 function.identifier(), std::move(return_sort), indices(function)},
207 {std::forward<argument_typest>(arguments)...}};
208 }
209
210 template <typename... argument_typest>
212 validation(argument_typest &&...arguments) const
213 {
214 const auto validation_errors = function.validation_errors(arguments...);
215 if(!validation_errors.empty())
216 return response_or_errort<smt_termt>{validation_errors};
217 auto return_sort = function.return_sort(arguments...);
220 function.identifier(), std::move(return_sort), indices(function)},
221 {std::forward<argument_typest>(arguments)...}}};
222 }
223 };
224};
225
227{
228public:
230 std::vector<smt_identifier_termt> bound_variables,
232 std::vector<std::reference_wrapper<const smt_identifier_termt>>
233 bound_variables() const;
234 const smt_termt &predicate() const;
235};
236
238{
239public:
241 std::vector<smt_identifier_termt> bound_variables,
243 std::vector<std::reference_wrapper<const smt_identifier_termt>>
244 bound_variables() const;
245 const smt_termt &predicate() const;
246};
247
249{
250public:
251#define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
252#include "smt_terms.def"
253#undef TERM_ID
254};
255
256#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:490
Holds either a valid parsed response or response sub-tree of type.
const smt_bit_vector_sortt & get_sort() const
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt)
Definition smt_terms.cpp:95
smt_bool_literal_termt(bool value)
Definition smt_terms.cpp:41
const smt_termt & predicate() const
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
smt_exists_termt(std::vector< smt_identifier_termt > bound_variables, smt_termt predicate)
smt_forall_termt(std::vector< smt_identifier_termt > bound_variables, smt_termt predicate)
const smt_termt & predicate() const
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
factoryt(function_type_argument_typest &&...arguments) noexcept
Definition smt_terms.h:193
response_or_errort< smt_termt > validation(argument_typest &&...arguments) const
Definition smt_terms.h:212
smt_function_application_termt operator()(argument_typest &&...arguments) const
Definition smt_terms.h:200
const smt_identifier_termt & function_identifier() const
smt_function_application_termt(smt_identifier_termt function_identifier, std::vector< smt_termt > arguments)
Unchecked construction of function application terms.
static std::vector< smt_indext > indices(const functiont &function)
Returns function.indices if functiont has an indices member function or returns an empty collection o...
Definition smt_terms.h:176
static std::vector< smt_indext > indices(const functiont &function, const std::true_type &has_indices)
Overload for when functiont has indices member function.
Definition smt_terms.h:168
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
static std::vector< smt_indext > indices(const functiont &function, const std::false_type &has_indices)
Overload for when functiont does not have indices.
Definition smt_terms.h:160
Stores identifiers in unescaped and unquoted form.
Definition smt_terms.h:94
irep_idt identifier() const
Definition smt_terms.cpp:81
smt_identifier_termt(irep_idt identifier, smt_sortt sort, std::vector< smt_indext > indices={})
Constructs an identifier term with the given identifier and sort.
Definition smt_terms.cpp:60
std::vector< std::reference_wrapper< const smt_indext > > indices() const
Definition smt_terms.cpp:87
Class for adding the ability to up and down cast smt_indext to and from irept.
Definition smt_index.h:37
Class for adding the ability to up and down cast smt_sortt to and from irept.
Definition smt_sorts.h:39
Class for adding the ability to up and down cast smt_termt to and from irept.
Definition smt_terms.h:45
static irept upcast(smt_termt term)
Definition smt_terms.h:66
static const smt_termt & downcast(const irept &)
Definition smt_terms.h:72
const smt_sortt & get_sort() const
Definition smt_terms.cpp:36
bool operator==(const smt_termt &) const
Definition smt_terms.cpp:26
void accept(smt_term_const_downcast_visitort &) const
smt_termt()=delete
bool operator!=(const smt_termt &) const
Definition smt_terms.cpp:31
STL namespace.
Data structure for smt sorts.
BigInt mp_integer
Definition smt_terms.h:18
Back ports of utilities available in the <type_traits> library for C++14 or C++17 to C++11.
typename detail::make_voidt< typest... >::type void_t
Definition type_traits.h:35