Struct Array 

pub struct Array {
    pub id: TermId,
    pub domain: SortId,
    pub range: SortId,
}

An array-sorted term, analogous to z3::Array<'ctx, D, R>.

Arrays are modelled by the theory of arrays (select/store). The domain and range sorts are recorded for convenience but the authoritative sort information lives inside the TermManager.

Fields

id: TermId

The underlying term identifier.

domain: SortId

The index (domain) sort of this array.

range: SortId

The element (range) sort of this array.

Implementations

impl Array

pub fn from_id(id: TermId, domain: SortId, range: SortId) -> Self

Wrap a raw TermId as an Array with known domain/range sorts.

pub fn new_const( ctx: &Z3Context, name: &str, domain: SortId, range: SortId, ) -> Self

Declare a fresh array constant named name with the given domain/range sorts.

Creates the array sort via SortManager::array and then declares a variable of that sort.

pub fn select(ctx: &Z3Context, arr: &Array, idx: TermId) -> TermId

Select an element from arr at index idx.

Returns a raw TermId whose sort is arr.range.

pub fn store(ctx: &Z3Context, arr: &Array, idx: TermId, val: TermId) -> Array

Store val at index idx in arr, returning the updated array.

The returned Array has the same domain/range as arr.

pub fn eq(ctx: &Z3Context, lhs: &Array, rhs: &Array) -> Bool

Equality between two arrays of the same domain/range sorts.

Trait Implementations

impl Clone for Array

fn clone(&self) -> Array

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Array

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

Formats the value using the given formatter.

impl From<Array> for TermId

fn from(a: Array) -> Self

Converts to this type from the input type.