Struct z3::ast::BV[][src]

pub struct BV<'ctx> { /* fields omitted */ }
Expand description

Ast node representing a bitvector value.

Implementations

Create a bit vector from an integer.

The bit vector will have width sz.

Examples

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)

Bitwise negation

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.

Bitwise and

Bitwise or

Bitwise exclusive-or

Bitwise nand

Bitwise nor

Bitwise xnor

Addition

Subtraction

Multiplication

Unsigned division

Signed division

Unsigned remainder

Signed remainder (sign follows dividend)

Signed remainder (sign follows divisor)

Unsigned less than

Signed less than

Unsigned less than or equal

Signed less than or equal

Unsigned greater or equal

Signed greater or equal

Unsigned greater than

Signed greater than

Shift left

Logical shift right (add zeroes in the high bits)

Arithmetic shift right (sign-extend in the high bits)

Rotate left

Rotate right

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.

Trait Implementations

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

The resulting type after applying the + operator.

Performs the + operation. Read more

Performs the += operation. Read more

Performs the += operation. Read more

Performs the += operation. Read more

Performs the += operation. Read more

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 Asts, and get a Bool which is true only if all arguments (including Self) are pairwise distinct. Read more

Get the Sort of the Ast

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 nth child 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

Return the FuncDecl of the Ast. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

The resulting type after applying the & operator.

Performs the & operation. Read more

Performs the &= operation. Read more

Performs the &= operation. Read more

Performs the &= operation. Read more

Performs the &= operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

The resulting type after applying the | operator.

Performs the | operation. Read more

Performs the |= operation. Read more

Performs the |= operation. Read more

Performs the |= operation. Read more

Performs the |= operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

The resulting type after applying the ^ operator.

Performs the ^ operation. Read more

Performs the ^= operation. Read more

Performs the ^= operation. Read more

Performs the ^= operation. Read more

Performs the ^= operation. Read more

Returns a copy of the value. Read more

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

Performs the conversion.

Performs the conversion.

Feeds this value into the given Hasher. Read more

Feeds a slice of this type into the given Hasher. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

The resulting type after applying the * operator.

Performs the * operation. Read more

Performs the *= operation. Read more

Performs the *= operation. Read more

Performs the *= operation. Read more

Performs the *= operation. Read more

The resulting type after applying the - operator.

Performs the unary - operation. Read more

The resulting type after applying the - operator.

Performs the unary - operation. Read more

The resulting type after applying the ! operator.

Performs the unary ! operation. Read more

The resulting type after applying the ! operator.

Performs the unary ! operation. Read more

This method tests for self and other values to be equal, and is used by ==. Read more

This method tests for !=.

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

The resulting type after applying the << operator.

Performs the << operation. Read more

Performs the <<= operation. Read more

Performs the <<= operation. Read more

Performs the <<= operation. Read more

Performs the <<= operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

The resulting type after applying the - operator.

Performs the - operation. Read more

Performs the -= operation. Read more

Performs the -= operation. Read more

Performs the -= operation. Read more

Performs the -= operation. Read more

The type returned in the event of a conversion error.

Performs the conversion.

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Performs the conversion.

Performs the conversion.

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.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.