15 #define TERM_ID(the_id) \
16 const irep_idt ID_smt_##the_id##_term{"smt_" #the_id "_term"};
17 #include <solvers/smt2_incremental/smt_terms.def>
21 :
irept{id, {{ID_type,
upcast(std::move(sort))}}, {}}
32 return !(*
this == other);
55 static const std::regex valid{
"[^\\|]*"};
56 return std::regex_match(
id2string(identifier), valid);
60 :
smt_termt(ID_smt_identifier_term, std::move(sort))
68 R
"(Identifiers may not contain | characters.)");
74 return get(ID_identifier);
80 :
smt_termt{ID_smt_bit_vector_constant_term, std::move(sort)}
84 "value must fit in number of bits available.");
87 "Negative numbers are not supported by bit vector constants.");
93 std::size_t bit_width)
112 std::vector<smt_termt> arguments)
113 :
smt_termt(ID_smt_function_application_term, function_identifier.get_sort())
117 std::make_move_iterator(
arguments.begin()),
118 std::make_move_iterator(
arguments.end()),
120 [](
smt_termt &&argument) {
return static_cast<irept &&
>(argument); });
129 std::vector<std::reference_wrapper<const smt_termt>>
133 return std::cref(
static_cast<const smt_termt &
>(argument));
137 template <
typename visitort>
140 #define TERM_ID(the_id) \
141 if(id == ID_smt_##the_id##_term) \
142 return visitor.visit(static_cast<const smt_##the_id##_termt &>(term));
145 #include <solvers/smt2_incremental/smt_terms.def>
157 ::accept(*
this,
id(), std::move(visitor));
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
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.
bool get_bool(const irep_idt &name) const
bool operator==(const irept &other) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
const smt_bit_vector_sortt & get_sort() const
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt)
std::size_t bit_width() const
smt_bool_literal_termt(bool value)
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.
static irept upcast(smt_sortt sort)
static const smt_sortt & 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
const std::string & id2string(const irep_idt &d)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Data structure for smt sorts.
void accept(const smt_termt &term, const irep_idt &id, visitort &&visitor)
static bool is_valid_smt_identifier(irep_idt identifier)
#define UNREACHABLE
This should be used to mark dead code.