- Generated by
1.9.8
|
SMTStabilizer API
Public API documentation for SMTStabilizer
|
#include <bitvector.h>
Static Public Member Functions | |
| static bool | fits_in_size (uint64_t size, const std::string &str, uint32_t base) |
| static bool | fits_in_size (uint64_t size, uint64_t value, bool sign=false) |
| static bool | fits_in_size (uint64_t size, const mpz_t value) |
| static BitVector | from_ui (uint64_t size, uint64_t value, bool truncate=false) |
| static BitVector | from_si (uint64_t size, int64_t value, bool truncate=false) |
| static BitVector | mk_true () |
| static BitVector | mk_false () |
| static BitVector | mk_zero (uint64_t size) |
| static BitVector | mk_one (uint64_t size) |
| static BitVector | mk_ones (uint64_t size) |
| static BitVector | mk_min_signed (uint64_t size) |
| static BitVector | mk_max_signed (uint64_t size) |
| static BitVector | bvite (const BitVector &c, const BitVector &t, const BitVector &e) |
Static Public Attributes | |
| static constexpr size_t | s_native_size = sizeof(unsigned long) * 8 |
Private Member Functions | |
| uint64_t | count_leading (bool zeros) const |
| bool | shift_is_uint64 (uint64_t *res) const |
| uint64_t | get_limb (void *limb, uint64_t nbits_rem, bool zeros) const |
| bool | is_gmp () const |
Static Private Member Functions | |
| static uint64_t | uint64_fdiv_r_2exp (uint64_t size, uint64_t val) |
Private Attributes | ||
| uint64_t | d_size = 0 | |
| union { | ||
| uint64_t d_val_uint64 | ||
| mpz_t d_val_gmp | ||
| }; | ||
Definition at line 27 of file bitvector.h.
| stabilizer::util::BitVector::BitVector | ( | ) |
Default constructor.
Definition at line 162 of file bitvector.cpp.
Referenced by bvadd(), bvand(), bvashr(), bvashr(), bvconcat(), bvdec(), bveq(), bvextract(), bvimplies(), bvinc(), bvmodinv(), bvmul(), bvnand(), bvne(), bvneg(), bvnego(), bvnor(), bvnot(), bvor(), bvpow(), bvredand(), bvredor(), bvredxor(), bvrepeat(), bvrol(), bvroli(), bvror(), bvrori(), bvsaddo(), bvsdiv(), bvsdivo(), bvsext(), bvsge(), bvsgt(), bvshl(), bvshl(), bvshr(), bvshr(), bvsle(), bvslt(), bvsmod(), bvsmulo(), bvsrem(), bvssubo(), bvsub(), bvuaddo(), bvudiv(), bvuge(), bvugt(), bvule(), bvult(), bvumulo(), bvurem(), bvusubo(), bvxnor(), bvxor(), bvzext(), and mk_zero().
| stabilizer::util::BitVector::BitVector | ( | uint64_t | size | ) |
| stabilizer::util::BitVector::BitVector | ( | uint64_t | size, |
| const std::string & | value, | ||
| uint32_t | base = 2 |
||
| ) |
Construct a bit-vector of given size from given binary string.
| size | The size of the bit-vector, must be >= the length of value. |
| value | A string representing the value of the bit-vector. If the length of this string is > size, the value is zero extended. |
| base | The base the string is given in (2 for binary, 10 for decimal, 16 for hexadecimal). |
Definition at line 171 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, fits_in_size(), hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Construct a bit-vector of given size from given GMP value.
| size | The size of the bit-vector. |
| value | A GMP value representing the bit-vector value. The value must be representable with size bits if truncate is false. |
| truncate | True to allow truncating the value if it is not representable with size bits. |
Definition at line 192 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, fits_in_size(), hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), and size().
Copy constructor.
Definition at line 246 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
| stabilizer::util::BitVector::BitVector | ( | BitVector && | other | ) |
Move constructor.
Definition at line 264 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
| stabilizer::util::BitVector::~BitVector | ( | ) |
Destructor.
Definition at line 287 of file bitvector.cpp.
Determine the value of the bit at given index.
| idx | The index of the bit. |
Definition at line 472 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, hash(), is_gmp(), is_null(), and size().
Referenced by count_trailing_ones(), count_trailing_zeros(), flip_bit(), is_false(), is_true(), lsb(), and msb().
Create a bit-vector representing the addition of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 781 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvadd().
Referenced by is_sadd_overflow().
Create a bit-vector representing the bit-wise and of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 789 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvand().
Create a bit-vector representing the arithmetic right shift of this bit-vector by the given bit-vector shift value.
| bv | A bit-vector representing the number of bits to shift this bit-vector to the right. |
Definition at line 877 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvashr().
Create a bit-vector representing the arithmetic right shift of this bit-vector by the given unsigned integer shift value.
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the right. |
Definition at line 873 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvashr().
Create a bit-vector representing the concatenation of this bit-vector and the given bit-vector. The given bit-vector is concatenated (at the right, the lsb side) to this bit-vector.
| bv | The other bit-vector. |
Definition at line 933 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvconcat().
| BitVector stabilizer::util::BitVector::bvdec | ( | ) | const |
Create a bit-vector representing the decrement (- 1) of this bit-vector.
Definition at line 771 of file bitvector.cpp.
References BitVector(), d_size, and ibvdec().
Referenced by is_power_of_two().
Create a bit-vector representing the equality of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 817 of file bitvector.cpp.
References BitVector(), hash(), and ibveq().
Create a bit-vector representing the extract of a given bit range from this bit-vector.
| idx_hi | The upper bit-index of the range (inclusive). |
| idx_lo | The lower bit-index of the range (inclusive). |
Definition at line 937 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvextract().
Referenced by shift_is_uint64().
Create a bit-vector representing the implication of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 793 of file bitvector.cpp.
References BitVector(), hash(), and ibvimplies().
| BitVector stabilizer::util::BitVector::bvinc | ( | ) | const |
Create a bit-vector representing the increment (+ 1) of this bit-vector.
Definition at line 769 of file bitvector.cpp.
References BitVector(), d_size, and ibvinc().
|
static |
Create an if-then-else (ite) over the given bit-vectors.
| c | A bit-vector representing the condition of the ite. |
| t | A bit-vector representing the then branch of the ite. |
| e | A bit-vector representing the else branch of the ite. |
Definition at line 153 of file bitvector.cpp.
| BitVector stabilizer::util::BitVector::bvmodinv | ( | ) | const |
Calculate modular inverse for this bit-vector by means of the Extended Euclidean Algorithm.
Definition at line 969 of file bitvector.cpp.
References BitVector(), d_size, and ibvmodinv().
Create a bit-vector representing the multiplication of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 881 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvmul().
Create a bit-vector representing the bit-wise nand of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 797 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvnand().
Create a bit-vector representing the disequality of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 821 of file bitvector.cpp.
References BitVector(), hash(), and ibvne().
| BitVector stabilizer::util::BitVector::bvneg | ( | ) | const |
Create a bit-vector representing the two's complement negation of this bit-vector.
Definition at line 765 of file bitvector.cpp.
References BitVector(), d_size, and ibvneg().
| BitVector stabilizer::util::BitVector::bvnego | ( | ) | const |
Create a bit-vector representing a predicate that indicates if bit-vector negation produces an overflow.
Definition at line 779 of file bitvector.cpp.
References BitVector(), and ibvnego().
Create a bit-vector representing the bit-wise nor of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 801 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvnor().
| BitVector stabilizer::util::BitVector::bvnot | ( | ) | const |
Create a bit-vector representing the bit-wise negation of this bit-vector.
Definition at line 767 of file bitvector.cpp.
References BitVector(), d_size, and ibvnot().
Create a bit-vector representing the bit-wise or of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 805 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvor().
Calculate a bit-vector representing this bit-vector exponentiated by exp.
| exp | The exponent GMP value. |
Definition at line 973 of file bitvector.cpp.
References BitVector(), d_size, and ibvpow().
| BitVector stabilizer::util::BitVector::bvredand | ( | ) | const |
Create a bit-vector representing the and reduction of this bit-vector.
Definition at line 773 of file bitvector.cpp.
References BitVector(), and ibvredand().
| BitVector stabilizer::util::BitVector::bvredor | ( | ) | const |
Create a bit-vector representing the or reduction of this bit-vector.
Definition at line 775 of file bitvector.cpp.
References BitVector(), and ibvredor().
| BitVector stabilizer::util::BitVector::bvredxor | ( | ) | const |
Create a bit-vector representing the xor reduction of this bit-vector.
Definition at line 777 of file bitvector.cpp.
References BitVector(), and ibvredxor().
Create a bit-vector representing this bit-vector repeated n times.
| n | The number of times to repeat this bit-vector, must be > 0. |
Definition at line 949 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvrepeat().
Create a bit-vector representing this bit-vector rotated left by n bits.
| n | The number of bits to rotate this bit-vector by. |
Definition at line 957 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvrol().
Create a bit-vector representing this bit-vector rotated left by n bits.
| n | The number of bits to rotate this bit-vector by. |
Definition at line 953 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvroli().
Create a bit-vector representing this bit-vector rotated right by n bits.
| n | The number of bits to rotate this bit-vector by. |
Definition at line 965 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvror().
Create a bit-vector representing this bit-vector rotated right by n bits.
| n | The number of bits to rotate this bit-vector by. |
Definition at line 961 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvrori().
Create a bit-vector representing a predicate that indicates if bit-vector signed addition produces an overflow.
| bv | The other bit-vector. |
Definition at line 909 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsaddo().
Create a bit-vector representing the signed division of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 893 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsdiv().
Create a bit-vector representing a predicate that indicates if bit-vector signed division produces an overflow.
| bv | The other bit-vector. |
Definition at line 929 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsdivo().
Create a bit-vector representing the sign extension of this bit-vector by the given number of bits.
| n | The number of bits to extend this bit-vector with. |
Definition at line 945 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsext().
Referenced by is_smul_overflow().
Create a bit-vector representing the signed greater than or equal of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 853 of file bitvector.cpp.
References BitVector(), hash(), and ibvsge().
Create a bit-vector representing the signed greater than of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 849 of file bitvector.cpp.
References BitVector(), hash(), and ibvsgt().
Create a bit-vector representing the logical left shift of this bit-vector by the given bit-vector shift value.
| shift | A bit-vector representing he number of bits to shift this bit-vector to the left. |
Definition at line 861 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvshl().
Create a bit-vector representing the logical left shift of this bit-vector by the given unsigned integer shift value.
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the left. |
Definition at line 857 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvshl().
Create a bit-vector representing the logical right shift of this bit-vector by the given bit-vector shift value.
| bv | A bit-vector representing the number of bits to shift this bit-vector to the right. |
Definition at line 869 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvshr().
Create a bit-vector representing the logical right shift of this bit-vector by the given unsigned integer shift value.
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the right. |
Definition at line 865 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvshr().
Create a bit-vector representing the signed less than or equal of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 845 of file bitvector.cpp.
References BitVector(), hash(), and ibvsle().
Create a bit-vector representing the signed less than of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 841 of file bitvector.cpp.
References BitVector(), hash(), and ibvslt().
Create a bit-vector representing the signed remainder (sign follows divisor) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 901 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsmod().
Create a bit-vector representing a predicate that indicates if bit-vector signed multiplication produces an overflow.
| bv | The other bit-vector. |
Definition at line 925 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsmulo().
Create a bit-vector representing the signed remainder (sign follows dividend) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 897 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsrem().
Create a bit-vector representing a predicate that indicates if bit-vector signed subtraction produces an overflow.
| bv | The other bit-vector. |
Definition at line 917 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvssubo().
Create a bit-vector representing the subtraction of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 785 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvsub().
Referenced by is_ssub_overflow().
Create a bit-vector representing a predicate that indicates if bit-vector unsigned addition produces an overflow.
| bv | The other bit-vector. |
Definition at line 905 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvuaddo().
Create a bit-vector representing the unsigned division of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 885 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvudiv().
| void stabilizer::util::BitVector::bvudivurem | ( | const BitVector & | bv, |
| BitVector * | quot, | ||
| BitVector * | rem | ||
| ) | const |
Merged bit-vector operations. --------------------------------------— Calculate the unsigned division and remainder of this bit-vector with bv. The result of the division is stored in quot, and the result of the remainder operation is stored in rem.
| bv | The bit-vector to divide by. |
| quot | The bit-vector to store the result of the division in. |
| rem | The bit-vector to store the result of the remainder in. |
Definition at line 2910 of file bitvector.cpp.
References d_size, d_val_uint64, from_ui(), hash(), is_gmp(), is_null(), mk_ones(), mk_zero(), and stabilizer::util::mpz_fdiv_r_2exp_ull().
Referenced by ibvmodinv().
Create a bit-vector representing the unsigned greater than or equal of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 837 of file bitvector.cpp.
References BitVector(), hash(), and ibvuge().
Create a bit-vector representing the unsigned greater than of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 833 of file bitvector.cpp.
References BitVector(), hash(), and ibvugt().
Create a bit-vector representing the unsigned less than or equal of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 829 of file bitvector.cpp.
References BitVector(), hash(), and ibvule().
Create a bit-vector representing the unsigned less than of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 825 of file bitvector.cpp.
References BitVector(), hash(), and ibvult().
Create a bit-vector representing a predicate that indicates if bit-vector unsigned multiplication produces an overflow.
| bv | The other bit-vector. |
Definition at line 921 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvumulo().
Create a bit-vector representing the unsigned remainder of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 889 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvurem().
Create a bit-vector representing a predicate that indicates if bit-vector unsigned subtraction produces an overflow.
| bv | The other bit-vector. |
Definition at line 913 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvusubo().
Create a bit-vector representing the bit-wise xnor of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 809 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvxnor().
Create a bit-vector representing the bit-wise xor of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 813 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvxor().
Create a bit-vector representing the zero extension of this bit-vector by the given number of bits.
| n | The number of bits to extend this bit-vector with. |
Definition at line 941 of file bitvector.cpp.
References BitVector(), d_size, hash(), and ibvzext().
Compare this bit-vector with given bit-vector (unsigned).
| bv | The bit-vector to compare this bit-vector with. |
this is unsigned less than bv, and 1 if this is unsigned greater than bv. Definition at line 431 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by is_usub_overflow(), operator!=(), operator==(), and signed_compare().
Count leading zeros or ones.
| zeros | True to determine number of leading zeros, false to count number of leading ones. |
Definition at line 2980 of file bitvector.cpp.
References d_size, get_limb(), hash(), and is_null().
Referenced by count_leading_ones(), and count_leading_zeros().
| uint64_t stabilizer::util::BitVector::count_leading_ones | ( | ) | const |
Definition at line 756 of file bitvector.cpp.
References count_leading(), and is_null().
| uint64_t stabilizer::util::BitVector::count_leading_zeros | ( | ) | const |
Definition at line 751 of file bitvector.cpp.
References count_leading(), and is_null().
Referenced by shift_is_uint64().
| uint64_t stabilizer::util::BitVector::count_trailing_ones | ( | ) | const |
| uint64_t stabilizer::util::BitVector::count_trailing_zeros | ( | ) | const |
Determine if given GMP value fits into a bit-vector of given size.
| size | The size of the bit-vector. |
| value | The GMP value. |
Definition at line 116 of file bitvector.cpp.
|
static |
Determine if given string representation of a value in the given numeric base fits into a bit-vector of given size.
| size | The size of the bit-vector. |
| str | The string represent of the value. |
| base | The numeric base the value is given in. |
Definition at line 73 of file bitvector.cpp.
References hash(), mk_min_signed(), mk_ones(), size(), and str().
Referenced by BitVector(), BitVector(), fits_in_size(), from_si(), from_ui(), and to_uint64().
|
static |
Determine if given integer value fits into a bit-vector of given size.
| size | The size of the bit-vector. |
| value | The integer value. |
| sign | True if given value is to be interpreted as signed. |
Definition at line 104 of file bitvector.cpp.
References fits_in_size(), hash(), stabilizer::util::mpz_init_set_ull(), and size().
|
static |
Construct a bit-vector of given size from given int64 value.
Truncates value if truncate is true and the value cannot be represented with size bits.
size if size > 64, which is not the case with from_ui() (which zero extends the value).| size | The size of the bit-vector. |
| value | A int64 representing the bit-vector value. The value must be representable with size bits if truncate is false. |
| truncate | True to allow truncating the value if it is not representable with size bits. |
Definition at line 230 of file bitvector.cpp.
References fits_in_size(), hash(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_init_set_sll(), size(), and uint64_fdiv_r_2exp().
|
static |
Construct a bit-vector of given size from given uint64 value.
Truncates value if truncate is true and the value cannot be represented with size bits.
from_si() instead. It guarantees that negative values are sign extended to size if size > 64, which is not the case with from_ui() (which zero extends the value).| size | The size of the bit-vector. |
| value | A uint64 representing the bit-vector value. The value must be representable with size bits if truncate is false. |
| truncate | True to allow truncating the value if it is not representable with size bits. |
Definition at line 214 of file bitvector.cpp.
References fits_in_size(), hash(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_init_set_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvudivurem(), ibvrol(), ibvror(), and mk_one().
|
private |
Get the first limb and return the number of limbs needed to represent this bit-vector if all zero limbs are disregarded.
| limb | The result pointer for the first limb. |
| nbits_rem | The number of bits that spill over into the most significant limb, assuming that all bits are represented). Zero if the bit-width is a multiple of n_bits_per_limb. |
| zeros | True for leading zeros, else ones. |
Definition at line 3011 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by count_leading().
Get mpz_t value from Integer class.
Definition at line 2957 of file bitvector.cpp.
| size_t stabilizer::util::BitVector::hash | ( | ) | const |
Definition at line 326 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and stabilizer::util::mpz_hash().
Referenced by bit(), BitVector(), BitVector(), BitVector(), BitVector(), BitVector(), bvadd(), bvand(), bvashr(), bvashr(), bvconcat(), bveq(), bvextract(), bvimplies(), bvite(), bvmul(), bvnand(), bvne(), bvnor(), bvor(), bvrepeat(), bvrol(), bvroli(), bvror(), bvrori(), bvsaddo(), bvsdiv(), bvsdivo(), bvsext(), bvsge(), bvsgt(), bvshl(), bvshl(), bvshr(), bvshr(), bvsle(), bvslt(), bvsmod(), bvsmulo(), bvsrem(), bvssubo(), bvsub(), bvuaddo(), bvudiv(), bvudivurem(), bvuge(), bvugt(), bvule(), bvult(), bvumulo(), bvurem(), bvusubo(), bvxnor(), bvxor(), bvzext(), compare(), count_leading(), count_trailing_ones(), count_trailing_zeros(), fits_in_size(), fits_in_size(), fits_in_size(), flip_bit(), from_si(), from_ui(), get_limb(), hash(), ibvadd(), ibvadd(), ibvand(), ibvand(), ibvashr(), ibvashr(), ibvashr(), ibvashr(), ibvconcat(), ibvconcat(), ibvdec(), ibveq(), ibveq(), ibvextract(), ibvextract(), ibvimplies(), ibvimplies(), ibvinc(), ibvite(), ibvmodinv(), ibvmul(), ibvmul(), ibvnand(), ibvnand(), ibvne(), ibvne(), ibvneg(), ibvnego(), ibvnor(), ibvnor(), ibvnot(), ibvor(), ibvor(), ibvpow(), ibvredand(), ibvredor(), ibvredxor(), ibvrepeat(), ibvrepeat(), ibvrol(), ibvrol(), ibvroli(), ibvroli(), ibvror(), ibvror(), ibvrori(), ibvrori(), ibvsaddo(), ibvsaddo(), ibvsdiv(), ibvsdiv(), ibvsdivo(), ibvsdivo(), ibvsext(), ibvsext(), ibvsge(), ibvsge(), ibvsgt(), ibvsgt(), ibvshl(), ibvshl(), ibvshl(), ibvshl(), ibvshr(), ibvshr(), ibvshr(), ibvshr(), ibvsle(), ibvsle(), ibvslt(), ibvslt(), ibvsmod(), ibvsmod(), ibvsmulo(), ibvsmulo(), ibvsrem(), ibvsrem(), ibvssubo(), ibvssubo(), ibvsub(), ibvsub(), ibvuaddo(), ibvuaddo(), ibvudiv(), ibvudiv(), ibvuge(), ibvuge(), ibvugt(), ibvugt(), ibvule(), ibvule(), ibvult(), ibvult(), ibvumulo(), ibvumulo(), ibvurem(), ibvurem(), ibvusubo(), ibvusubo(), ibvxnor(), ibvxnor(), ibvxor(), ibvxor(), ibvzext(), ibvzext(), is_max_signed(), is_min_signed(), is_one(), is_ones(), is_sadd_overflow(), is_sdiv_overflow(), is_smul_overflow(), is_ssub_overflow(), is_uadd_overflow(), is_umul_overflow(), is_usub_overflow(), is_zero(), iset(), mk_max_signed(), mk_min_signed(), mk_ones(), operator!=(), operator=(), operator==(), set_bit(), shift_is_uint64(), signed_compare(), str(), to_mpz(), to_uint64(), uint64_fdiv_r_2exp(), and ~BitVector().
Addition (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2643 of file bitvector.cpp.
Addition (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the addition. |
| bv1 | The second operand of the addition. |
Definition at line 1128 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvadd(), stabilizer::parser::BitVectorUtils::bvAdd(), ibvadd(), ibvroli(), ibvrori(), and ibvsmod().
Bit-wise and (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2648 of file bitvector.cpp.
Bit-wise and (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the bit-wise and. |
| bv1 | The second operand of the bit-wise and. |
Definition at line 1178 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvand(), ibvand(), and is_power_of_two().
Arithmetic right shift (in-place) of this bit-vector by the given bit-vector shift value.
| bv | A bit-vector representing the number of bits to shift this bit-vector to the right. |
Definition at line 2763 of file bitvector.cpp.
| BitVector & stabilizer::util::BitVector::ibvashr | ( | const BitVector & | bv, |
| const BitVector & | arithmetic | ||
| ) |
Arithmetic right shift (in-place) of the given bit-vector by the given bit-vector shift value.
| bv | The bit-vector to shift. |
| shift | The bit-vector representing the number of bits to shift bv. |
Definition at line 1696 of file bitvector.cpp.
Arithmetic right shift (in-place) of the given bit-vector by the given unsigned integer shift value.
| bv | The bit-vector to shift. |
| shift | The bit-vector representing the number of bits to shift bv. |
Definition at line 1684 of file bitvector.cpp.
References hash(), ibvnot(), ibvnot(), and ibvshr().
Referenced by bvashr(), stabilizer::parser::BitVectorUtils::bvAshr(), bvashr(), ibvashr(), and ibvashr().
Arithmetic right shift (in-place) of this bit-vector by the given unsigned integer shift value.
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the right. |
Definition at line 2758 of file bitvector.cpp.
Concatenation (in-place) of this bit-vector and the given bit-vector. Bit-vector bv is concatenated (at the right, the lsb side) to this bit-vector.
| bv | The other bit-vector. |
Definition at line 2833 of file bitvector.cpp.
References hash(), and ibvconcat().
Concatenation (in-place) of the given bit-vectors. Bit-vector bv1 is concatenated (at the right, the lsb side) to bv0.
| bv0 | The first operand of the concatenation. |
| bv1 | The second operand of the concatenation. |
Definition at line 2026 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_mul_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Referenced by bvconcat(), and ibvconcat().
| BitVector & stabilizer::util::BitVector::ibvdec | ( | ) |
Decrement (in-place, chainable) of this bit-vector.
Definition at line 2618 of file bitvector.cpp.
References ibvdec().
Referenced by ibvdec().
Decrement (in-place) of the given bit-vector.
| bv | The bit-vector to compute the decrement for. |
bv. Definition at line 1041 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvdec().
Equality (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2688 of file bitvector.cpp.
Equality (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the equality. |
| bv1 | The second operand of the equality. |
Definition at line 1347 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
| BitVector & stabilizer::util::BitVector::ibvextract | ( | const BitVector & | bv, |
| uint64_t | idx_hi, | ||
| uint64_t | idx_lo | ||
| ) |
Extract a bit range from bit-vector bv (in-place).
| bv | The bit-vector to extract a bit range from. |
| idx_hi | The upper bit-index of the range (inclusive). |
| idx_lo | The lower bit-index of the range (inclusive). |
Definition at line 2080 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_q_2exp_ull(), stabilizer::util::mpz_fdiv_r_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Referenced by bvextract(), and ibvextract().
Extract a bit range from this bit-vector (in-place).
| idx_hi | The upper bit-index of the range (inclusive). |
| idx_lo | The lower bit-index of the range (inclusive). |
Definition at line 2838 of file bitvector.cpp.
References hash(), and ibvextract().
Implication (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2653 of file bitvector.cpp.
References hash(), and ibvimplies().
| BitVector & stabilizer::util::BitVector::ibvimplies | ( | const BitVector & | bv0, |
| const BitVector & | bv1 | ||
| ) |
Implication (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the implication. |
| bv1 | The second operand of the implication. |
Definition at line 1203 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvimplies(), and ibvimplies().
| BitVector & stabilizer::util::BitVector::ibvinc | ( | ) |
Increment (in-place, chainable) of this bit-vector.
Definition at line 2613 of file bitvector.cpp.
References ibvinc().
Referenced by ibvinc().
Increment (in-place) of the given bit-vector.
| bv | The bit-vector to compute the increment for. |
bv. Definition at line 1019 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvinc().
| BitVector & stabilizer::util::BitVector::ibvite | ( | const BitVector & | c, |
| const BitVector & | t, | ||
| const BitVector & | e | ||
| ) |
Create an if-then-else over the given bit-vectors (in-place).
| c | A bit-vector representing the condition of the ite. |
| t | A bit-vector representing the then branch of the ite. |
| e | A bit-vector representing the else branch of the ite. |
Definition at line 2453 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), is_null(), and size().
| BitVector & stabilizer::util::BitVector::ibvmodinv | ( | ) |
Calculate modular inverse of this bit-vector by means of the Extended Euclidean Algorithm (in-place).
Definition at line 2878 of file bitvector.cpp.
References ibvmodinv().
Referenced by ibvmodinv().
Calculate modular inverse of the given bit-vector by means of the Extended Euclidean Algorithm (in-place).
bv must be odd. The greatest common divisor gcd (c, 2^bw) must be (and is, in this case) always 1.| bv | The bit-vector to compute the modular inverse for. |
Definition at line 2494 of file bitvector.cpp.
References bvudivurem(), d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), mk_one(), stabilizer::util::mpz_fdiv_r_2exp_ull(), s_native_size, and size().
Referenced by bvmodinv().
Multiplication (in-place) of this bit-vector by the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2768 of file bitvector.cpp.
Multiplication (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the multiplication. |
| bv1 | The second operand of the multiplication. |
Definition at line 1717 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvmul(), stabilizer::parser::BitVectorUtils::bvMul(), ibvmul(), and is_smul_overflow().
Bit-wise nand (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2658 of file bitvector.cpp.
Bit-wise nand (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the bit-wise nand. |
| bv1 | The second operand of the bit-wise nand. |
Definition at line 1219 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Disequality (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2693 of file bitvector.cpp.
Disequality (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the disequality. |
| bv1 | The second operand of the disequality. |
Definition at line 1367 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
| BitVector & stabilizer::util::BitVector::ibvneg | ( | ) |
Two's complement negation (in-place) of this bit-vector.
Definition at line 2603 of file bitvector.cpp.
References ibvneg().
Referenced by ibvneg(), ibvsdiv(), ibvsmod(), and ibvsrem().
Two's complement negation (in-place) of the given bit-vector.
| bv | The bit-vector to compute the two's complement for. |
bv. Definition at line 981 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvnot(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), and uint64_fdiv_r_2exp().
Referenced by bvneg(), stabilizer::parser::BitVectorUtils::bvNeg(), and ibvsrem().
| BitVector & stabilizer::util::BitVector::ibvnego | ( | ) |
Bit-vector negation overflow check (in-place, chainable) of this bit-vector.
Result is a bit-vector of size 1, representing the result of the overflow check of the given bit-vector (1 if an overflow occurs, and 0 otherwise).
Definition at line 2638 of file bitvector.cpp.
References ibvnego().
Referenced by ibvnego().
Bit-vector negation overflow check (in-place) of the given bit-vector.
Result is a bit-vector of size 1, representing the result of the overflow check of the given bit-vector (1 if an overflow occurs, and 0 otherwise).
| bv | The bit-vector to compute the overflow check for. |
bv. Definition at line 1119 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvnego().
Bit-wise nor (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2663 of file bitvector.cpp.
Bit-wise nor (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the bit-wise nor. |
| bv1 | The second operand of the bit-wise nor. |
Definition at line 1245 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
| BitVector & stabilizer::util::BitVector::ibvnot | ( | ) |
Bit-wise negation (in-place) of this bit-vector.
Definition at line 2608 of file bitvector.cpp.
References ibvnot().
Bit-wise negation (in-place) of the given bit-vector.
| bv | The bit-vector to compute the bit-wise negation for. |
bv. Definition at line 997 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Bit-wise or (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2668 of file bitvector.cpp.
Bit-wise or (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the bit-wise or. |
| bv1 | The second operand of the bit-wise or. |
Definition at line 1271 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Calculate a bit-vector base exponentiated by exp (in-place).
| base | The base bit-vector. |
| exp | The exponent GMP value. |
Definition at line 2883 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_get_ull(), stabilizer::util::mpz_init_set_ull(), stabilizer::util::mpz_mul_2exp_ull(), and size().
Calculate a bit-vector representing this bit-vector exponentiated by exp (in-place).
| exp | The exponent GMP value. |
Definition at line 2903 of file bitvector.cpp.
References ibvpow().
| BitVector & stabilizer::util::BitVector::ibvredand | ( | ) |
And reduction (in-place, chainable) of this bit-vector.
Result is a bit-vector of size 1, representing the result of the and reduction of this bit-vector (1 if all bits of this bit-vector are one, and 0 otherwise).
Definition at line 2623 of file bitvector.cpp.
References ibvredand().
Referenced by ibvredand().
And reduction (in-place) of the given bit-vector.
Result is a bit-vector of size 1, representing the result of the and reduction of the given bit-vector (1 if all bits of this bit-vector are one, and 0 otherwise).
| bv | The bit-vector to compute the and reduction for. |
bv. Definition at line 1063 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvredand().
| BitVector & stabilizer::util::BitVector::ibvredor | ( | ) |
Or reduction (in-place, chainable) of this bit-vector.
Result is a bit-vector of size 1, representing the result of the or reduction of this bit-vector (1 if at least one bit of this bit-vector is one, and 0 otherwise).
Definition at line 2628 of file bitvector.cpp.
References ibvredor().
Referenced by ibvredor().
Or reduction (in-place) of the given bit-vector.
Result is a bit-vector of size 1, representing the result of the or reduction of the given bit-vector (1 if at least one bit of this bit-vector is one, and 0 otherwise).
| bv | The bit-vector to compute the or reduction for. |
bv. Definition at line 1076 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvredor().
| BitVector & stabilizer::util::BitVector::ibvredxor | ( | ) |
Xor reduction (in-place, chainable) of this bit-vector.
Result is a bit-vector of size 1, representing the result of the xor reduction of this bit-vector (1 if an uneven number of bits is set to 1, and 0 otherwise).
Definition at line 2633 of file bitvector.cpp.
References ibvredxor().
Referenced by ibvredxor().
Xor reduction (in-place) of the given bit-vector.
Result is a bit-vector of size 1, representing the result of the xor reduction of the given bit-vector (1 if an uneven number of bits is set to 1, and 0 otherwise).
| bv | The bit-vector to compute the xor reduction for. |
bv. Definition at line 1099 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvredxor().
Repeat (in-place) of the given bit-vector.
| bv | The bit-vector to repeat. |
| n | The number of times to repeat bit-vector bv, must be > 0. |
Definition at line 2266 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_mul_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Referenced by bvrepeat(), and ibvrepeat().
Repeat (in-place) of this bit-vector.
| n | The number of times to repeat this bit-vector, must be > 0. |
Definition at line 2853 of file bitvector.cpp.
References hash(), and ibvrepeat().
Rotate left (in-place) of the given bit-vector.
| bv | The bit-vector to rotate. |
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2367 of file bitvector.cpp.
References bvurem(), d_size, from_ui(), hash(), ibvroli(), shift_is_uint64(), and size().
Rotate left (in-place) of this bit-vector.
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2863 of file bitvector.cpp.
Rotate left (in-place) of the given bit-vector.
| bv | The bit-vector to rotate. |
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2319 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvadd(), is_gmp(), stabilizer::util::mpz_mul_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Rotate left (in-place) of this bit-vector.
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2858 of file bitvector.cpp.
Rotate right (in-place) of the given bit-vector.
| bv | The bit-vector to rotate. |
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2434 of file bitvector.cpp.
References bvurem(), d_size, from_ui(), hash(), ibvrori(), shift_is_uint64(), and size().
Rotate right (in-place) of this bit-vector.
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2873 of file bitvector.cpp.
Rotate right (in-place) of the given bit-vector.
| bv | The bit-vector to rotate. |
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2386 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvadd(), is_gmp(), stabilizer::util::mpz_fdiv_q_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Rotate right(in-place) of this bit-vector.
| n | The number of bits to rotate bit-vector bv by. |
Definition at line 2868 of file bitvector.cpp.
Signed addition overflow check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2803 of file bitvector.cpp.
References hash(), and ibvsaddo().
Signed addition overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the addition. |
| bv1 | The second operand of the addition. |
Definition at line 1948 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvsaddo(), and ibvsaddo().
Signed division (in-place) of this bit-vector by the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2783 of file bitvector.cpp.
Signed division (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the signed division. |
| bv1 | The second operand of the signed division. |
Definition at line 1813 of file bitvector.cpp.
References hash(), ibvneg(), and ibvudiv().
Referenced by bvsdiv(), stabilizer::parser::BitVectorUtils::bvSdiv(), and ibvsdiv().
Signed overflow division check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2828 of file bitvector.cpp.
References hash(), and ibvsdivo().
Signed division overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the division. |
| bv1 | The second operand of the division. |
Definition at line 2013 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvsdivo(), and ibvsdivo().
Sign extension (in-place) of the given bit-vector.
| bv | The bit-vector to sign extend. |
| n | The number of bits to extend bit-vector bv with. |
Definition at line 2181 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvzext(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_mul_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Referenced by bvsext(), ibvsext(), and is_smul_overflow().
Sign extension (in-place) of this bit-vector.
| n | The number of bits to extend bit-vector bv with. |
Definition at line 2848 of file bitvector.cpp.
Signed greater than or equal (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2733 of file bitvector.cpp.
Signed greater than or equal (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the signed greater than or equal. |
| bv1 | The second operand of the signed greater than or equal. |
Definition at line 1539 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvuge(), and is_gmp().
Signed greater than (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2728 of file bitvector.cpp.
Signed greater than (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the signed greater than. |
| bv1 | The second operand of the signed greater than. |
Definition at line 1515 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvugt(), and is_gmp().
Logical left shift (in-place) of this bit-vector by the given bit-vector shift value.
| bv | A bit-vector representing the number of bits to shift this bit-vector to the left. |
Definition at line 2743 of file bitvector.cpp.
Logical left shift (in-place) of the given bit-vector by the given bit-vector shift value.
| bv | The bit-vector to shift. |
| shift | The bit-vector representing the number of bits to shift bv. |
Definition at line 1595 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvshl(), is_gmp(), and size().
Logical left shift (in-place) of the given bit-vector by the given unsigned integer value.
| bv | The bit-vector to shift. |
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the left. |
Definition at line 1563 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_mul_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvshl(), stabilizer::parser::BitVectorUtils::bvShl(), bvshl(), ibvshl(), ibvshl(), and ibvshl().
Logical left shift (in-place) of this bit-vector by the given unsigned integer value.
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the left. |
Definition at line 2738 of file bitvector.cpp.
Logical right shift (in-place) of this bit-vector by the given bit-vector shift value.
| bv | A bit-vector representing the number of bits to shift this bit-vector to the right. |
Definition at line 2753 of file bitvector.cpp.
Logical right shift (in-place) of the given bit-vector by the given bit-vector shift value.
| bv | The bit-vector to shift. |
| shift | The bit-vector representing the number of bits to shift bv. |
Definition at line 1655 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvshr(), is_gmp(), and size().
Logical right shift (in-place) of of the given bit-vector by the given unsigned integer shift value.
| bv | The bit-vector to shift. |
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the right. |
Definition at line 1624 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_q_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by stabilizer::parser::BitVectorUtils::bvLshr(), bvshr(), bvshr(), ibvashr(), ibvashr(), ibvshr(), ibvshr(), and ibvshr().
Logical right shift (in-place) of this bit-vector by the given unsigned integer value.
| shift | An unsigned integer representing the number of bits to shift this bit-vector to the right. |
Definition at line 2748 of file bitvector.cpp.
Signed less than or equal (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2723 of file bitvector.cpp.
Signed less than or equal (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned less than or equal. |
| bv1 | The second operand of the unsigned less than or equal. |
Definition at line 1491 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvule(), and is_gmp().
Signed less than (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2718 of file bitvector.cpp.
Signed less than (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the signed less than. |
| bv1 | The second operand of the signed less than. |
Definition at line 1467 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), ibvult(), and is_gmp().
Signed remainder (sign follows divisor, in-place) of this bit-vector by the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2793 of file bitvector.cpp.
Signed remainder (sign follows divisor, in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the signed remainder. |
| bv1 | The second operand of the signed remainder. |
Definition at line 1886 of file bitvector.cpp.
References hash(), ibvadd(), ibvneg(), ibvurem(), and is_zero().
Referenced by bvsmod(), stabilizer::parser::BitVectorUtils::bvSmod(), and ibvsmod().
Signed overflow multiplication check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2823 of file bitvector.cpp.
References hash(), and ibvsmulo().
Signed multiplication overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the multiplication. |
| bv1 | The second operand of the multiplication. |
Definition at line 2000 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvsmulo(), and ibvsmulo().
Signed remainder (sign follows divident, in-place) of this bit-vector by the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2788 of file bitvector.cpp.
Signed remainder (sign follows dividend, in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the signed remainder. |
| bv1 | The second operand of the signed remainder. |
Definition at line 1850 of file bitvector.cpp.
References hash(), ibvneg(), ibvneg(), and ibvurem().
Referenced by bvsrem(), stabilizer::parser::BitVectorUtils::bvSrem(), and ibvsrem().
Signed subtraction overflow check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2813 of file bitvector.cpp.
References hash(), and ibvssubo().
Signed subtraction overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the subtraction. |
| bv1 | The second operand of the subtraction. |
Definition at line 1974 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvssubo(), and ibvssubo().
Subtraction (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2673 of file bitvector.cpp.
Subtraction (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the subtraction. |
| bv1 | The second operand of the subtraction. |
Definition at line 1153 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvsub(), stabilizer::parser::BitVectorUtils::bvSub(), and ibvsub().
Unsigned addition overflow check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2798 of file bitvector.cpp.
References hash(), and ibvuaddo().
Unsigned addition overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the addition. |
| bv1 | The second operand of the addition. |
Definition at line 1935 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvuaddo(), and ibvuaddo().
Unsigned division (in-place) of this bit-vector by the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2773 of file bitvector.cpp.
Unsigned division (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned division. |
| bv1 | The second operand of the unsigned division. |
Definition at line 1742 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_mul_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvudiv(), stabilizer::parser::BitVectorUtils::bvUdiv(), ibvsdiv(), and ibvudiv().
Unsigned greater than or equal (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2713 of file bitvector.cpp.
Unsigned greater than or equal (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned greater than or equal. |
| bv1 | The second operand of the unsigned greater than or equal. |
Definition at line 1447 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Unsigned greater than (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2708 of file bitvector.cpp.
Unsigned greater than (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned greater than. |
| bv1 | The second operand of the unsigned greater than. |
Definition at line 1427 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Unsigned less than or equal (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2703 of file bitvector.cpp.
Unsigned less than or equal (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned less than or equal. |
| bv1 | The second operand of the unsigned less than or equal. |
Definition at line 1407 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Unsigned less than (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2698 of file bitvector.cpp.
Unsigned less than (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned less than. |
| bv1 | The second operand of the unsigned less than. |
Definition at line 1387 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Unsigned multiplication overflow check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2818 of file bitvector.cpp.
References hash(), and ibvumulo().
Unsigned multiplication overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the multiplication. |
| bv1 | The second operand of the multiplication. |
Definition at line 1987 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvumulo(), and ibvumulo().
Unsigned division (in-place) of this bit-vector by the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2778 of file bitvector.cpp.
Unsigned remainder (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the unsigned remainder. |
| bv1 | The second operand of the unsigned remainder. |
Definition at line 1778 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Referenced by bvurem(), stabilizer::parser::BitVectorUtils::bvUrem(), ibvsmod(), ibvsrem(), and ibvurem().
Unsigned subtraction overflow check (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2808 of file bitvector.cpp.
References hash(), and ibvusubo().
Unsigned subtraction overflow check (in-place) of given bit-vectors bv0 and bv1.
| bv0 | The first operand of the subtraction. |
| bv1 | The second operand of the subtraction. |
Definition at line 1961 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
Referenced by bvusubo(), and ibvusubo().
Bit-wise xnor (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2678 of file bitvector.cpp.
Bit-wise xnor (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the bit-wise xnor. |
| bv1 | The second operand of the bit-wise xnor. |
Definition at line 1296 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Bit-wise xor (in-place) of this bit-vector and the given bit-vector.
| bv | The other bit-vector. |
Definition at line 2683 of file bitvector.cpp.
Bit-wise xor (in-place) of the given bit-vectors bv0 and bv1.
| bv0 | The first operand of the bit-wise xor. |
| bv1 | The second operand of the bit-wise xor. |
Definition at line 1322 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), stabilizer::util::mpz_fdiv_r_2exp_ull(), size(), and uint64_fdiv_r_2exp().
Zero extension (in-place) of the given bit-vector.
| bv | The bit-vector to zero extend. |
| n | The number of bits to extend bit-vector bv with. |
Definition at line 2132 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), s_native_size, and size().
Zero extension (in-place) of this bit-vector.
| n | The number of bits to extend bit-vector bv with. |
Definition at line 2843 of file bitvector.cpp.
| bool stabilizer::util::BitVector::is_false | ( | ) | const |
Definition at line 529 of file bitvector.cpp.
|
inlineprivate |
Determine whether value is stored as GMP value or uint64_t. This check depends on s_native_size, i.e., for 64-bit Windows values exceeding 32 bit are stored as GMP value, for 64-bit Linux and macOS values exceeding 64 bit are stored as GMP value.
Definition at line 2195 of file bitvector.h.
References d_size, and s_native_size.
Referenced by bit(), BitVector(), BitVector(), BitVector(), BitVector(), BitVector(), bvudivurem(), compare(), count_trailing_ones(), count_trailing_zeros(), flip_bit(), get_limb(), gmp_value(), hash(), ibvadd(), ibvand(), ibvconcat(), ibvdec(), ibveq(), ibvextract(), ibvimplies(), ibvinc(), ibvite(), ibvmodinv(), ibvmul(), ibvnand(), ibvne(), ibvneg(), ibvnego(), ibvnor(), ibvnot(), ibvor(), ibvpow(), ibvredand(), ibvredor(), ibvredxor(), ibvrepeat(), ibvroli(), ibvrori(), ibvsaddo(), ibvsdivo(), ibvsext(), ibvsge(), ibvsgt(), ibvshl(), ibvshl(), ibvshr(), ibvshr(), ibvsle(), ibvslt(), ibvsmulo(), ibvssubo(), ibvsub(), ibvuaddo(), ibvudiv(), ibvuge(), ibvugt(), ibvule(), ibvult(), ibvumulo(), ibvurem(), ibvusubo(), ibvxnor(), ibvxor(), ibvzext(), is_max_signed(), is_min_signed(), is_one(), is_ones(), is_uadd_overflow(), is_umul_overflow(), is_zero(), iset(), iset(), operator=(), set_bit(), str(), to_mpz(), to_uint64(), and ~BitVector().
| bool stabilizer::util::BitVector::is_max_signed | ( | ) | const |
Definition at line 596 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
| bool stabilizer::util::BitVector::is_min_signed | ( | ) | const |
Definition at line 581 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by is_neg_overflow(), and is_sdiv_overflow().
| bool stabilizer::util::BitVector::is_neg_overflow | ( | ) | const |
Determine if the negation of this bit-vector produces an overflow.
Definition at line 617 of file bitvector.cpp.
References is_min_signed(), and is_null().
|
inline |
Definition at line 194 of file bitvector.h.
References d_size.
Referenced by bit(), bvite(), bvudivurem(), compare(), count_leading(), count_leading_ones(), count_leading_zeros(), count_trailing_ones(), count_trailing_zeros(), flip_bit(), get_limb(), ibvite(), is_false(), is_max_signed(), is_min_signed(), is_neg_overflow(), is_one(), is_ones(), is_power_of_two(), is_sadd_overflow(), is_sdiv_overflow(), is_smul_overflow(), is_ssub_overflow(), is_true(), is_uadd_overflow(), is_umul_overflow(), is_usub_overflow(), is_zero(), iset(), iset(), lsb(), msb(), operator!=(), operator==(), set_bit(), signed_compare(), str(), and to_uint64().
| bool stabilizer::util::BitVector::is_one | ( | ) | const |
Definition at line 573 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by is_smul_overflow().
| bool stabilizer::util::BitVector::is_ones | ( | ) | const |
Definition at line 544 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), is_null(), and uint64_fdiv_r_2exp().
| bool stabilizer::util::BitVector::is_power_of_two | ( | ) | const |
Determine if the (signed) division of this and the given bit-vector produces an overflow.
| bv | The bit-vector to divide this bit-vector by. |
Definition at line 709 of file bitvector.cpp.
References d_size, hash(), is_min_signed(), and is_null().
Determine if the (signed) multiplication of this and the given bit-vector produces an overflow.
| bv | The bit-vector to multiply this bit-vector with. |
Definition at line 693 of file bitvector.cpp.
References bvsext(), d_size, hash(), ibvmul(), ibvsext(), is_null(), is_one(), mk_max_signed(), mk_min_signed(), and signed_compare().
| bool stabilizer::util::BitVector::is_true | ( | ) | const |
Definition at line 522 of file bitvector.cpp.
| bv | A bit-vector representing the number of bits to shift this bit-vector to the left. |
| bv | The bit-vector to add to this bit-vector. |
Definition at line 622 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), is_null(), and stabilizer::util::mpz_fdiv_q_2exp_ull().
Determine if the (unsigned) multiplication of this and the given bit-vector produces an overflow.
| bv | The bit-vector to multiply this bit-vector with. |
Definition at line 672 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), is_null(), and stabilizer::util::mpz_fdiv_q_2exp_ull().
| bool stabilizer::util::BitVector::is_zero | ( | ) | const |
Definition at line 536 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by ibvsmod(), and is_power_of_two().
Set the value of this bit-vector to the value of bv (in-place).
| bv | A bit-vector representing the value this bit-vector is to between set to. |
Definition at line 363 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Set the value of this bit-vector to the given unsigned (in-place).
| value | The value to set. |
Definition at line 351 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, is_gmp(), is_null(), stabilizer::util::mpz_fdiv_r_2exp_ull(), stabilizer::util::mpz_set_ull(), and uint64_fdiv_r_2exp().
| bool stabilizer::util::BitVector::lsb | ( | ) | const |
Definition at line 512 of file bitvector.cpp.
|
static |
Create a false bit-vector (value 0 of size 1).
Definition at line 122 of file bitvector.cpp.
References mk_zero().
Create a maximum signed value (01..1) bit-vector of given size.
| size | The size of the bit-vector. |
Definition at line 147 of file bitvector.cpp.
References hash(), mk_ones(), and size().
Referenced by is_smul_overflow().
Create a minimum signed value (10..0) bit-vector of given size.
| size | The size of the bit-vector. |
Definition at line 141 of file bitvector.cpp.
References hash(), mk_zero(), and size().
Referenced by fits_in_size(), and is_smul_overflow().
Create a one bit-vector of given size.
| size | The size of the bit-vector. |
Definition at line 126 of file bitvector.cpp.
References from_ui(), and size().
Referenced by ibvmodinv(), and mk_true().
Create a ones bit-vector of given size.
| size | The size of the bit-vector. |
Definition at line 128 of file bitvector.cpp.
References hash(), stabilizer::util::mpz_mul_2exp_ull(), s_native_size, size(), and uint64_fdiv_r_2exp().
Referenced by bvudivurem(), fits_in_size(), and mk_max_signed().
|
static |
Create a true bit-vector (value 1 of size 1).
Definition at line 120 of file bitvector.cpp.
References mk_one().
Create a zero bit-vector of given size.
| size | The size of the bit-vector. |
Definition at line 124 of file bitvector.cpp.
References BitVector(), and size().
Referenced by bvudivurem(), mk_false(), and mk_min_signed().
| bool stabilizer::util::BitVector::msb | ( | ) | const |
Definition at line 517 of file bitvector.cpp.
References bit(), d_size, and is_null().
Referenced by is_sadd_overflow(), is_ssub_overflow(), and signed_compare().
Disequality comparison operator.
| bv | The bit-vector to compare this bit-vector to. |
Definition at line 381 of file bitvector.cpp.
| BitVector & stabilizer::util::BitVector::operator= | ( | const BitVector & | other | ) |
Copy assignment operator.
Definition at line 293 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), and is_gmp().
| bool stabilizer::util::BitVector::operator== | ( | const BitVector & | bv | ) | const |
Equality comparison operator.
| bv | The bit-vector to compare this bit-vector to. |
Definition at line 375 of file bitvector.cpp.
Set the bit at given index to the given value.
| idx | The index of the bit. |
| value | The value. |
Definition at line 481 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by flip_bit().
Determine if this bit-vector can be represented with a uint64_t.
| res | If true, uint64_t representation is stored in res. |
Definition at line 3084 of file bitvector.cpp.
References bvextract(), count_leading_zeros(), d_size, hash(), and to_uint64().
Compare this bit-vector with given bit-vector (signed).
| bv | The bit-vector to compare this bit-vector with. |
this is signed less than bv, and 1 if this is signed greater than bv. Definition at line 452 of file bitvector.cpp.
References compare(), d_size, hash(), is_null(), and msb().
Referenced by is_smul_overflow().
|
inline |
Definition at line 248 of file bitvector.h.
References d_size.
Referenced by bit(), BitVector(), BitVector(), BitVector(), fits_in_size(), fits_in_size(), fits_in_size(), from_si(), from_ui(), ibvadd(), ibvand(), ibvconcat(), ibvdec(), ibvextract(), ibvinc(), ibvite(), ibvmodinv(), ibvmul(), ibvnand(), ibvnor(), ibvnot(), ibvor(), ibvpow(), ibvrepeat(), ibvrol(), ibvroli(), ibvror(), ibvrori(), ibvsext(), ibvshl(), ibvshl(), ibvshr(), ibvshr(), ibvsub(), ibvudiv(), ibvurem(), ibvxnor(), ibvxor(), ibvzext(), mk_max_signed(), mk_min_signed(), mk_one(), mk_ones(), mk_zero(), and uint64_fdiv_r_2exp().
| std::string stabilizer::util::BitVector::str | ( | uint32_t | base = 2 | ) | const |
Get the string representation of this bit-vector.
| base | 2 for binary representation, 10 for decimal representation, 16 for hexadecimal representation. |
Definition at line 387 of file bitvector.cpp.
References d_size, d_val_gmp, d_val_uint64, hash(), is_gmp(), and is_null().
Referenced by stabilizer::parser::BitVectorUtils::bvAdd(), stabilizer::parser::BitVectorUtils::bvAshr(), stabilizer::parser::BitVectorUtils::bvLshr(), stabilizer::parser::BitVectorUtils::bvMul(), stabilizer::parser::BitVectorUtils::bvNeg(), stabilizer::parser::BitVectorUtils::bvSdiv(), stabilizer::parser::BitVectorUtils::bvShl(), stabilizer::parser::BitVectorUtils::bvSmod(), stabilizer::parser::BitVectorUtils::bvSrem(), stabilizer::parser::BitVectorUtils::bvSub(), stabilizer::parser::BitVectorUtils::bvUdiv(), stabilizer::parser::BitVectorUtils::bvUrem(), fits_in_size(), and stabilizer::util::operator<<().
| mpz_class stabilizer::util::BitVector::to_mpz | ( | ) | const |
Convert bit-vector to mpz_class.
Definition at line 2962 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, hash(), is_gmp(), and stabilizer::util::uint64_to_mpz_class().
Get the uint64_t representation of this bit-vector.
| size | The size of this bit-vector, must be <= 64. |
| truncate | True to allow truncating the value if it is not representable with 64 bits. |
Definition at line 420 of file bitvector.cpp.
References d_val_gmp, d_val_uint64, fits_in_size(), hash(), is_gmp(), is_null(), and stabilizer::util::mpz_get_ull().
Referenced by shift_is_uint64().
|
staticprivate |
Normalize uint64_t value for a given bit-width. The equivalent of mpz_fdiv_r_2exp for uint64_t values. Compute the remainder of the division of val by 2^size, implemented with shifts and a bit mask.
| size | The bit-width. |
| val | The value. |
Definition at line 2973 of file bitvector.cpp.
References hash(), and size().
Referenced by BitVector(), from_si(), from_ui(), ibvadd(), ibvand(), ibvconcat(), ibvdec(), ibvextract(), ibvinc(), ibvmul(), ibvnand(), ibvneg(), ibvnor(), ibvnot(), ibvor(), ibvrepeat(), ibvroli(), ibvrori(), ibvsext(), ibvshl(), ibvshr(), ibvsub(), ibvudiv(), ibvurem(), ibvxnor(), ibvxor(), is_ones(), iset(), and mk_ones().
| union { ... } stabilizer::util::BitVector |
The bit-vector value.
Note: We use a union instead of std::variant here in order to avoid the overhead of the latter, since we already have a "tracking variable" (the size of the bit-vector, d_size). Further, we do not use a unique_ptr for d_val_gmp because we don't gain anything if it is in a union – we have to manually destruct it anyways.
|
private |
The size of this bit-vector.
Definition at line 2198 of file bitvector.h.
Referenced by BitVector(), BitVector(), bvadd(), bvand(), bvashr(), bvashr(), bvconcat(), bvdec(), bvextract(), bvinc(), bvite(), bvmodinv(), bvmul(), bvnand(), bvneg(), bvnor(), bvnot(), bvor(), bvpow(), bvrepeat(), bvrol(), bvroli(), bvror(), bvrori(), bvsaddo(), bvsdiv(), bvsdivo(), bvsext(), bvshl(), bvshl(), bvshr(), bvshr(), bvsmod(), bvsmulo(), bvsrem(), bvssubo(), bvsub(), bvuaddo(), bvudiv(), bvudivurem(), bvumulo(), bvurem(), bvusubo(), bvxnor(), bvxor(), bvzext(), compare(), count_leading(), count_trailing_ones(), count_trailing_zeros(), get_limb(), hash(), ibvadd(), ibvand(), ibvconcat(), ibvdec(), ibveq(), ibvextract(), ibvimplies(), ibvinc(), ibvite(), ibvmodinv(), ibvmul(), ibvnand(), ibvne(), ibvneg(), ibvnego(), ibvnor(), ibvnot(), ibvor(), ibvredand(), ibvredor(), ibvredxor(), ibvrepeat(), ibvrol(), ibvroli(), ibvror(), ibvrori(), ibvsaddo(), ibvsdivo(), ibvsext(), ibvsge(), ibvsgt(), ibvshl(), ibvshl(), ibvshr(), ibvshr(), ibvsle(), ibvslt(), ibvsmulo(), ibvssubo(), ibvsub(), ibvuaddo(), ibvudiv(), ibvuge(), ibvugt(), ibvule(), ibvult(), ibvumulo(), ibvurem(), ibvusubo(), ibvxnor(), ibvxor(), ibvzext(), is_false(), is_gmp(), is_max_signed(), is_min_signed(), is_null(), is_ones(), is_sadd_overflow(), is_sdiv_overflow(), is_smul_overflow(), is_ssub_overflow(), is_true(), is_uadd_overflow(), is_umul_overflow(), is_usub_overflow(), iset(), iset(), msb(), operator=(), set_bit(), shift_is_uint64(), signed_compare(), size(), and str().
| mpz_t stabilizer::util::BitVector::d_val_gmp |
Definition at line 2210 of file bitvector.h.
Referenced by bit(), BitVector(), BitVector(), BitVector(), BitVector(), BitVector(), compare(), count_trailing_ones(), count_trailing_zeros(), flip_bit(), get_limb(), gmp_value(), hash(), ibvadd(), ibvand(), ibvconcat(), ibvdec(), ibveq(), ibvextract(), ibvimplies(), ibvinc(), ibvite(), ibvmodinv(), ibvmul(), ibvnand(), ibvne(), ibvneg(), ibvnego(), ibvnor(), ibvnot(), ibvor(), ibvpow(), ibvredand(), ibvredor(), ibvredxor(), ibvrepeat(), ibvroli(), ibvrori(), ibvsaddo(), ibvsdivo(), ibvsext(), ibvsge(), ibvsgt(), ibvshl(), ibvshl(), ibvshr(), ibvshr(), ibvsle(), ibvslt(), ibvsmulo(), ibvssubo(), ibvsub(), ibvuaddo(), ibvudiv(), ibvuge(), ibvugt(), ibvule(), ibvult(), ibvumulo(), ibvurem(), ibvusubo(), ibvxnor(), ibvxor(), ibvzext(), is_max_signed(), is_min_signed(), is_one(), is_ones(), is_uadd_overflow(), is_umul_overflow(), is_zero(), iset(), iset(), operator=(), set_bit(), str(), to_mpz(), to_uint64(), and ~BitVector().
| uint64_t stabilizer::util::BitVector::d_val_uint64 |
Definition at line 2209 of file bitvector.h.
Referenced by bit(), BitVector(), BitVector(), BitVector(), BitVector(), bvudivurem(), compare(), get_limb(), hash(), ibvadd(), ibvand(), ibvconcat(), ibvdec(), ibveq(), ibvextract(), ibvimplies(), ibvinc(), ibvite(), ibvmodinv(), ibvmul(), ibvnand(), ibvne(), ibvneg(), ibvnego(), ibvnor(), ibvnot(), ibvor(), ibvpow(), ibvredand(), ibvredor(), ibvredxor(), ibvrepeat(), ibvroli(), ibvrori(), ibvsaddo(), ibvsdivo(), ibvsext(), ibvsge(), ibvsgt(), ibvshl(), ibvshl(), ibvshr(), ibvshr(), ibvsle(), ibvslt(), ibvsmulo(), ibvssubo(), ibvsub(), ibvuaddo(), ibvudiv(), ibvuge(), ibvugt(), ibvule(), ibvult(), ibvumulo(), ibvurem(), ibvusubo(), ibvxnor(), ibvxor(), ibvzext(), is_max_signed(), is_min_signed(), is_one(), is_ones(), is_uadd_overflow(), is_umul_overflow(), is_zero(), iset(), iset(), operator=(), set_bit(), str(), to_mpz(), and to_uint64().
|
staticconstexpr |
Definition at line 36 of file bitvector.h.
Referenced by ibvconcat(), ibvextract(), ibvmodinv(), ibvrepeat(), ibvroli(), ibvrori(), ibvsext(), ibvzext(), is_gmp(), and mk_ones().
1.9.8