Struct Expanded 

pub struct Expanded {
    pub conjuncts: Vec<Expr>,
    pub elem_vars: Vec<(ArrayId, usize)>,
    pub elem_tys: Vec<Ty>,
    pub extra_states: Vec<Option<BigUint>>,
    pub extra_dists: Vec<Dist>,
}

The result of expand.

Fields

conjuncts: Vec<Expr>

Scalar constraints over the field variables 0..n_vars0 and the element variables n_vars0...

elem_vars: Vec<(ArrayId, usize)>

Element variable n_vars0 + k is (array, index) of elem_vars[k].

elem_tys: Vec<Ty>

Types of the element variables.

extra_states: Vec<Option<BigUint>>

State values appended after the caller’s states (an element of an inactive or non-rand array).

extra_dists: Vec<Dist>

The instances of the program’s dist templates (Dist::subject), one per iteration that met one. The instance k has the selector SELECTOR_BASE + n_program_dists + k, and its variable ids are already the expansion’s (element variables numbered after the field variables).

Trait Implementations

impl Clone for Expanded

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 Expanded

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

Formats the value using the given formatter.

impl Default for Expanded

fn default() -> Self

Returns the “default value” for a type.