Struct ArrayState 

pub struct ArrayState {
    pub elem_ty: Ty,
    pub active: bool,
    pub cur: Vec<Option<BigUint>>,
    pub domain: Option<Vec<BigUint>>,
    pub rows: Option<RowsState>,
    pub template_of: Option<ArrayId>,
}

One array of a program as seen by one randomize() call.

Fields

elem_ty: Ty

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

active: bool

Whether the array’s elements (and size) are being randomized this call: a rand property whose rand_mode bit is set.

cur: Vec<Option<BigUint>>

The current elements; None is an element with an X/Z bit.

domain: Option<Vec<BigUint>>

The enum values an element must be one of (a rand enum array).

rows: Option<RowsState>

For an array of dynamic arrays or queues (rand int a[][]): its rows. Self::cur then holds one placeholder per row and Self::elem_ty is the leaf type; the rows’ own elements live here.

template_of: Option<ArrayId>

For a row template (ArrayNode::RowScope): the array of arrays whose rows it stands for. A template has no elements of its own.

Implementations

impl ArrayState

pub fn flat(elem_ty: Ty, active: bool, cur: Vec<Option<BigUint>>) -> ArrayState

A state holding cur, no domain and no rows.

pub fn with_domain(self, domain: Option<Vec<BigUint>>) -> ArrayState

This state with the enum values an element must be one of.

Trait Implementations

impl Clone for ArrayState

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 ArrayState

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

Formats the value using the given formatter.