cprover
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 
25 bool smt_termt::operator==(const smt_termt &other) const
26 {
27  return irept::operator==(other);
28 }
29 
30 bool smt_termt::operator!=(const smt_termt &other) const
31 {
32  return !(*this == other);
33 }
34 
36 {
37  return downcast(find(ID_type));
38 }
39 
41  : smt_termt{ID_smt_bool_literal_term, smt_bool_sortt{}}
42 {
43  set(ID_value, value);
44 }
45 
47 {
48  return get_bool(ID_value);
49 }
50 
51 static 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 
60  : smt_termt(ID_smt_identifier_term, std::move(sort))
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.
66  INVARIANT(
68  R"(Identifiers may not contain | characters.)");
69  set(ID_identifier, identifier);
70 }
71 
73 {
74  return get(ID_identifier);
75 }
76 
78  const mp_integer &value,
80  : smt_termt{ID_smt_bit_vector_constant_term, std::move(sort)}
81 {
82  INVARIANT(
84  "value must fit in number of bits available.");
85  INVARIANT(
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 
92  const mp_integer &value,
93  std::size_t bit_width)
95 {
96 }
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 {
115  set(ID_identifier, std::move(function_identifier));
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 
123 const smt_identifier_termt &
125 {
126  return static_cast<const smt_identifier_termt &>(find(ID_identifier));
127 }
128 
129 std::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 
137 template <typename visitort>
138 void 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
147  UNREACHABLE;
148 }
149 
151 {
152  ::accept(*this, id(), visitor);
153 }
154 
156 {
157  ::accept(*this, id(), std::move(visitor));
158 }
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
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.
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
subt & get_sub()
Definition: irep.h:456
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
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:103
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
bool value() const
Definition: smt_terms.cpp:46
const smt_identifier_termt & function_identifier() const
Definition: smt_terms.cpp:124
smt_function_application_termt(smt_identifier_termt function_identifier, std::vector< smt_termt > arguments)
Unchecked construction of function application terms.
Definition: smt_terms.cpp:110
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:130
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
Definition: smt_terms.cpp:150
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
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)
Definition: smt_terms.cpp:138
static bool is_valid_smt_identifier(irep_idt identifier)
Definition: smt_terms.cpp:51
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503