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
35
42
46
51
58
65
69
71{
72 return "bvugt";
73}
74
81
88
92
93const char *
98
105
112
116
118{
119 return "bvslt";
120}
121
128
135
139
141{
142 return "bvsle";
143}
144
151
158
162
164{
165 return "bvsgt";
166}
167
174
181
185
190
197
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
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
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
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
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
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
364
368
370{
371 return "bvneg";
372}
373
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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)