Struct BvArray

pub struct BvArray<'ctx> { /* private fields */ }

A Z3 Array.

Implementations

impl<'ctx> BvArray<'ctx>

pub fn from_z3(array: Array<'ctx>, element_size: u32, index_size: u32) -> Self

Wraps a [z3::ast::Array].

pub fn as_z3(&self) -> &Array<'_>

Returns the wrapped [z3::ast::Array].

Trait Implementations

impl<'ctx> Clone for BvArray<'ctx>

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

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx> Debug for BvArray<'ctx>

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

Formats the value using the given formatter.

impl Display for BvArray<'_>

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

Formats the value using the given formatter.

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.