cprover
|
#include <bv_utils.h>
Public Types | |
enum class | representationt { SIGNED , UNSIGNED } |
enum class | shiftt { SHIFT_LEFT , SHIFT_LRIGHT , SHIFT_ARIGHT , ROTATE_LEFT , ROTATE_RIGHT } |
Public Member Functions | |
bv_utilst (propt &_prop) | |
bvt | incrementer (const bvt &op, literalt carry_in) |
bvt | inc (const bvt &op) |
void | incrementer (bvt &op, literalt carry_in, literalt &carry_out) |
bvt | negate (const bvt &op) |
bvt | negate_no_overflow (const bvt &op) |
bvt | absolute_value (const bvt &op) |
literalt | overflow_negate (const bvt &op) |
literalt | full_adder (const literalt a, const literalt b, const literalt carry_in, literalt &carry_out) |
literalt | carry (literalt a, literalt b, literalt c) |
bvt | add_sub (const bvt &op0, const bvt &op1, bool subtract) |
bvt | add_sub (const bvt &op0, const bvt &op1, literalt subtract) |
bvt | add_sub_no_overflow (const bvt &op0, const bvt &op1, bool subtract, representationt rep) |
bvt | saturating_add_sub (const bvt &op0, const bvt &op1, bool subtract, representationt rep) |
bvt | add (const bvt &op0, const bvt &op1) |
bvt | sub (const bvt &op0, const bvt &op1) |
literalt | overflow_add (const bvt &op0, const bvt &op1, representationt rep) |
literalt | overflow_sub (const bvt &op0, const bvt &op1, representationt rep) |
literalt | carry_out (const bvt &op0, const bvt &op1, literalt carry_in) |
bvt | shift (const bvt &op, const shiftt shift, const bvt &distance) |
bvt | unsigned_multiplier (const bvt &op0, const bvt &op1) |
bvt | signed_multiplier (const bvt &op0, const bvt &op1) |
bvt | multiplier (const bvt &op0, const bvt &op1, representationt rep) |
bvt | multiplier_no_overflow (const bvt &op0, const bvt &op1, representationt rep) |
bvt | divider (const bvt &op0, const bvt &op1, representationt rep) |
bvt | remainder (const bvt &op0, const bvt &op1, representationt rep) |
void | divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem, representationt rep) |
void | signed_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem) |
void | unsigned_divider (const bvt &op0, const bvt &op1, bvt &res, bvt &rem) |
literalt | equal (const bvt &op0, const bvt &op1) |
Bit-blasting ID_equal and use in other encodings. | |
literalt | is_zero (const bvt &op) |
literalt | is_not_zero (const bvt &op) |
literalt | is_int_min (const bvt &op) |
literalt | is_one (const bvt &op) |
literalt | is_all_ones (const bvt &op) |
literalt | lt_or_le (bool or_equal, const bvt &bv0, const bvt &bv1, representationt rep) |
literalt | rel (const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep) |
literalt | unsigned_less_than (const bvt &bv0, const bvt &bv1) |
literalt | signed_less_than (const bvt &bv0, const bvt &bv1) |
void | set_equal (const bvt &a, const bvt &b) |
void | cond_implies_equal (literalt cond, const bvt &a, const bvt &b) |
bvt | cond_negate (const bvt &bv, const literalt cond) |
bvt | select (literalt s, const bvt &a, const bvt &b) |
If s is true, selects a otherwise selects b. | |
literalt | verilog_bv_has_x_or_z (const bvt &) |
Static Public Member Functions | |
static bvt | build_constant (const mp_integer &i, std::size_t width) |
static bvt | inverted (const bvt &op) |
static bvt | shift (const bvt &op, const shiftt shift, std::size_t distance) |
static literalt | sign_bit (const bvt &op) |
static bool | is_constant (const bvt &bv) |
static bvt | extension (const bvt &bv, std::size_t new_size, representationt rep) |
static bvt | sign_extension (const bvt &bv, std::size_t new_size) |
static bvt | zero_extension (const bvt &bv, std::size_t new_size) |
static bvt | zeros (std::size_t new_size) |
static bvt | extract (const bvt &a, std::size_t first, std::size_t last) |
static bvt | extract_msb (const bvt &a, std::size_t n) |
static bvt | extract_lsb (const bvt &a, std::size_t n) |
static bvt | concatenate (const bvt &a, const bvt &b) |
static bvt | verilog_bv_normal_bits (const bvt &) |
Protected Member Functions | |
NODISCARD std::pair< bvt, literalt > | adder (const bvt &op0, const bvt &op1, literalt carry_in) |
Return the sum and carry-out when adding op0 and op1 under initial carry carry_in . | |
NODISCARD bvt | adder_no_overflow (const bvt &op0, const bvt &op1, bool subtract, representationt rep) |
NODISCARD bvt | adder_no_overflow (const bvt &op0, const bvt &op1) |
bvt | unsigned_multiplier_no_overflow (const bvt &op0, const bvt &op1) |
bvt | signed_multiplier_no_overflow (const bvt &op0, const bvt &op1) |
bvt | cond_negate_no_overflow (const bvt &bv, const literalt cond) |
bvt | wallace_tree (const std::vector< bvt > &pps) |
bvt | dadda_tree (const std::vector< bvt > &pps) |
Protected Attributes | |
propt & | prop |
Definition at line 24 of file bv_utils.h.
|
strong |
Enumerator | |
---|---|
SIGNED | |
UNSIGNED |
Definition at line 29 of file bv_utils.h.
|
strong |
Enumerator | |
---|---|
SHIFT_LEFT | |
SHIFT_LRIGHT | |
SHIFT_ARIGHT | |
ROTATE_LEFT | |
ROTATE_RIGHT |
Definition at line 74 of file bv_utils.h.
|
inlineexplicit |
Definition at line 27 of file bv_utils.h.
Definition at line 1033 of file bv_utils.cpp.
Definition at line 67 of file bv_utils.h.
Definition at line 336 of file bv_utils.cpp.
Definition at line 348 of file bv_utils.cpp.
bvt bv_utilst::add_sub_no_overflow | ( | const bvt & | op0, |
const bvt & | op1, | ||
bool | subtract, | ||
representationt | rep ) |
Definition at line 327 of file bv_utils.cpp.
|
protected |
Return the sum and carry-out when adding op0
and op1
under initial carry carry_in
.
Definition at line 296 of file bv_utils.cpp.
Definition at line 510 of file bv_utils.cpp.
|
protected |
Definition at line 475 of file bv_utils.cpp.
|
static |
Definition at line 13 of file bv_utils.cpp.
Definition at line 229 of file bv_utils.cpp.
Definition at line 312 of file bv_utils.cpp.
Definition at line 78 of file bv_utils.cpp.
Definition at line 1589 of file bv_utils.cpp.
Definition at line 1020 of file bv_utils.cpp.
Definition at line 1039 of file bv_utils.cpp.
Definition at line 691 of file bv_utils.cpp.
void bv_utilst::divider | ( | const bvt & | op0, |
const bvt & | op1, | ||
bvt & | res, | ||
bvt & | rem, | ||
representationt | rep ) |
Definition at line 1133 of file bv_utils.cpp.
|
inline |
Definition at line 90 of file bv_utils.h.
Bit-blasting ID_equal and use in other encodings.
op0 | Lhs bitvector to compare |
op1 | Rhs bitvector to compare |
Definition at line 1363 of file bv_utils.cpp.
|
static |
Definition at line 107 of file bv_utils.cpp.
Definition at line 40 of file bv_utils.cpp.
Definition at line 68 of file bv_utils.cpp.
Definition at line 56 of file bv_utils.cpp.
literalt bv_utilst::full_adder | ( | const literalt | a, |
const literalt | b, | ||
const literalt | carry_in, | ||
literalt & | carry_out ) |
Definition at line 138 of file bv_utils.cpp.
Definition at line 34 of file bv_utils.h.
Definition at line 613 of file bv_utils.cpp.
Definition at line 628 of file bv_utils.cpp.
Definition at line 636 of file bv_utils.cpp.
Definition at line 159 of file bv_utils.h.
|
static |
Definition at line 1578 of file bv_utils.cpp.
Definition at line 150 of file bv_utils.h.
Definition at line 147 of file bv_utils.h.
Definition at line 24 of file bv_utils.cpp.
Definition at line 144 of file bv_utils.h.
literalt bv_utilst::lt_or_le | ( | bool | or_equal, |
const bvt & | bv0, | ||
const bvt & | bv1, | ||
representationt | rep ) |
Definition at line 1398 of file bv_utils.cpp.
bvt bv_utilst::multiplier | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep ) |
Definition at line 1068 of file bv_utils.cpp.
bvt bv_utilst::multiplier_no_overflow | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep ) |
Definition at line 1082 of file bv_utils.cpp.
Definition at line 588 of file bv_utils.cpp.
Definition at line 596 of file bv_utils.cpp.
literalt bv_utilst::overflow_add | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep ) |
Definition at line 426 of file bv_utils.cpp.
Definition at line 602 of file bv_utils.cpp.
literalt bv_utilst::overflow_sub | ( | const bvt & | op0, |
const bvt & | op1, | ||
representationt | rep ) |
Definition at line 450 of file bv_utils.cpp.
literalt bv_utilst::rel | ( | const bvt & | bv0, |
irep_idt | id, | ||
const bvt & | bv1, | ||
representationt | rep ) |
Definition at line 1556 of file bv_utils.cpp.
|
inline |
Definition at line 97 of file bv_utils.h.
bvt bv_utilst::saturating_add_sub | ( | const bvt & | op0, |
const bvt & | op1, | ||
bool | subtract, | ||
representationt | rep ) |
Definition at line 357 of file bv_utils.cpp.
If s is true, selects a otherwise selects b.
Definition at line 94 of file bv_utils.cpp.
Definition at line 33 of file bv_utils.cpp.
Definition at line 515 of file bv_utils.cpp.
Definition at line 536 of file bv_utils.cpp.
Definition at line 139 of file bv_utils.h.
Definition at line 183 of file bv_utils.h.
Definition at line 1098 of file bv_utils.cpp.
Definition at line 1549 of file bv_utils.cpp.
Definition at line 1002 of file bv_utils.cpp.
Definition at line 1046 of file bv_utils.cpp.
Definition at line 68 of file bv_utils.h.
Definition at line 1151 of file bv_utils.cpp.
Definition at line 1537 of file bv_utils.cpp.
Definition at line 918 of file bv_utils.cpp.
Definition at line 963 of file bv_utils.cpp.
Definition at line 1612 of file bv_utils.cpp.
Definition at line 1627 of file bv_utils.cpp.
Definition at line 644 of file bv_utils.cpp.
Definition at line 188 of file bv_utils.h.
|
inlinestatic |
Definition at line 193 of file bv_utils.h.
|
protected |
Definition at line 223 of file bv_utils.h.