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  static const std::regex valid{R"(^[^\|\\]*$)"};
54  return std::regex_match(id2string(identifier), valid);
55 }
56 
58  : smt_termt(ID_smt_identifier_term, std::move(sort))
59 {
60  INVARIANT(
62  R"(Identifiers may not contain | or \ characters.)");
63  set(ID_identifier, identifier);
64 }
65 
67 {
68  return get(ID_identifier);
69 }
70 
72  const mp_integer &value,
74  : smt_termt{ID_smt_bit_vector_constant_term, std::move(sort)}
75 {
76  INVARIANT(
78  "value must fit in number of bits available.");
79  INVARIANT(
80  !value.is_negative(),
81  "Negative numbers are not supported by bit vector constants.");
82  set(ID_value, integer2bvrep(value, get_sort().bit_width()));
83 }
84 
86  const mp_integer &value,
87  std::size_t bit_width)
89 {
90 }
91 
93 {
94  return bvrep2integer(get(ID_value), get_sort().bit_width(), false);
95 }
96 
98 {
99  // The below cast is sound because the constructor only allows bit_vector
100  // sorts to be set.
101  return static_cast<const smt_bit_vector_sortt &>(smt_termt::get_sort());
102 }
103 
105  smt_identifier_termt function_identifier,
106  std::vector<smt_termt> arguments)
107  : smt_termt(ID_smt_function_application_term, function_identifier.get_sort())
108 {
109  set(ID_identifier, std::move(function_identifier));
111  std::make_move_iterator(arguments.begin()),
112  std::make_move_iterator(arguments.end()),
113  std::back_inserter(get_sub()),
114  [](smt_termt &&argument) { return static_cast<irept &&>(argument); });
115 }
116 
117 const smt_identifier_termt &
119 {
120  return static_cast<const smt_identifier_termt &>(find(ID_identifier));
121 }
122 
123 std::vector<std::reference_wrapper<const smt_termt>>
125 {
126  return make_range(get_sub()).map([](const irept &argument) {
127  return std::cref(static_cast<const smt_termt &>(argument));
128  });
129 }
130 
131 template <typename visitort>
132 void accept(const smt_termt &term, const irep_idt &id, visitort &&visitor)
133 {
134 #define TERM_ID(the_id) \
135  if(id == ID_smt_##the_id##_term) \
136  return visitor.visit(static_cast<const smt_##the_id##_termt &>(term));
137 // The include below is marked as nolint because including the same file
138 // multiple times is required as part of the x macro pattern.
139 #include <solvers/smt2_incremental/smt_terms.def> // NOLINT(build/include)
140 #undef TERM_ID
141  UNREACHABLE;
142 }
143 
145 {
146  ::accept(*this, id(), visitor);
147 }
148 
150 {
151  ::accept(*this, id(), std::move(visitor));
152 }
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:383
bool operator==(const irept &other) const
Definition: irep.cpp:146
subt & get_sub()
Definition: irep.h:467
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
const smt_bit_vector_sortt & get_sort() const
Definition: smt_terms.cpp:97
smt_bit_vector_constant_termt(const mp_integer &value, smt_bit_vector_sortt)
Definition: smt_terms.cpp:71
mp_integer value() const
Definition: smt_terms.cpp:92
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:118
smt_function_application_termt(smt_identifier_termt function_identifier, std::vector< smt_termt > arguments)
Unchecked construction of function application terms.
Definition: smt_terms.cpp:104
std::vector< std::reference_wrapper< const smt_termt > > arguments() const
Definition: smt_terms.cpp:124
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
irep_idt identifier() const
Definition: smt_terms.cpp:66
smt_identifier_termt(irep_idt identifier, smt_sortt sort)
Constructs an identifier term with the given identifier and sort.
Definition: smt_terms.cpp:57
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:144
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:49
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:132
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