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

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).

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