Struct ArrayInfo 

pub struct ArrayInfo {
    pub symbol: SymbolId,
    pub name: String,
    pub elem_ty: Ty,
    pub rand: bool,
    pub elem_domain: Option<Vec<BigUint>>,
    pub assoc: bool,
    pub nested: bool,
    pub template_of: Option<ArrayId>,
    pub inner_fixed: u32,
    pub row_depth: u32,
    pub window: Option<Window>,
}

A dynamic array or queue the constraints reach.

Fields

symbol: SymbolId

The property’s key.

name: String

Its declared name.

elem_ty: Ty

The element type (a 4-state element is solved as 2-state).

rand: bool

Whether the property is rand: its size and elements are then random variables of the program (an inactive rand_mode is decided at run time). A non-rand array a constraint reads is state.

elem_domain: Option<Vec<BigUint>>

For an array of an enum type, the named constants every element takes (LRM 6.19.3, 18.3).

assoc: bool

An associative array (only ever rand, and only its existing values are drawn: no constraint can name it, 18.4).

nested: bool

An array of dynamic arrays or queues (rand int a[][], 18.4): its elements are rows, and Self::elem_ty / Self::elem_domain describe the leaf elements of the rows.

template_of: Option<ArrayId>

For the row template of an array of arrays (ArrayNode::RowScope): that array. A template is not a property; it is how a constraint names “the row a[i] selects”.

inner_fixed: u32

For an array of fixed-size rows (rand int b[][4]): the row length N; every row is pinned to N elements by an implicit constraint and stored inline in its outer element. Zero for dynamic rows.

row_depth: u32

How many levels of rows lie below this array: 0 for a plain dynamic array or queue, 1 for int a[][] / int b[][4], 2 for int a[][][]. Zero exactly when Self::nested is false. A row template has one level fewer than the array it is the template of.

window: Option<Window>

Where the array’s handle sits in its property when it is a leaf of an aggregate (a row of rand int a[3][], a queue member of a struct).

Trait Implementations

impl Clone for ArrayInfo

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ArrayInfo

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

Formats the value using the given formatter.

impl Eq for ArrayInfo

impl PartialEq for ArrayInfo

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

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for ArrayInfo