3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
43 template <
typename derivedt>
56template <
typename derivedt>
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.");
65template <
typename derivedt>
68 return static_cast<irept &&
>(std::move(term));
71template <
typename derivedt>
74 return static_cast<const smt_termt &
>(irep);
112 std::vector<smt_indext>
indices = {});
114 std::vector<std::reference_wrapper<const smt_indext>>
indices()
const;
145 template <
class functiont,
class =
void>
150 template <
class functiont>
158 template <
class functiont>
159 static std::vector<smt_indext>
166 template <
class functiont>
167 static std::vector<smt_indext>
170 return function.indices();
175 template <
class functiont>
183 std::vector<std::reference_wrapper<const smt_termt>>
arguments()
const;
185 template <
typename functiont>
207 {std::forward<argument_typest>(
arguments)...}};
215 if(!validation_errors.empty())
221 {std::forward<argument_typest>(
arguments)...}}};
232 std::vector<std::reference_wrapper<const smt_identifier_termt>>
243 std::vector<std::reference_wrapper<const smt_identifier_termt>>
251#define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
252#include "smt_terms.def"
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const smt_bit_vector_sortt & get_sort() const
const smt_termt & predicate() const
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
const smt_termt & predicate() const
std::vector< std::reference_wrapper< const smt_identifier_termt > > bound_variables() const
factoryt(function_type_argument_typest &&...arguments) noexcept
response_or_errort< smt_termt > validation(argument_typest &&...arguments) const
smt_function_application_termt operator()(argument_typest &&...arguments) const
const smt_identifier_termt & function_identifier() const
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...
static std::vector< smt_indext > indices(const functiont &function, const std::true_type &has_indices)
Overload for when functiont has indices member function.
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.
Stores identifiers in unescaped and unquoted form.
irep_idt identifier() const
std::vector< std::reference_wrapper< const smt_indext > > indices() const
Class for adding the ability to up and down cast smt_indext to and from irept.
Class for adding the ability to up and down cast smt_sortt to and from irept.
Class for adding the ability to up and down cast smt_termt to and from irept.
static irept upcast(smt_termt term)
static const smt_termt & downcast(const irept &)
const smt_sortt & get_sort() const
bool operator==(const smt_termt &) const
void accept(smt_term_const_downcast_visitort &) const
bool operator!=(const smt_termt &) const
Data structure for smt sorts.
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