3#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
4#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TERMS_H
37 template <
typename derivedt>
50template <
typename derivedt>
54 std::is_base_of<irept, derivedt>::value &&
55 std::is_base_of<storert<derivedt>, derivedt>::value,
56 "Only irept based classes need to upcast smt_termt to store it.");
59template <
typename derivedt>
62 return static_cast<irept &&
>(std::move(term));
65template <
typename derivedt>
68 return static_cast<const smt_termt &
>(irep);
126 std::vector<std::reference_wrapper<const smt_termt>>
arguments()
const;
128 template <
typename functiont>
135 template <
typename... function_type_argument_typest>
141 template <
typename... argument_typest>
149 {std::forward<argument_typest>(
arguments)...}};
157#define TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0;
158#include "smt_terms.def"
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
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt)
smt_bool_literal_termt(bool value)
smt_function_application_termt operator()(argument_typest &&... arguments) const
factoryt(function_type_argument_typest &&... arguments)
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.
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Stores identifiers in unescaped and unquoted form.
irep_idt identifier() const
smt_identifier_termt(irep_idt identifier, smt_sortt sort)
Constructs an identifier term with the given identifier and sort.
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.