pub struct BV<'ctx> { /* fields omitted */ }
Expand description
Ast
node representing a bitvector value.
Create a bit vector from an integer.
The bit vector will have width sz
.
let i = ast::Int::new_const(&ctx, "x");
solver.assert(&i._eq(&ast::Int::from_i64(&ctx, -3)));
let x = ast::BV::from_int(&i, 64);
assert_eq!(64, x.get_size());
assert_eq!(solver.check(), SatResult::Sat);
let model = solver.get_model().unwrap();;
assert_eq!(-3, model.eval(&x.to_int(true), true).unwrap().as_i64().expect("as_i64() shouldn't fail"));
Create an integer from a bitvector.
This is just a convenience wrapper around
Int::from_bv
; see notes there
Get the size of the bitvector (in bits)
pub fn bvnot(&self) -> Self
pub fn bvneg(&self) -> Self
Two’s complement negation
Conjunction of all the bits in the vector. Returns a BV with size (bitwidth) 1.
Disjunction of all the bits in the vector. Returns a BV with size (bitwidth) 1.
pub fn bvand(&self, other: &Self) -> Self
pub fn bvor(&self, other: &Self) -> Self
pub fn bvxor(&self, other: &Self) -> Self
pub fn bvnand(&self, other: &Self) -> Self
pub fn bvnor(&self, other: &Self) -> Self
pub fn bvxnor(&self, other: &Self) -> Self
pub fn bvadd(&self, other: &Self) -> Self
pub fn bvsub(&self, other: &Self) -> Self
pub fn bvmul(&self, other: &Self) -> Self
pub fn bvudiv(&self, other: &Self) -> Self
pub fn bvsdiv(&self, other: &Self) -> Self
pub fn bvurem(&self, other: &Self) -> Self
pub fn bvsrem(&self, other: &Self) -> Self
Signed remainder (sign follows dividend)
pub fn bvsmod(&self, other: &Self) -> Self
Signed remainder (sign follows divisor)
Unsigned less than or equal
Signed less than or equal
Unsigned greater or equal
pub fn bvshl(&self, other: &Self) -> Self
pub fn bvlshr(&self, other: &Self) -> Self
Logical shift right (add zeroes in the high bits)
pub fn bvashr(&self, other: &Self) -> Self
Arithmetic shift right (sign-extend in the high bits)
pub fn bvrotl(&self, other: &Self) -> Self
pub fn bvrotr(&self, other: &Self) -> Self
pub fn concat(&self, other: &Self) -> Self
Concatenate two bitvectors
Check if negation overflows
Check if addition overflows
Check if subtraction underflows
Check if multiplication overflows
Check if addition underflows
Check if subtraction overflows
Check if signed division overflows
Check if multiplication underflows
Extract the bits high
down to low
from the bitvector.
Returns a bitvector of size n
, where n = high - low + 1
.
Sign-extend the bitvector to size m+i
, where m
is the original size of the bitvector.
That is, i
bits will be added.
Zero-extend the bitvector to size m+i
, where m
is the original size of the bitvector.
That is, i
bits will be added.
impl<'a, 'ctx> Add<&'a BV<'ctx>> for BV<'ctx>
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<&'a BV<'ctx>> for u64
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<&'a BV<'ctx>> for i64
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<BV<'ctx>> for BV<'ctx>
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<i64> for &'a BV<'ctx>
The resulting type after applying the +
operator.
The resulting type after applying the +
operator.
impl<'a, 'ctx> Add<u64> for &'a BV<'ctx>
The resulting type after applying the +
operator.
impl<'ctx> Ast<'ctx> for BV<'ctx>
Compare this Ast
with another Ast
, and get a Bool
representing the result. Read more
Compare this Ast
with another Ast
, and get a Result. Errors if the sort does not
match for the two values. Read more
Compare this Ast
with a list of other Ast
s, and get a Bool
which is true only if all arguments (including Self) are pairwise distinct. Read more
Simplify the Ast
. Returns a new Ast
which is equivalent,
but simplified using algebraic simplification rules, such as
constant propagation. Read more
Performs substitution on the Ast
. The slice substitutions
contains a
list of pairs with a “from” Ast
that will be substituted by a “to” Ast
. Read more
Return the number of children of this Ast
. Read more
Return the children of this node as a Vec<Dynamic>
.
Return the AstKind
for this Ast
.
Return true
if this is a Z3 function application. Read more
Return true
if this is a Z3 constant. Read more
The resulting type after applying the &
operator.
impl<'a, 'ctx> BitAnd<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
The resulting type after applying the &
operator.
impl<'a, 'ctx> BitOr<&'a BV<'ctx>> for BV<'ctx>
The resulting type after applying the |
operator.
impl<'a, 'ctx> BitOr<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
impl<'a, 'ctx> BitOr<BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the |
operator.
The resulting type after applying the ^
operator.
impl<'a, 'ctx> BitXor<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
The resulting type after applying the ^
operator.
Performs copy-assignment from source
. Read more
Formats the value using the given formatter. Read more
Formats the value using the given formatter. Read more
Executes the destructor for this type. Read more
fn from(ast: BV<'ctx>) -> Self
fn from(ast: BV<'ctx>) -> Self
impl<'a, 'ctx> Mul<&'a BV<'ctx>> for BV<'ctx>
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<&'a BV<'ctx>> for u64
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<&'a BV<'ctx>> for i64
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<BV<'ctx>> for BV<'ctx>
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<i64> for &'a BV<'ctx>
The resulting type after applying the *
operator.
The resulting type after applying the *
operator.
impl<'a, 'ctx> Mul<u64> for &'a BV<'ctx>
The resulting type after applying the *
operator.
impl<'a, 'ctx> Neg for BV<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Neg for &'a BV<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Not for BV<'ctx>
The resulting type after applying the !
operator.
impl<'a, 'ctx> Not for &'a BV<'ctx>
The resulting type after applying the !
operator.
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
This method tests for !=
.
impl<'a, 'ctx> Shl<&'a BV<'ctx>> for BV<'ctx>
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<&'a BV<'ctx>> for u64
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<&'a BV<'ctx>> for i64
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<BV<'ctx>> for BV<'ctx>
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the <<
operator.
The resulting type after applying the <<
operator.
The resulting type after applying the <<
operator.
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<i64> for &'a BV<'ctx>
The resulting type after applying the <<
operator.
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Shl<u64> for &'a BV<'ctx>
The resulting type after applying the <<
operator.
impl<'a, 'ctx> Sub<&'a BV<'ctx>> for BV<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<&'a BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<&'a BV<'ctx>> for u64
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<&'a BV<'ctx>> for i64
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<BV<'ctx>> for BV<'ctx>
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<BV<'ctx>> for &'a BV<'ctx>
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<i64> for &'a BV<'ctx>
The resulting type after applying the -
operator.
The resulting type after applying the -
operator.
impl<'a, 'ctx> Sub<u64> for &'a BV<'ctx>
The resulting type after applying the -
operator.
The type returned in the event of a conversion error.
impl<'ctx> Eq for BV<'ctx>
impl<T> Any for T where
T: 'static + ?Sized,
Immutably borrows from an owned value. Read more
Mutably borrows from an owned value. Read more
impl<T, U> Into<U> for T where
U: From<T>,
The resulting type after obtaining ownership.
Creates owned data from borrowed data, usually by cloning. Read more
🔬 This is a nightly-only experimental API. (toowned_clone_into
)
recently added
Uses borrowed data to replace owned data, usually by cloning. Read more
Converts the given value to a String
. Read more
The type returned in the event of a conversion error.
The type returned in the event of a conversion error.