cprover
Loading...
Searching...
No Matches
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
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
93const 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)