Struct ProgArray 

pub struct ProgArray {

    pub elem_ty: Ty,
    pub elem_words: usize,
    pub slot: FieldSlot,
    pub home: Home,
    pub rand: bool,
    pub prop_index: Option<usize>,
    pub elem_domain: Option<Vec<BigUint>>,
    pub assoc: bool,
    pub nested: bool,
    pub template_of: Option<u32>,
    pub inner_fixed: u32,
    pub row_depth: u32,
    pub window: Option<Window>,
}

A dynamic array or queue property of a Program (LRM 18.4, 18.5.7).

Fields

elem_ty: Ty

Element type (the solver’s 2-state view of it).

elem_words: usize

64-bit words per stored element (ceil(2 * width / 64), 4-state packed: the same layout the collection store and codegen use).

slot: FieldSlot

Where the collection handle lives, as an offset into Self::home.

home: Home

The object Self::slot is an offset into.

rand: bool

Whether the property is rand. A non-rand array a constraint reads is state.

prop_index: Option<usize>

As ProgVar::prop_index; one rand_mode bit covers the whole array.

elem_domain: Option<Vec<BigUint>>

The enum values every element must be one of, for an array of an enum type (LRM 6.19.3: a rand enum is limited to its named values).

assoc: bool

An associative array: its keys (hence its size) are never randomized, only the values at the keys it already has (LRM 18.4), so the solved values are written back by key instead of resizing a sequence.

nested: bool

An array of dynamic arrays or queues (rand int a[][], LRM 18.4): the property’s elements are row handles, and Self::elem_ty / Self::elem_words describe the leaf elements of the rows.

template_of: Option<u32>

For the row template of the array of arrays with this id (super::ir::ArrayNode::RowScope): the array exists only in the constraints, so it has no property (Self::slot and Self::home are placeholders).

inner_fixed: u32

For an array of FIXED-size rows (rand int b[][4], LRM 7.4.5): the rows’ element count N. Every row is N elements stored inline in its outer element (one flat 4-state value of N leaf elements, lowest index first) instead of a row collection handle; zero for dynamic rows.

row_depth: u32

How many levels of rows lie below the array (0 unless Self::nested): rand int a[][][] is 2. Every level but the last holds row handles (collections of handles); the last holds the leaf elements, or with Self::inner_fixed the inline fixed-size rows.

window: Option<Window>

When the collection handle is not the whole property but one leaf of an aggregate (a row of rand int a[3][], a rand queue member of an unpacked struct, LRM 18.4): where it sits in the property’s value.

Trait Implementations

impl Clone for ProgArray

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 ProgArray

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ProgArray

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for ProgArray

impl PartialEq for ProgArray

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for ProgArray

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for ProgArray