cprover
Loading...
Searching...
No Matches
smt_terms.cpp
Go to the documentation of this file.
1// Author: Diffblue Ltd.
2
4
6
7#include <util/arith_tools.h>
8#include <util/mp_arith.h>
9#include <util/range.h>
10
11#include <algorithm>
12#include <regex>
13
14// Define the irep_idts for terms.
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>
18#undef TERM_ID
19
21 : irept{id, {{ID_type, upcast(std::move(sort))}}, {}}
22{
23}
24
25bool smt_termt::operator==(const smt_termt &other) const
26{
27 return irept::operator==(other);
28}
29
30bool smt_termt::operator!=(const smt_termt &other) const
31{
32 return !(*this == other);
33}
34
36{
37 return downcast(find(ID_type));
38}
39
45
47{
48 return get_bool(ID_value);
49}
50
51static bool is_valid_smt_identifier(irep_idt identifier)
52{
53 // The below regex matches a complete string which does not contain the `|`
54 // character. So it would match the string `foo bar`, but not `|foo bar|`.
55 static const std::regex valid{"[^\\|]*"};
56 return std::regex_match(id2string(identifier), valid);
57}
58
61{
62 // The below invariant exists as a sanity check that the string being used for
63 // the identifier is in unescaped form. This is because the escaping and
64 // unescaping are implementation details of the printing to string and
65 // response parsing respectively, not part of the underlying data.
68 R"(Identifiers may not contain | characters.)");
70}
71
76
78 const mp_integer &value,
81{
84 "value must fit in number of bits available.");
86 !value.is_negative(),
87 "Negative numbers are not supported by bit vector constants.");
88 set(ID_value, integer2bvrep(value, get_sort().bit_width()));
89}
90
97
99{
100 return bvrep2integer(get(ID_value), get_sort().bit_width(), false);
101}
102
104{
105 // The below cast is sound because the constructor only allows bit_vector
106 // sorts to be set.
107 return static_cast<const smt_bit_vector_sortt &>(smt_termt::get_sort());
108}
109
111 smt_identifier_termt function_identifier,
112 std::vector<smt_termt> arguments)
113 : smt_termt(ID_smt_function_application_term, function_identifier.get_sort())
114{
116 std::transform(
117 std::make_move_iterator(arguments.begin()),
118 std::make_move_iterator(arguments.end()),
119 std::back_inserter(get_sub()),
120 [](smt_termt &&argument) { return static_cast<irept &&>(argument); });
121}
122
128
129std::vector<std::reference_wrapper<const smt_termt>>
131{
132 return make_range(get_sub()).map([](const irept &argument) {
133 return std::cref(static_cast<const smt_termt &>(argument));
134 });
135}
136
137template <typename visitort>
138void accept(const smt_termt &term, const irep_idt &id, visitort &&visitor)
139{
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));
143// The include below is marked as nolint because including the same file
144// multiple times is required as part of the x macro pattern.
145#include <solvers/smt2_incremental/smt_terms.def> // NOLINT(build/include)
146#undef TERM_ID
148}
149
154
156{
157 ::accept(*this, id(), std::move(visitor));
158}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
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 get_bool(const irep_idt &name) const
Definition irep.cpp:58
bool operator==(const irept &other) const
Definition irep.cpp:146
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
subt & get_sub()
Definition irep.h:456
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:77
mp_integer value() const
Definition smt_terms.cpp:98
std::size_t bit_width() const
Definition smt_sorts.cpp:60
smt_bool_literal_termt(bool value)
Definition smt_terms.cpp:40
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.
Definition smt_terms.h:81
irep_idt identifier() const
Definition smt_terms.cpp:72
smt_identifier_termt(irep_idt identifier, smt_sortt sort)
Constructs an identifier term with the given identifier and sort.
Definition smt_terms.cpp:59
static irept upcast(smt_sortt sort)
Definition smt_sorts.h:66
static const smt_sortt & downcast(const irept &)
Definition smt_sorts.h:72
const smt_sortt & get_sort() const
Definition smt_terms.cpp:35
bool operator==(const smt_termt &) const
Definition smt_terms.cpp:25
void accept(smt_term_const_downcast_visitort &) const
smt_termt()=delete
bool operator!=(const smt_termt &) const
Definition smt_terms.cpp:30
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
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
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)
Definition smt_terms.cpp:51
#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