Struct Z3Solver
pub struct Z3Solver<'ctx> { /* private fields */ }
Expand description
The Z3 SmtSolver
.
Implementations§
Trait Implementations§
§impl<'ctx> SmtBV<'ctx, Z3Solver<'ctx>> for BV<'ctx>
impl<'ctx> SmtBV<'ctx, Z3Solver<'ctx>> for BV<'ctx>
fn concat(self, other: Self) -> Self
fn extract(self, hi: u32, lo: u32) -> Self
fn zero_ext(self, num: u32) -> Self
fn sign_ext(self, num: u32) -> Self
fn bvshl(self, count: Self) -> Self
fn bvlshr(self, count: Self) -> Self
fn bvashr(self, count: Self) -> Self
§fn _eq(self, other: Self) -> Bool<'ctx>
fn _eq(self, other: Self) -> Bool<'ctx>
Returns an SMT expression that performs an equality comparison between the two bitvectors.
fn bvurem(self, n: Self) -> Self
fn bvsrem(self, n: Self) -> Self
fn bvudiv(self, n: Self) -> Self
fn bvsdiv(self, n: Self) -> Self
fn bvrotl(self, count: Self) -> Self
fn bvslt(self, other: Self) -> Bool<'ctx>
fn bvsge(self, other: Self) -> Bool<'ctx>
fn bvrotr(self, count: Self) -> Self
§fn is_identical(&self, other: &Self) -> bool
fn is_identical(&self, other: &Self) -> bool
Returns true if both expressions are structurally identical.
fn bvsgt(self, other: Self) -> Bool<'ctx>
fn bvugt(self, other: Self) -> Bool<'ctx>
fn bvult(self, other: Self) -> Bool<'ctx>
fn bvule(self, other: Self) -> Bool<'ctx>
fn bvuge(self, other: Self) -> Bool<'ctx>
§fn into_dynamic(self) -> Dynamic<'a, S>
fn into_dynamic(self) -> Dynamic<'a, S>
Converts the bitvector into a
Dynamic
expression.§fn swap_bytes(self, num_bytes: usize) -> Self
fn swap_bytes(self, num_bytes: usize) -> Self
Swaps the lowest
num_bytes
in the bitvector.§fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self
fn swap_bytes_to_128bits(self, num_bytes: usize) -> Self
Swaps the lowest
num_bytes
in the bitvector, and zero-extends to an 128-bit bitvector.§impl<'ctx> SmtBVArray<'ctx, Z3Solver<'ctx>> for BvArray<'ctx>
impl<'ctx> SmtBVArray<'ctx, Z3Solver<'ctx>> for BvArray<'ctx>
§fn _eq(self, other: Self) -> Bool<'ctx>
fn _eq(self, other: Self) -> Bool<'ctx>
Returns an SMT expression that performs an equality comparison between the two bools.
§fn is_identical(&self, other: &Self) -> bool
fn is_identical(&self, other: &Self) -> bool
Returns true if both expressions are structurally identical.
§fn store(self, index: BV<'ctx>, value: BV<'ctx>) -> Self
fn store(self, index: BV<'ctx>, value: BV<'ctx>) -> Self
Returns an updated array that contains
value
at index index
.§fn element_size(&self) -> u32
fn element_size(&self) -> u32
Returns the size of the bitvector elements in the array.
§fn index_size(&self) -> u32
fn index_size(&self) -> u32
Returns the size of the bitvector indices in the array.
§fn into_dynamic(self) -> Dynamic<'a, S>
fn into_dynamic(self) -> Dynamic<'a, S>
Converts the bool into a
Dynamic
expression.§impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'ctx>
impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'ctx>
§fn ite_bv(self, lhs: BV<'ctx>, rhs: BV<'ctx>) -> BV<'ctx>
fn ite_bv(self, lhs: BV<'ctx>, rhs: BV<'ctx>) -> BV<'ctx>
Creates an If-Then-Else expression that returns bitvectors. Read more
§fn _eq(self, other: Self) -> Bool<'ctx>
fn _eq(self, other: Self) -> Bool<'ctx>
Returns an SMT expression that performs an equality comparison between the two bools.
§fn ite_int(self, lhs: Int<'ctx>, rhs: Int<'ctx>) -> Int<'ctx>
fn ite_int(self, lhs: Int<'ctx>, rhs: Int<'ctx>) -> Int<'ctx>
Creates an If-Then-Else expression that returns integers. Read more
§fn ite_bool(self, lhs: Bool<'ctx>, rhs: Bool<'ctx>) -> Bool<'ctx>
fn ite_bool(self, lhs: Bool<'ctx>, rhs: Bool<'ctx>) -> Bool<'ctx>
Creates an If-Then-Else expression that returns booleans. Read more
§fn ite_bv_array(self, lhs: BvArray<'ctx>, rhs: BvArray<'ctx>) -> BvArray<'ctx>
fn ite_bv_array(self, lhs: BvArray<'ctx>, rhs: BvArray<'ctx>) -> BvArray<'ctx>
Creates an If-Then-Else expression that returns bitvector arrays. Read more
§fn is_identical(&self, other: &Self) -> bool
fn is_identical(&self, other: &Self) -> bool
Returns true if both expressions are structurally identical.
§fn ite_dynamic(self, lhs: Dynamic<'a, S>, rhs: Dynamic<'a, S>) -> Dynamic<'a, S>
fn ite_dynamic(self, lhs: Dynamic<'a, S>, rhs: Dynamic<'a, S>) -> Dynamic<'a, S>
§fn into_dynamic(self) -> Dynamic<'a, S>
fn into_dynamic(self) -> Dynamic<'a, S>
Converts the bool into a
Dynamic
expression.§impl<'ctx> SmtInt<'ctx, Z3Solver<'ctx>> for Int<'ctx>
impl<'ctx> SmtInt<'ctx, Z3Solver<'ctx>> for Int<'ctx>
§fn _eq(self, other: Self) -> Bool<'ctx>
fn _eq(self, other: Self) -> Bool<'ctx>
Returns an SMT expression that performs an equality comparison between the two ints.
§fn is_identical(&self, other: &Self) -> bool
fn is_identical(&self, other: &Self) -> bool
Returns true if both expressions are structurally identical.
§fn into_dynamic(self) -> Dynamic<'a, S>
fn into_dynamic(self) -> Dynamic<'a, S>
Converts the integer into a
Dynamic
expression.§impl<'ctx> SmtModel<'ctx, Z3Solver<'ctx>> for Model<'ctx>
impl<'ctx> SmtModel<'ctx, Z3Solver<'ctx>> for Model<'ctx>
§fn get_const_interp(&self, name: &BV<'ctx>) -> Option<BV<'ctx>>
fn get_const_interp(&self, name: &BV<'ctx>) -> Option<BV<'ctx>>
Obtain the value for a constant in the model.
§impl<'ctx> SmtModelRef<'ctx, Z3Solver<'ctx>> for ModelRef<'_, 'ctx>
impl<'ctx> SmtModelRef<'ctx, Z3Solver<'ctx>> for ModelRef<'_, 'ctx>
§impl<'ctx> SmtSolver<'ctx> for Z3Solver<'ctx>
impl<'ctx> SmtSolver<'ctx> for Z3Solver<'ctx>
§type ModelRef<'a> = ModelRef<'a, 'ctx>
where
Self: 'a
type ModelRef<'a> = ModelRef<'a, 'ctx> where Self: 'a
References to models for satisfied assertions.
§fn bv_from_i64(&mut self, val: i64, size: u32) -> Self::BV
fn bv_from_i64(&mut self, val: i64, size: u32) -> Self::BV
Creates a bitvector from an i64.
§fn bv_from_u64(&mut self, val: u64, size: u32) -> Self::BV
fn bv_from_u64(&mut self, val: u64, size: u32) -> Self::BV
Creates a bitvector from an u64.
§fn int_from_i64(&mut self, val: i64) -> Self::Int
fn int_from_i64(&mut self, val: i64) -> Self::Int
Creates an int from an i64.
§fn int_from_bv(&mut self, bv: Self::BV, signed: bool) -> Self::Int
fn int_from_bv(&mut self, bv: Self::BV, signed: bool) -> Self::Int
Creates an int from a bitvector.
§fn bv_from_int(&mut self, int: Self::Int, size: u32) -> Self::BV
fn bv_from_int(&mut self, int: Self::Int, size: u32) -> Self::BV
Creates a bitvector from an Int.
§fn new_bv_const(&mut self, name: impl AsRef<str>, size: u32) -> Self::BV
fn new_bv_const(&mut self, name: impl AsRef<str>, size: u32) -> Self::BV
Declares a new bitvector constant.
§fn check_assertions(
&mut self,
assertions: &[Self::Bool],
) -> SatResult<Self::ModelRef<'_>>
fn check_assertions( &mut self, assertions: &[Self::Bool], ) -> SatResult<Self::ModelRef<'_>>
Runs the SMT solver on the provided assertions.
§fn bool_from_bool(&mut self, val: bool) -> Self::Bool
fn bool_from_bool(&mut self, val: bool) -> Self::Bool
Creates an SMT bool from a Rust bool.
§fn int_from_u64(&mut self, val: u64) -> Self::Int
fn int_from_u64(&mut self, val: u64) -> Self::Int
Creates an int from an u64.
§fn forall_const(
&mut self,
vals: &[Dynamic<'ctx, Self>],
condition: Self::Bool,
) -> Self::Bool
fn forall_const( &mut self, vals: &[Dynamic<'ctx, Self>], condition: Self::Bool, ) -> Self::Bool
Creates a forall condition.
§fn new_bool_const(&mut self, name: impl AsRef<str>) -> Self::Bool
fn new_bool_const(&mut self, name: impl AsRef<str>) -> Self::Bool
Declares a new boolean constant.
§fn new_bv_array_const(
&mut self,
name: impl AsRef<str>,
index_size: u32,
element_size: u32,
) -> Self::BvArray
fn new_bv_array_const( &mut self, name: impl AsRef<str>, index_size: u32, element_size: u32, ) -> Self::BvArray
Declare a new bitvector array constant.
§fn bv_from_i128(&mut self, value: i128) -> Self::BV
fn bv_from_i128(&mut self, value: i128) -> Self::BV
Creates a bitvector from an i128.
§fn extract_bits<const N: u32>(
&mut self,
src: Self::BV,
mask: Self::BV,
) -> Self::BV
fn extract_bits<const N: u32>( &mut self, src: Self::BV, mask: Self::BV, ) -> Self::BV
The PEXT operation.
§fn deposit_bits<const N: u32>(
&mut self,
src: Self::BV,
mask: Self::BV,
) -> Self::BV
fn deposit_bits<const N: u32>( &mut self, src: Self::BV, mask: Self::BV, ) -> Self::BV
The PDEP operation.
§fn count_trailing_zeros(&mut self, bv: Self::BV) -> Self::BV
fn count_trailing_zeros(&mut self, bv: Self::BV) -> Self::BV
Count the number of trailing zeros in
bv
.§fn count_leading_zeros(&mut self, bv: Self::BV) -> Self::BV
fn count_leading_zeros(&mut self, bv: Self::BV) -> Self::BV
Count the number of leading zeros in
bv
.Auto Trait Implementations§
impl<'ctx> Freeze for Z3Solver<'ctx>
impl<'ctx> RefUnwindSafe for Z3Solver<'ctx>
impl<'ctx> !Send for Z3Solver<'ctx>
impl<'ctx> !Sync for Z3Solver<'ctx>
impl<'ctx> Unpin for Z3Solver<'ctx>
impl<'ctx> UnwindSafe for Z3Solver<'ctx>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
source§unsafe fn clone_to_uninit(&self, dst: *mut T)
unsafe fn clone_to_uninit(&self, dst: *mut T)
🔬This is a nightly-only experimental API. (
clone_to_uninit
)§impl<T> Identity for Twhere
T: ?Sized,
impl<T> Identity for Twhere
T: ?Sized,
source§impl<T> IntoEither for T
impl<T> IntoEither for T
source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left
is true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read moresource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self
into a Left
variant of Either<Self, Self>
if into_left(&self)
returns true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read more