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,
}

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.

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