Enum ArrayNode 

pub enum ArrayNode {
    Size(ArrayId),
    Elem {
        array: ArrayId,
        index: Box<Expr>,
        ty: Ty,
    },
    Loop(LoopId, Ty),
    Foreach {
        array: ArrayId,
        var: LoopId,
        body: Box<Expr>,
    },
    Reduce {
        op: ReduceOp,
        array: ArrayId,
        var: LoopId,
        index_var: LoopId,
        body: Box<Expr>,
    },
    Call {
        func: FuncId,
        args: Vec<Expr>,
        ty: Ty,
    },
    Pick {
        index: Box<Expr>,
        low: i64,
        elems: Vec<Expr>,
        ty: Ty,
    },
    Distinct {
        scalars: Vec<Expr>,
        arrays: Vec<ArrayId>,
    },
    RowScope {
        template: ArrayId,
        row: Box<Expr>,
        body: Box<Expr>,
    },
}

The array-level IR nodes (see Expr::Array).

Variants

Size(ArrayId)

A.size(): the array’s length, s[32].

Elem

A[index] (LRM 18.5.7.1). After loop-variable substitution the index must be free of random variables (the builder rejects the rest).

Fields

array: ArrayId

The indexed array.

index: Box<Expr>

The index expression.

ty: Ty

The element type.

Loop(LoopId, Ty)

The current value of a foreach loop variable or reduction iterator.

Foreach

foreach (A[i]) body: body holds for every index i of A. One bit. The body reads the index as Loop(var, s[32]).

Fields

array: ArrayId

The iterated array.

var: LoopId

The loop variable.

body: Box<Expr>

The constraint body (a boolean expression).

Reduce

A.op() with (body): the reduction of body over every element, read as Loop(var, elem_ty) for the item and Loop(idx, s[32]) for item.index. The body’s type is the result type.

Fields

op: ReduceOp

The reduction.

array: ArrayId

The reduced array.

var: LoopId

The item binding.

index_var: LoopId

The item.index binding.

body: Box<Expr>

The per-element expression (the item itself without a with).

Call

A call of a user function (LRM 18.5.11), func indexing the program’s function table (super::func). Like the nodes above it is resolved before the solver sees the tree: once its arguments are constants the call is evaluated and replaced by the constant it returns (the return value is a state variable of the constraint that holds it).

Fields

func: FuncId

The called function.

args: Vec<Expr>

The actual arguments, one per formal, already converted to the formal’s type.

ty: Ty

The return type.

Pick

A[index] over a fixed-size unpacked array held in a class property (LRM 7.4, 18.4): every element is its own variable or state, and the element read is the one the index names. The index is a constant, a state or a loop variable, so it is known once the node is expanded; only the chosen element is expanded, so an index outside the array is an error only when this node is live (LRM 18.5.7.1: the user excludes such indices with a guard).

Fields

index: Box<Expr>

The index expression.

low: i64

The array’s lowest declared index: elems[i - low] is element i.

elems: Vec<Expr>

The elements, lowest declared index first; all of type ty.

ty: Ty

The element type.

Distinct

unique { m0, m1, ... } (LRM 18.5.4) whose group holds a whole dynamic array or queue, whose length is known only at run time: true iff no two of the scalars and of every element of every array in arrays hold the same value. One bit. Expansion replaces it with the Expr::AllDistinct over the scalars followed by each array’s elements (a group of fewer than two members is simply true).

Fields

scalars: Vec<Expr>

The singular members (variables or states of the element type).

arrays: Vec<ArrayId>

The dynamic arrays or queues whose every element is a member.

RowScope

body read with the row array template standing for row row of the array of arrays that template is the row template of (LRM 18.4, 7.4.5: a[i].size, a[i][j], a[i].sum() over rand int a[][]). The row arrays of an array of dynamic arrays or queues are not known when the constraints are built (the outer size is solved first, then every row gets its own size and elements), so body is ordinary one-dimensional array IR over template, and expansion rebinds template to the concrete row array of the row row names once the outer size is fixed (super::array::lower_rows). row is free of random variables, like an element index.

Fields

template: ArrayId

The row template: a program array that only stands for “the row”.

row: Box<Expr>

The row index (an index into the outer array).

body: Box<Expr>

The expression over template.

Implementations

impl ArrayNode

pub fn ty(&self) -> Ty

The result type of this node.

pub fn for_each_child(&self, f: &mut impl FnMut(&Expr))

Calls f on every direct sub-expression.

pub fn map_children(&self, f: &mut impl FnMut(&Expr) -> Expr) -> ArrayNode

A copy with every direct sub-expression replaced by f(child).

Trait Implementations

impl Clone for ArrayNode

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 ArrayNode

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ArrayNode

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for ArrayNode

impl Hash for ArrayNode

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for ArrayNode

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for ArrayNode

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 ArrayNode