Trait SmtBVArray

pub trait SmtBVArray<'a, S: SmtSolver<'a, BvArray = Self>>:
    Clone
    + Debug
    + Display {
    // Required methods
    fn is_identical(&self, other: &Self) -> bool;
    fn _eq(self, other: Self) -> S::Bool;
    fn simplify(self) -> Self;
    fn select(self, index: S::BV) -> S::BV;
    fn store(self, index: S::BV, value: S::BV) -> S::BvArray;
    fn element_size(&self) -> u32;
    fn index_size(&self) -> u32;

    // Provided method
    fn into_dynamic(self) -> Dynamic<'a, S> { ... }
}

Array expressions in the SMT solver.

Required Methods

fn is_identical(&self, other: &Self) -> bool

Returns true if both expressions are structurally identical.

fn _eq(self, other: Self) -> S::Bool

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

fn simplify(self) -> Self

Simplifies, if possible, the SMT expression.

fn select(self, index: S::BV) -> S::BV

Returns the value at the provided index in the array.

fn store(self, index: S::BV, value: S::BV) -> S::BvArray

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.

Provided Methods

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

Converts the bool into a Dynamic expression.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<'ctx> SmtBVArray<'ctx, Z3Solver<'ctx>> for BvArray<'ctx>

impl<'ctx, S: SmtSolver<'ctx> + 'ctx, C: SolverCache> SmtBVArray<'ctx, CachedSolver<'ctx, S, C>> for CacheBVArray<'ctx, S>