cprover
smt_bit_vector_theory.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
5 #include <util/invariant.h>
6 
8  const smt_termt &left,
9  const smt_termt &right)
10 {
11  const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
12  INVARIANT(left_sort, "Left operand must have bitvector sort.");
13  const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
14  INVARIANT(right_sort, "Right operand must have bitvector sort.");
15  // The below invariant is based on the smtlib standard.
16  // See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
17  INVARIANT(
18  left_sort->bit_width() == right_sort->bit_width(),
19  "Left and right operands must have the same bit width.");
20 }
21 
22 // Relational operator definitions
23 
25 {
26  return "bvult";
27 }
28 
30  const smt_termt &lhs,
31  const smt_termt &rhs)
32 {
33  return smt_bool_sortt{};
34 }
35 
37  const smt_termt &lhs,
38  const smt_termt &rhs)
39 {
41 }
42 
46 
48 {
49  return "bvule";
50 }
51 
53  const smt_termt &lhs,
54  const smt_termt &rhs)
55 {
56  return smt_bool_sortt{};
57 }
58 
60  const smt_termt &lhs,
61  const smt_termt &rhs)
62 {
64 }
65 
69 
71 {
72  return "bvugt";
73 }
74 
76  const smt_termt &lhs,
77  const smt_termt &rhs)
78 {
79  return smt_bool_sortt{};
80 }
81 
83  const smt_termt &lhs,
84  const smt_termt &rhs)
85 {
87 }
88 
92 
93 const char *
95 {
96  return "bvuge";
97 }
98 
100  const smt_termt &lhs,
101  const smt_termt &rhs)
102 {
103  return smt_bool_sortt{};
104 }
105 
107  const smt_termt &lhs,
108  const smt_termt &rhs)
109 {
111 }
112 
116 
118 {
119  return "bvslt";
120 }
121 
123  const smt_termt &lhs,
124  const smt_termt &rhs)
125 {
126  return smt_bool_sortt{};
127 }
128 
130  const smt_termt &lhs,
131  const smt_termt &rhs)
132 {
134 }
135 
139 
141 {
142  return "bvsle";
143 }
144 
146  const smt_termt &lhs,
147  const smt_termt &rhs)
148 {
149  return smt_bool_sortt{};
150 }
151 
153  const smt_termt &lhs,
154  const smt_termt &rhs)
155 {
157 }
158 
162 
164 {
165  return "bvsgt";
166 }
167 
169  const smt_termt &lhs,
170  const smt_termt &rhs)
171 {
172  return smt_bool_sortt{};
173 }
174 
176  const smt_termt &lhs,
177  const smt_termt &rhs)
178 {
180 }
181 
185 
187 {
188  return "bvsge";
189 }
190 
192  const smt_termt &lhs,
193  const smt_termt &rhs)
194 {
195  return smt_bool_sortt{};
196 }
197 
199  const smt_termt &lhs,
200  const smt_termt &rhs)
201 {
203 }
204 
208 
210 {
211  return "bvadd";
212 }
213 
215  const smt_termt &lhs,
216  const smt_termt &rhs)
217 {
218  return lhs.get_sort();
219 }
220 
222  const smt_termt &lhs,
223  const smt_termt &rhs)
224 {
226 }
227 
230 
232 {
233  return "bvsub";
234 }
235 
237  const smt_termt &lhs,
238  const smt_termt &rhs)
239 {
240  return lhs.get_sort();
241 }
242 
244  const smt_termt &lhs,
245  const smt_termt &rhs)
246 {
248 }
249 
253 
255 {
256  return "bvmul";
257 }
258 
260  const smt_termt &lhs,
261  const smt_termt &rhs)
262 {
263  return lhs.get_sort();
264 }
265 
267  const smt_termt &lhs,
268  const smt_termt &rhs)
269 {
271 }
272 
276 
278 {
279  return "bvudiv";
280 }
281 
283  const smt_termt &lhs,
284  const smt_termt &rhs)
285 {
286  return lhs.get_sort();
287 }
288 
290  const smt_termt &lhs,
291  const smt_termt &rhs)
292 {
294 }
295 
299 
301 {
302  return "bvsdiv";
303 }
304 
306  const smt_termt &lhs,
307  const smt_termt &rhs)
308 {
309  return lhs.get_sort();
310 }
311 
313  const smt_termt &lhs,
314  const smt_termt &rhs)
315 {
317 }
318 
322 
324 {
325  return "bvurem";
326 }
327 
329  const smt_termt &lhs,
330  const smt_termt &rhs)
331 {
332  return lhs.get_sort();
333 }
334 
336  const smt_termt &lhs,
337  const smt_termt &rhs)
338 {
340 }
341 
345 
347 {
348  return "bvsrem";
349 }
350 
352  const smt_termt &lhs,
353  const smt_termt &rhs)
354 {
355  return lhs.get_sort();
356 }
357 
359  const smt_termt &lhs,
360  const smt_termt &rhs)
361 {
363 }
364 
368 
370 {
371  return "bvneg";
372 }
373 
375 {
376  return operand.get_sort();
377 }
378 
380 {
381  const auto operand_sort = operand.get_sort().cast<smt_bit_vector_sortt>();
382  INVARIANT(operand_sort, "The operand is expected to have a bit-vector sort.");
383 }
384 
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal
static const smt_function_application_termt::factoryt< addt > add
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal
static const smt_function_application_termt::factoryt< multiplyt > multiply
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< negatet > negate
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide
static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder
static const smt_function_application_termt::factoryt< subtractt > subtract
const sub_classt * cast() const &
const smt_sortt & get_sort() const
Definition: smt_terms.cpp:35
static void validate_bit_vector_operator_arguments(const smt_termt &left, const smt_termt &right)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &operand)
static smt_sortt return_sort(const smt_termt &operand)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)