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

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.

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