liblisa::smt::z3

Struct Z3Solver

pub struct Z3Solver<'ctx> { /* private fields */ }
Expand description

The Z3 SmtSolver.

Implementations§

§

impl<'ctx> Z3Solver<'ctx>

pub fn new(context: &'ctx Context) -> Self

Creates a new Z3Solver from the provided context.

pub fn context(&self) -> &'ctx Context

Returns the [z3::Context] wrapped by this struct.

pub fn solver(&self) -> &Solver<'ctx>

Returns the [z3::Solver] wrapped by this struct.

§

impl Z3Solver<'static>

pub fn with_thread_local<T>( timeout: Duration, f: impl FnOnce(Z3Solver<'_>) -> T, ) -> T

Creates a new thread-local Z3Solver.

Trait Implementations§

§

impl<'ctx> Clone for Z3Solver<'ctx>

§

fn clone(&self) -> Z3Solver<'ctx>

Returns a copy of the value. Read more
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
§

impl<'ctx> Debug for Z3Solver<'ctx>

§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more
§

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 get_size(&self) -> u32

Returns the size of the bitvector.
§

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 simplify(self) -> Self

Simplifies, if possible, the SMT expression.
§

fn bvrotr(self, count: Self) -> Self

§

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 as_u64(&self) -> Option<u64>

Converts the bitvector to an u64, if possible.
§

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bitvector into a Dynamic expression.
§

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

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>

§

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.
§

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

Returns true if both expressions are structurally identical.
§

fn select(self, index: BV<'ctx>) -> BV<'ctx>

Returns the value at the provided index in the array.
§

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

Returns the size of the bitvector elements in the array.
§

fn index_size(&self) -> u32

Returns the size of the bitvector indices in the array.
§

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bool into a Dynamic expression.
§

impl<'ctx> SmtBool<'ctx, Z3Solver<'ctx>> for Bool<'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 simplify(self) -> Self

Simplifies, if possible, the SMT expression.
§

fn _eq(self, other: Self) -> Bool<'ctx>

Returns an SMT expression that performs an equality comparison between the two bools.
§

fn as_bool(&self) -> Option<bool>

Converts the SMT boolean expression to a bool, if possible.
§

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>

Creates an If-Then-Else expression that returns booleans. Read more
§

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

Returns true if both expressions are structurally identical.
§

fn ite_dynamic(self, lhs: Dynamic<'a, S>, rhs: Dynamic<'a, S>) -> Dynamic<'a, S>

Creates an If-Then-Else expression that returns Dynamics. Read more
§

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the bool into a Dynamic expression.
§

impl<'ctx> SmtInt<'ctx, Z3Solver<'ctx>> for Int<'ctx>

§

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.
§

fn as_u64(&self) -> Option<u64>

Converts the integer to an u64, if possible.
§

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

Returns true if both expressions are structurally identical.
§

fn into_dynamic(self) -> Dynamic<'a, S>

Converts the integer into a Dynamic expression.
§

impl<'ctx> SmtModel<'ctx, Z3Solver<'ctx>> for Model<'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>

§

fn to_model(&self) -> Option<Model<'ctx>>

Convert the reference into an owned model.
§

impl<'ctx> SmtSolver<'ctx> for Z3Solver<'ctx>

§

type BV = BV<'ctx>

Bitvector expressions
§

type Int = Int<'ctx>

Integer expressions
§

type Bool = Bool<'ctx>

Boolean expressions
§

type BvArray = BvArray<'ctx>

Bitvector array expressions
§

type ModelRef<'a> = ModelRef<'a, 'ctx> where Self: 'a

References to models for satisfied assertions.
§

type Model = Model<'ctx>

Models for satisfied assertions.
§

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

Creates a bitvector from an u64.
§

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

Creates an int from a bitvector.
§

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

Declares a new bitvector constant.
§

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

Creates an SMT bool from a Rust bool.
§

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

Creates a forall condition.
§

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

Declare a new bitvector array constant.
§

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

The PEXT operation.
§

fn popcount(&mut self, bv: &Self::BV, bv_size: u32) -> Self::Int

Counts the number of ones in 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

Count the number of trailing zeros in 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> Any for T
where T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for T
where T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<T> CloneToUninit for T
where T: Clone,

source§

unsafe fn clone_to_uninit(&self, dst: *mut T)

🔬This is a nightly-only experimental API. (clone_to_uninit)
Performs copy-assignment from self to dst. Read more
source§

impl<T> DynClone for T
where T: Clone,

source§

fn __clone_box(&self, _: Private) -> *mut ()

source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

§

impl<T, W> HasTypeWitness<W> for T
where W: MakeTypeWitness<Arg = T>, T: ?Sized,

§

const WITNESS: W = W::MAKE

A constant of the type witness
§

impl<T> Identity for T
where T: ?Sized,

§

const TYPE_EQ: TypeEq<T, <T as Identity>::Type> = TypeEq::NEW

Proof that Self is the same type as Self::Type, provides methods for casting between Self and Self::Type.
§

type Type = T

The same type as Self, used to emulate type equality bounds (T == U) with associated type equality constraints (T: Identity<Type = U>).
source§

impl<T, U> Into<U> for T
where U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> IntoEither for T

source§

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 more
source§

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

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
§

impl<T> Pointable for T

§

const ALIGN: usize = _

The alignment of pointer.
§

type Init = T

The type for initializers.
§

unsafe fn init(init: <T as Pointable>::Init) -> usize

Initializes a with the given initializer. Read more
§

unsafe fn deref<'a>(ptr: usize) -> &'a T

Dereferences the given pointer. Read more
§

unsafe fn deref_mut<'a>(ptr: usize) -> &'a mut T

Mutably dereferences the given pointer. Read more
§

unsafe fn drop(ptr: usize)

Drops the object pointed to by the given pointer. Read more
source§

impl<T> Same for T

source§

type Output = T

Should always be Self
source§

impl<T> ToOwned for T
where T: Clone,

source§

type Owned = T

The resulting type after obtaining ownership.
source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

source§

type Error = Infallible

The type returned in the event of a conversion error.
source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<V, T> VZip<V> for T
where V: MultiLane<T>,

§

fn vzip(self) -> V