cprover
smt_responses.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
5 #include <util/range.h>
6 
7 // Define the irep_idts for responses.
8 #define RESPONSE_ID(the_id, the_base) \
9  const irep_idt ID_smt_##the_id##_response{"smt_" #the_id "_response"};
10 #include <solvers/smt2_incremental/smt_responses.def>
11 #undef RESPONSE_ID
12 
13 bool smt_responset::operator==(const smt_responset &other) const
14 {
15  return irept::operator==(other);
16 }
17 
18 bool smt_responset::operator!=(const smt_responset &other) const
19 {
20  return !(*this == other);
21 }
22 
23 #define RESPONSE_ID(the_id, the_base) \
24  template <> \
25  const smt_##the_id##_responset *the_base::cast<smt_##the_id##_responset>() \
26  const & \
27  { \
28  return id() == ID_smt_##the_id##_response \
29  ? static_cast<const smt_##the_id##_responset *>(this) \
30  : nullptr; \
31  }
32 #include <solvers/smt2_incremental/smt_responses.def> // NOLINT(build/include)
33 #undef RESPONSE_ID
34 
35 template <typename sub_classt>
36 const sub_classt *smt_responset::cast() const &
37 {
38  return nullptr;
39 }
40 
42 operator==(const smt_check_sat_response_kindt &other) const
43 {
44  return irept::operator==(other);
45 }
46 
48 operator!=(const smt_check_sat_response_kindt &other) const
49 {
50  return !(*this == other);
51 }
52 
54  : smt_responset{ID_smt_success_response}
55 {
56 }
57 
59  : smt_check_sat_response_kindt{ID_smt_sat_response}
60 {
61 }
62 
64  : smt_check_sat_response_kindt{ID_smt_unsat_response}
65 {
66 }
67 
69  : smt_check_sat_response_kindt{ID_smt_unknown_response}
70 {
71 }
72 
73 template <typename derivedt>
75 {
76  static_assert(
77  std::is_base_of<irept, derivedt>::value &&
78  std::is_base_of<storert<derivedt>, derivedt>::value,
79  "Only irept based classes need to upcast smt_termt to store it.");
80 }
81 
82 template <typename derivedt>
84  smt_check_sat_response_kindt check_sat_response_kind)
85 {
86  return static_cast<irept &&>(std::move(check_sat_response_kind));
87 }
88 
89 template <typename derivedt>
92 {
93  return static_cast<const smt_check_sat_response_kindt &>(irep);
94 }
95 
98  : smt_responset{ID_smt_check_sat_response}
99 {
100  set(ID_value, upcast(std::move(kind)));
101 }
102 
104 {
105  return downcast(find(ID_value));
106 }
107 
109  smt_termt descriptor,
110  smt_termt value)
111 {
112  INVARIANT(
114  "SMT valuation pair must have matching sort for the descriptor and value.");
115  get_sub().push_back(upcast(std::move(descriptor)));
116  get_sub().push_back(upcast(std::move(value)));
117 }
118 
120  irep_idt descriptor,
121  const smt_termt &value)
122  : valuation_pairt(smt_identifier_termt{descriptor, value.get_sort()}, value)
123 {
124 }
125 
127 {
128  return downcast(get_sub().at(0));
129 }
130 
132 {
133  return downcast(get_sub().at(1));
134 }
135 
138 {
139  return irept::operator==(other);
140 }
141 
144 {
145  return !(*this == other);
146 }
147 
149  std::vector<valuation_pairt> pairs)
150  : smt_responset(ID_smt_get_value_response)
151 {
152  // SMT-LIB standard version 2.6 requires one or more pairs.
153  // See page 47, figure 3.9: Command responses.
154  INVARIANT(
155  !pairs.empty(), "Get value response must contain one or more pairs.");
156  for(auto &pair : pairs)
157  {
158  get_sub().push_back(std::move(pair));
159  }
160 }
161 
162 std::vector<
163  std::reference_wrapper<const smt_get_value_responset::valuation_pairt>>
165 {
166  return make_range(get_sub()).map([](const irept &pair) {
167  return std::cref(static_cast<const valuation_pairt &>(pair));
168  });
169 }
170 
172  : smt_responset{ID_smt_unsupported_response}
173 {
174 }
175 
177  : smt_responset{ID_smt_error_response}
178 {
179  set(ID_value, message);
180 }
181 
183 {
184  return get(ID_value);
185 }
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 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
Class for adding the ability to up and down cast smt_check_sat_response_kindt to and from irept.
Definition: smt_responses.h:57
static irept upcast(smt_check_sat_response_kindt check_sat_response_kind)
static const smt_check_sat_response_kindt & downcast(const irept &)
bool operator==(const smt_check_sat_response_kindt &) const
bool operator!=(const smt_check_sat_response_kindt &) const
smt_check_sat_responset(smt_check_sat_response_kindt kind)
const smt_check_sat_response_kindt & kind() const
const irep_idt & message() const
smt_error_responset(irep_idt message)
bool operator==(const valuation_pairt &) const
bool operator!=(const valuation_pairt &) const
smt_get_value_responset(std::vector< valuation_pairt > pairs)
std::vector< std::reference_wrapper< const valuation_pairt > > pairs() const
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
const sub_classt * cast() const &
bool operator!=(const smt_responset &) const
bool operator==(const smt_responset &) const
static irept upcast(smt_termt term)
Definition: smt_terms.h:60
static const smt_termt & downcast(const irept &)
Definition: smt_terms.h:66
const smt_sortt & get_sort() const
Definition: smt_terms.cpp:35
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