vj-sim 0.3.0

//! Array constraints for the [`Builder`] (plan tasks C11, C12, C14; IEEE
//! 1800-2023 18.4, 18.5.7).
//!
//! A `rand` dynamic array or queue property is one *array* of the program
//! ([`ArrayInfo`]); constraints over it build array-level IR
//! ([`ArrayNode`]) that does not yet know how many elements the array has, and
//! the run-time expansion ([`super::super::array`]) turns that into scalar IR
//! once the sizes are decided:
//!
//! * `A.size` / `A.size()` is [`ArrayNode::Size`] (18.4: a size constraint
//!   resizes the array);
//! * `A[i]` is [`ArrayNode::Elem`]; the index is a constant, a state variable,
//!   a loop variable or the array size, never a random variable (the elements
//!   are the random variables, so a random index would be a selection among
//!   them: [`BuildError::BadArray`]);
//! * `foreach (A[i]) body` is [`ArrayNode::Foreach`] over a loop variable the
//!   body reads as [`ArrayNode::Loop`] (18.5.7.1). The loop variable's name is
//!   not in the semantic tree, so it is recovered from the syntax tree;
//! * `A.sum() with (e)` (and `product`, `and`, `or`, `xor`) is
//!   [`ArrayNode::Reduce`] (18.5.7.2), its `item` and `item.index` bound the
//!   same way.
//!
//! A `foreach` over a *packed* value or a fixed-size unpacked array with
//! declared elements has a size known now, so it unrolls immediately with the
//! loop variable a constant.
//!
//! # Limits (each a typed error, never a silent drop)
//!
//! * A multi-dimensional `foreach` unrolls only over fixed-size dimensions; an array of
//!   dynamic arrays, a dynamic dimension in `foreach (m[i, j])` and a `randc` array are
//!   [`BuildError::Unsupported`].
//! * Elements are integral (packed structs included, 18.4: a packed struct is
//!   one variable); an unpacked-struct or class-handle element is
//!   [`BuildError::NonIntegral`].
//! * An associative array has no randomizable size or index (18.4): a `rand`
//!   one has its existing values redrawn (and nothing else), and any
//!   constraint on its size or elements is [`BuildError::BadArray`].
//! * A `dist`, `solve ... before` or real constraint inside a `foreach` body
//!   (it would have to be one per element) and a `dist` over array elements
//!   are [`BuildError::Unsupported`].

use super::aggregate::{RawStep, Sel, aggregate_chain};
use super::real::strip_conversions;
use super::*;
use crate::constraints::ir::{ArrayId, ArrayNode, LoopId, ReduceOp};
use sv_lang::KnownSystemName;
use sv_lang::kinds::SymbolKind;
use sv_lang::nodes::LoopConstraintSyntax;

/// A dynamic array or queue the constraints reach.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct ArrayInfo {
    /// The property's key.
    pub symbol: SymbolId,
    /// Its declared name.
    pub name: String,
    /// The element type (a 4-state element is solved as 2-state).
    pub elem_ty: Ty,
    /// 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.
    pub rand: bool,
    /// For an array of an enum type, the named constants every element takes
    /// (LRM 6.19.3, 18.3).
    pub elem_domain: Option<Vec<BigUint>>,
    /// An associative array (only ever `rand`, and only its existing values
    /// are drawn: no constraint can name it, 18.4).
    pub assoc: bool,
    /// An array of dynamic arrays or queues (`rand int a[][]`, 18.4): its
    /// elements are rows, and [`Self::elem_ty`] / [`Self::elem_domain`] describe
    /// the leaf elements of the rows.
    pub nested: bool,
    /// For the row template of an array of arrays ([`ArrayNode::RowScope`]):
    /// that array. A template is not a property; it is how a constraint names
    /// "the row `a[i]` selects".
    pub template_of: Option<ArrayId>,
    /// For an array of fixed-size rows (`rand int b[][4]`): the row length `N`;
    /// every row is pinned to `N` elements by an implicit constraint and stored
    /// inline in its outer element. Zero for dynamic rows.
    pub inner_fixed: u32,
    /// How many levels of rows lie below this array: 0 for a plain dynamic
    /// array or queue, 1 for `int a[][]` / `int b[][4]`, 2 for `int a[][][]`.
    /// Zero exactly when [`Self::nested`] is false. A row template has one
    /// level fewer than the array it is the template of.
    pub row_depth: u32,
    /// Where the array's handle sits in its property when it is a leaf of an
    /// aggregate (a row of `rand int a[3][]`, a queue member of a struct).
    pub window: Option<Window>,
}

/// The shape of the array `e` names. A row `b[i]` of `rand int b[][4]` is
/// stored inline but is one row of the outer array's template, so it counts as
/// a dynamic array like any other row.
pub(super) fn expr_shape(e: Expression<'_>) -> Option<ArrayShape> {
    let shape = array_shape(e.expr_type()?);
    if shape == Some(ArrayShape::Fixed) {
        let inner = strip_conversions(e);
        if inner.kind() == ExpressionKind::ElementSelect
            && inner
                .select_value()
                .and_then(|v| v.expr_type())
                .and_then(array_shape)
                == Some(ArrayShape::Collection)
        {
            return Some(ArrayShape::Collection);
        }
    }
    shape
}

/// An array operand: the array and the row scopes (template, row index) it is
/// read through, outermost first ([`Builder::array_ref`]).
pub(super) type ArrayRef = (ArrayId, Vec<(ArrayId, Expr)>);

/// What a loop name stands for while its body is built.
#[derive(Clone, Debug)]
pub(super) enum LoopBind {
    /// A run-time loop variable ([`ArrayNode::Loop`]).
    Runtime(LoopId, Ty),
    /// A constant index of an unrolled loop.
    Const(i64),
    /// The element an unrolled reduction over a fixed-size array is at: the
    /// expression of that element.
    Elem(Expr),
}

/// One name bound by a `foreach` or a reduction's iterator.
#[derive(Clone, Debug)]
pub(super) struct LoopScope {
    name: String,
    /// What the name itself reads: the index of a `foreach` variable, the
    /// element of a reduction's `item`.
    value: LoopBind,
    /// What `name.index` reads (a reduction iterator only).
    index: Option<LoopBind>,
}

/// How an array-typed expression is stored.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(super) enum ArrayShape {
    /// A dynamic array or queue: its size is a run-time value.
    Collection,
    /// An associative array.
    Assoc,
    /// A fixed-size unpacked array.
    Fixed,
}

pub(super) fn array_shape(t: Type<'_>) -> Option<ArrayShape> {
    let c = t.canonical();
    if c.is_associative_array() {
        Some(ArrayShape::Assoc)
    } else if c.is_dynamically_sized_array() || c.is_queue() {
        Some(ArrayShape::Collection)
    } else if c.is_unpacked_array() {
        Some(ArrayShape::Fixed)
    } else {
        None
    }
}

fn bad_array(what: impl Into<String>) -> BuildError {
    BuildError::BadArray { what: what.into() }
}

/// The value of a constant `Expr` of type `ty` as a signed integer.
pub(super) fn const_i64(ty: Ty, v: &BigUint) -> Option<i64> {
    let signed = BigInt::from(v.clone());
    let signed = if ty.signed && v.bit(u64::from(ty.width) - 1) {
        signed - (BigInt::one() << ty.width)
    } else {
        signed
    };
    i64::try_from(signed).ok()
}

impl Builder<'_> {
    pub(super) fn arrays_allowed(&self, what: &str) -> Result<(), BuildError> {
        match self.no_arrays {
            None => Ok(()),
            Some(inside) => Err(unsupported(
                format!("{what} inside {inside}"),
                "C14 (array-level values have no weight or bound at build time)",
            )),
        }
    }

    /// Registers the `rand` dynamic-array or queue property `sym` as an
    /// active random array and returns its id (idempotent). Its size and
    /// every element are random variables at run time (IEEE 1800-2023 18.4).
    pub fn declare_rand_array(&mut self, sym: Symbol<'_>) -> Result<u32, BuildError> {
        let uid = sym.uid();
        let name = sym.name().to_string();
        match sym.rand_mode() {
            RandMode::None => return Err(BuildError::NotRand { name }),
            RandMode::RandC => {
                return Err(unsupported(
                    format!("the `randc` array `{name}`: per-element cycling"),
                    "C14",
                ));
            }
            RandMode::Rand => {}
        }
        if let Some(&id) = self.array_ix.get(&uid) {
            self.arrays[id as usize].rand = true;
            return Ok(id);
        }
        let vt = sym.value_type().ok_or_else(|| BuildError::Missing {
            what: format!("value type for `{name}`"),
        })?;
        let info = self.array_info(uid.clone(), name, vt, true)?;
        let id = self.arrays.len() as u32;
        self.arrays.push(info);
        self.array_ix.insert(uid, id);
        Ok(id)
    }

    /// Registers the dynamic-array or queue `sym` as an active random array
    /// whether or not it is declared `rand` (LRM 18.11, 18.12: an argument of
    /// `randomize(v)` / `std::randomize(v)` is random for that call). A `randc`
    /// array is refused as in [`Self::declare_rand_array`]. Idempotent.
    pub fn declare_array_forced(&mut self, sym: Symbol<'_>) -> Result<u32, BuildError> {
        let uid = sym.uid();
        let name = sym.name().to_string();
        if matches!(sym.rand_mode(), RandMode::RandC) {
            return Err(unsupported(
                format!("the `randc` array `{name}`: per-element cycling"),
                "C14",
            ));
        }
        if let Some(&id) = self.array_ix.get(&uid) {
            self.arrays[id as usize].rand = true;
            return Ok(id);
        }
        let vt = sym.value_type().ok_or_else(|| BuildError::Missing {
            what: format!("value type for `{name}`"),
        })?;
        let info = self.array_info(uid.clone(), name, vt, true)?;
        let id = self.arrays.len() as u32;
        self.arrays.push(info);
        self.array_ix.insert(uid, id);
        Ok(id)
    }

    pub(super) fn array_info(
        &self,
        symbol: SymbolId,
        name: String,
        vt: Type<'_>,
        rand: bool,
    ) -> Result<ArrayInfo, BuildError> {
        match array_shape(vt) {
            Some(ArrayShape::Collection) => {}
            // Declared `rand` it is registered so its values are redrawn; a
            // constraint operand is refused where the operand is resolved
            // ([`Builder::array_of`]).
            Some(ArrayShape::Assoc) if rand => {}
            Some(ArrayShape::Assoc) => return Err(Self::assoc_operand(&name)),
            // A fixed-size array is not one array-level value: its elements
            // are leaf variables (`super::aggregate`), and the methods that
            // take the whole array unroll over them.
            Some(ArrayShape::Fixed) => {
                return Err(unsupported(
                    format!(
                        "the fixed-size unpacked array `{name}` as a whole-array constraint \
                         operand (name its elements, or use a reduction method or `foreach`)"
                    ),
                    "C14",
                ));
            }
            None => {
                return Err(BuildError::NonIntegral {
                    what: format!(
                        "`{name}` of type `{}`, which is not an array",
                        vt.to_sv_string()
                    ),
                });
            }
        }
        let et = vt
            .canonical()
            .element_type()
            .ok_or_else(|| BuildError::Missing {
                what: format!("element type of the array `{name}`"),
            })?;
        // An array of dynamic arrays or queues: the leaf is the element of its
        // rows (LRM 7.4.5, 18.4); the rows are solved as arrays of their own,
        // one level at a time. Only the innermost dimension may be a fixed-size
        // one (`int b[][4]`, `int c[][][4]`), stored inline in its outer element.
        let mut row_depth = 0u32;
        let mut inner_fixed = 0u32;
        let mut leaf = et;
        if array_shape(vt) == Some(ArrayShape::Collection) {
            let mut cur = vt;
            loop {
                let elem = cur
                    .canonical()
                    .element_type()
                    .ok_or_else(|| BuildError::Missing {
                        what: format!("element type of the array `{name}`"),
                    })?;
                match array_shape(elem) {
                    None => {
                        leaf = elem;
                        break;
                    }
                    Some(ArrayShape::Collection) => {
                        row_depth += 1;
                        cur = elem;
                    }
                    Some(ArrayShape::Fixed) => {
                        let row = elem.canonical().element_type();
                        let Some(r) = row.filter(|r| array_shape(*r).is_none()) else {
                            return Err(unsupported(
                                format!(
                                    "`{name}`: a fixed-size row whose elements are arrays (a \
                                     fixed-size dimension in the middle of an array of arrays)"
                                ),
                                "C14",
                            ));
                        };
                        // `int b[][4]`: rows of a fixed length, stored inline. The
                        // position of element `j` is `j - lo`, and a dynamic row's
                        // elements are numbered from 0, so `lo` must be 0.
                        let range = elem.canonical().fixed_unpacked_array_range();
                        let (lo, hi) = (
                            i64::from(range.left).min(i64::from(range.right)),
                            i64::from(range.left).max(i64::from(range.right)),
                        );
                        if lo != 0 {
                            return Err(unsupported(
                                format!(
                                    "`{name}`: a fixed-size row whose lowest index is not 0 \
                                     (`[{}:{}]`)",
                                    range.left, range.right
                                ),
                                "C14",
                            ));
                        }
                        row_depth += 1;
                        inner_fixed = (hi + 1) as u32;
                        leaf = r;
                        break;
                    }
                    Some(ArrayShape::Assoc) => {
                        return Err(unsupported(
                            format!(
                                "`{name}`: a dynamic array or queue whose elements are \
                                 fixed-size or associative arrays"
                            ),
                            "C14",
                        ));
                    }
                }
            }
        }
        let nested = row_depth > 0;
        let elem_ty = ty_of(Some(leaf), &format!("an element of the array `{name}`"))?;
        let elem_domain = Self::enum_values(leaf, elem_ty)?;
        Ok(ArrayInfo {
            symbol,
            name,
            elem_ty,
            rand,
            elem_domain,
            assoc: array_shape(vt) == Some(ArrayShape::Assoc),
            nested,
            template_of: None,
            inner_fixed,
            row_depth,
            window: None,
        })
    }

    fn assoc_operand(name: &str) -> BuildError {
        bad_array(format!(
            "`{name}` is an associative array: its size and indices are not randomizable and \
             its elements are not constraint operands (IEEE 1800-2023 18.4)"
        ))
    }

    /// The array a constraint operand names: a dynamic array or queue property
    /// of this class, registered on first use (as state when it is not
    /// `rand`).
    pub(super) fn array_of(&mut self, e: Expression<'_>) -> Result<ArrayId, BuildError> {
        match self.array_ref(e)? {
            (id, rows) if rows.is_empty() && self.arrays[id as usize].nested => Err(unsupported(
                format!(
                    "the array of arrays `{}` as a whole-array operand here (supported: `.size`, \
                     `foreach`, and its rows' sizes, elements and reductions)",
                    self.arrays[id as usize].name
                ),
                "C14",
            )),
            (id, rows) if rows.is_empty() => Ok(id),
            (id, _) => Err(unsupported(
                format!(
                    "a row of the array of arrays `{}` as a whole-array operand (name its \
                     elements `a[i][j]`, or use `.size`, a reduction method, `inside` or \
                     `foreach` on the row)",
                    self.arrays[self.arrays[id as usize].template_of.unwrap_or(id) as usize].name
                ),
                "C14",
            )),
        }
    }

    /// The row template of the array of arrays `outer` (created on first use).
    pub(super) fn row_template(&mut self, outer: ArrayId) -> ArrayId {
        if let Some(&t) = self.templates.get(&outer) {
            return t;
        }
        let o = &self.arrays[outer as usize];
        let info = ArrayInfo {
            symbol: o.symbol.clone(),
            name: format!("{}[]", o.name),
            elem_ty: o.elem_ty,
            rand: false,
            elem_domain: o.elem_domain.clone(),
            assoc: false,
            nested: o.row_depth > 1,
            template_of: Some(outer),
            inner_fixed: 0,
            row_depth: o.row_depth.saturating_sub(1),
            window: None,
        };
        let id = self.arrays.len() as ArrayId;
        self.arrays.push(info);
        self.templates.insert(outer, id);
        id
    }

    /// An array operand: the array itself, or for `a[i]` of an array of arrays
    /// the row template and the row expression `i` ([`ArrayNode::RowScope`]).
    /// For `a[i][j]` of an array of arrays of arrays the chain holds one scope
    /// per level, outermost first, and the array is the innermost template.
    pub(super) fn array_ref(&mut self, e: Expression<'_>) -> Result<ArrayRef, BuildError> {
        let e = strip_conversions(e);
        if e.kind() == ExpressionKind::ElementSelect
            && let Some(id) = self.array_leaf(e)?
        {
            return Ok((id, Vec::new()));
        }
        if e.kind() == ExpressionKind::ElementSelect {
            let base = e.select_value().ok_or_else(|| BuildError::Missing {
                what: "base of a row select".into(),
            })?;
            let sel = e.selector().ok_or_else(|| BuildError::Missing {
                what: "index of a row select".into(),
            })?;
            let (outer, mut chain) = self.array_ref(base)?;
            if !self.arrays[outer as usize].nested {
                return Err(unsupported(
                    format!(
                        "an element select `{}[..]` as an array operand: it is not an array of \
                         arrays",
                        self.arrays[outer as usize].name
                    ),
                    "C14",
                ));
            }
            self.arrays_allowed("a row of an array of arrays")?;
            let row = self.expr(sel)?;
            let mut has_var = false;
            row.for_each_var(&mut |_, _| has_var = true);
            if has_var {
                return Err(bad_array(format!(
                    "a random variable in the row index of the array `{}`: an index is a \
                     constant, a state variable, a loop variable or the size (IEEE 1800-2023 \
                     18.5.7.1)",
                    self.arrays[outer as usize].name
                )));
            }
            let t = self.row_template(outer);
            chain.push((t, row));
            return Ok((t, chain));
        }
        Ok((self.array_named(e)?, Vec::new()))
    }

    fn reject_nested(&self, a: ArrayId, what: &str) -> Result<(), BuildError> {
        if self.arrays[a as usize].nested {
            return Err(unsupported(
                format!(
                    "{what} over the array of arrays `{}` itself (name a row `a[i]`)",
                    self.arrays[a as usize].name
                ),
                "C14",
            ));
        }
        Ok(())
    }

    /// `body` with the rows of `chain` bound, outermost scope outermost.
    fn row_scoped(chain: Vec<(ArrayId, Expr)>, body: Expr) -> Expr {
        chain.into_iter().rev().fold(body, |body, (t, row)| {
            Expr::Array(ArrayNode::RowScope {
                template: t,
                row: Box::new(row),
                body: Box::new(body),
            })
        })
    }

    /// The dynamic array or queue that `e` names inside an aggregate property
    /// (`a[1]` of `rand int a[3][]`, `s.q` of a struct): an array of its own
    /// whose handle sits at a window of the property. `None` when `e` is not
    /// such a leaf.
    fn array_leaf(&mut self, e: Expression<'_>) -> Result<Option<ArrayId>, BuildError> {
        if e.expr_type().and_then(array_shape) != Some(ArrayShape::Collection) {
            return Ok(None);
        }
        let Some(chain) = aggregate_chain(e, &self.forced_roots) else {
            return Ok(None);
        };
        if chain.steps.is_empty() {
            return Ok(None);
        }
        self.array_from_chain(chain).map(Some)
    }

    /// The array the leaf `chain` names (see [`Self::array_leaf`]).
    fn array_from_chain(
        &mut self,
        chain: super::aggregate::Chain<'_>,
    ) -> Result<ArrayId, BuildError> {
        let leaf = match self.resolve_chain(&chain)? {
            Sel::Leaf(leaf) => leaf,
            Sel::Pick { .. } => {
                return Err(unsupported(
                    "a dynamic array or queue element of a fixed-size array selected at a \
                     computed index (use a constant index or a `foreach` variable)",
                    "C14",
                ));
            }
        };
        let key = leaf.root.derive(&Self::leaf_tag(&leaf.path));
        if let Some(&id) = self.array_ix.get(&key) {
            return Ok(id);
        }
        if leaf.mode != RandMode::None {
            return Err(unsupported(
                format!(
                    "the random array `{}`, a leaf of an aggregate property that was not \
                     declared random",
                    leaf.name
                ),
                "C14",
            ));
        }
        let id = self.new_leaf_array(&leaf, false)?;
        self.array_ix.insert(key, id);
        Ok(id)
    }

    fn array_named(&mut self, e: Expression<'_>) -> Result<ArrayId, BuildError> {
        if let Some(id) = self.array_leaf(e)? {
            return Ok(id);
        }
        let sym = match e.kind() {
            ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue => e.referenced_symbol(),
            ExpressionKind::MemberAccess => {
                let base = Self::operand(e, "a member access")?;
                let is_this = base.kind() == ExpressionKind::NamedValue
                    && base.referenced_symbol().is_some_and(|s| s.name() == "this");
                if !is_this {
                    return Err(BuildError::ForeignObjectAccess {
                        what: format!(
                            "the array `.{}` of another object",
                            e.member_symbol()
                                .map_or(String::new(), |m| m.name().to_string())
                        ),
                    });
                }
                e.member_symbol()
            }
            other => {
                return Err(unsupported(
                    format!("a `{other:?}` expression as an array operand"),
                    "C14",
                ));
            }
        };
        let sym = sym.ok_or_else(|| BuildError::Missing {
            what: "symbol of an array operand".into(),
        })?;
        let uid = sym.uid();
        if let Some(&id) = self.array_ix.get(&uid) {
            if self.arrays[id as usize].assoc {
                return Err(Self::assoc_operand(&self.arrays[id as usize].name));
            }
            return Ok(id);
        }
        let vt = e.expr_type().ok_or_else(|| BuildError::Missing {
            what: format!("type of the array `{}`", sym.name()),
        })?;
        let info = self.array_info(uid.clone(), sym.name().to_string(), vt, false)?;
        let id = self.arrays.len() as u32;
        self.arrays.push(info);
        self.array_ix.insert(uid, id);
        Ok(id)
    }

    /// `A.size` / `A.size()` (and a queue's `num`): `Some(array operand)` for
    /// such a call.
    pub(super) fn size_call_array<'d>(e: Expression<'d>) -> Option<Expression<'d>> {
        let sub = e.system_subroutine()?;
        if !matches!(
            sub.known_name_id(),
            KnownSystemName::Size | KnownSystemName::ArraySize | KnownSystemName::Num
        ) {
            return None;
        }
        let arr = *e.operands().first()?;
        expr_shape(arr).map(|_| arr)
    }

    /// The array-level IR of `A.size`.
    pub(super) fn array_size(&mut self, arr: Expression<'_>) -> Result<Expr, BuildError> {
        self.arrays_allowed("an array size")?;
        let (id, rows) = self.array_ref(arr)?;
        Ok(Self::row_scoped(rows, Expr::Array(ArrayNode::Size(id))))
    }

    /// `A[sel]` where `base` (type of `A`) is an unpacked array.
    pub(super) fn array_element(
        &mut self,
        e: Expression<'_>,
        base: Expression<'_>,
        ty: Ty,
    ) -> Result<Expr, BuildError> {
        let mut shape = base.expr_type().and_then(array_shape);
        // `b[i][j]` of `rand int b[][4]`: the row `b[i]` is a fixed-size array
        // stored inline, but it is one row of the outer array's template.
        if shape == Some(ArrayShape::Fixed) {
            let inner = strip_conversions(base);
            if inner.kind() == ExpressionKind::ElementSelect
                && inner
                    .select_value()
                    .and_then(|v| v.expr_type())
                    .and_then(array_shape)
                    == Some(ArrayShape::Collection)
            {
                shape = Some(ArrayShape::Collection);
            }
        }
        let sel = e.selector().ok_or_else(|| BuildError::Missing {
            what: "index of an element select".into(),
        })?;
        match shape {
            Some(ArrayShape::Collection) => {
                self.arrays_allowed("an array element")?;
                let (id, rows) = self.array_ref(base)?;
                let index = self.expr(sel)?;
                let mut has_var = false;
                index.for_each_var(&mut |_, _| has_var = true);
                if has_var {
                    return Err(bad_array(format!(
                        "a random variable in the index of the array `{}`: an index is a \
                         constant, a state variable, a loop variable or the size (IEEE \
                         1800-2023 18.5.7.1)",
                        self.arrays[id as usize].name
                    )));
                }
                let elem_ty = self.arrays[id as usize].elem_ty;
                if self.arrays[id as usize].nested {
                    return Err(unsupported(
                        format!(
                            "a row `{}[..]` of an array of arrays as a value (name an element \
                             `a[i][j]`)",
                            self.arrays[id as usize].name
                        ),
                        "C14",
                    ));
                }
                let el = Self::row_scoped(
                    rows,
                    Expr::Array(ArrayNode::Elem {
                        array: id,
                        index: Box::new(index),
                        ty: elem_ty,
                    }),
                );
                Ok(if elem_ty == ty {
                    el
                } else {
                    Expr::Resize(Box::new(el), ty)
                })
            }
            Some(ArrayShape::Assoc) => Err(bad_array(
                "an element of an associative array: its indices are not randomizable and it \
                 has no constraint form (IEEE 1800-2023 18.4)",
            )),
            Some(ArrayShape::Fixed) => self.fixed_element(e),
            None => Err(BuildError::Missing {
                what: "array type of an element select base".into(),
            }),
        }
    }

    /// An element of a fixed-size unpacked array that is not reached through
    /// a property of this class (`aggregate_chain` resolves every property and
    /// struct-member path before this is asked): a local, a hierarchical
    /// reference, or an array read through an object handle.
    fn fixed_element(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        let what = e
            .select_value()
            .map(strip_conversions)
            .and_then(|b| b.referenced_symbol().or_else(|| b.member_symbol()))
            .map_or_else(String::new, |s| s.name().to_string());
        Err(unsupported(
            format!(
                "an element of the unpacked array `{what}`, which is not a property (or a \
                 member of a struct property) of this class"
            ),
            "C14",
        ))
    }

    /// The names of a `foreach` constraint's loop variables, from its syntax
    /// (the semantic node does not keep them).
    fn foreach_vars(&self, c: Constraint<'_>) -> Result<Vec<String>, BuildError> {
        for tree in self.trees {
            if let Some(node) = c.syntax(tree) {
                let l = LoopConstraintSyntax::cast(node).ok_or_else(|| BuildError::Missing {
                    what: "`foreach` syntax for a Foreach constraint".into(),
                })?;
                return Ok(l
                    .loop_list()
                    .loop_variables()
                    .iter()
                    .map(|v| v.syntax().text().trim().to_string())
                    .collect());
            }
        }
        Err(BuildError::Missing {
            what: "syntax node for a constraint (is its syntax tree passed to the builder?)".into(),
        })
    }

    pub(super) fn fresh_loop(&mut self) -> LoopId {
        let id = self.next_loop;
        self.next_loop += 1;
        id
    }

    /// Builds `body` with `scope` visible, returning its conjuncts.
    fn in_scope(
        &mut self,
        scope: LoopScope,
        body: Constraint<'_>,
    ) -> Result<Vec<Expr>, BuildError> {
        self.loops.push(scope);
        let r = self.constraint(body);
        self.loops.pop();
        r
    }

    /// `foreach (A[i]) body` (IEEE 1800-2023 18.5.7.1).
    pub(super) fn foreach(&mut self, c: Constraint<'_>) -> Result<Vec<Expr>, BuildError> {
        let names = self.foreach_vars(c)?;
        let kids = c.children();
        let arr =
            kids.iter()
                .find_map(|n| n.as_expression())
                .ok_or_else(|| BuildError::Missing {
                    what: "array expression of a `foreach` constraint".into(),
                })?;
        let body =
            kids.iter()
                .find_map(|n| n.as_constraint())
                .ok_or_else(|| BuildError::Missing {
                    what: "body of a `foreach` constraint".into(),
                })?;
        let at = arr.expr_type().ok_or_else(|| BuildError::Missing {
            what: "type of the `foreach` array".into(),
        })?;
        let shape = array_shape(at);
        // LRM 12.7.3 / 18.5.7.1: `foreach (m[i, j])` loops each listed dimension, the first
        // variable outermost; an empty slot (`m[i, , k]`) skips its dimension. Every looped
        // dimension must have a static extent (a fixed unpacked or a packed one), so the
        // body unrolls; a dynamic, queue or associative dimension stays refused.
        let nested_fixed = shape == Some(ArrayShape::Fixed)
            && at
                .canonical()
                .element_type()
                .is_some_and(|elem| array_shape(elem) == Some(ArrayShape::Fixed));
        let nested_dyn = shape == Some(ArrayShape::Collection)
            && at.canonical().element_type().is_some_and(|elem| {
                matches!(
                    array_shape(elem),
                    Some(ArrayShape::Collection | ArrayShape::Fixed)
                )
            });
        if nested_dyn {
            return self.foreach_nested(arr, &names, body);
        }
        // `rand int a[3][]`: the outer dimension is static (unrolled), each row
        // is a dynamic array of its own.
        let fixed_of_dyn = shape == Some(ArrayShape::Fixed)
            && at
                .canonical()
                .element_type()
                .is_some_and(|elem| array_shape(elem) == Some(ArrayShape::Collection));
        if fixed_of_dyn {
            return self.foreach_fixed_outer(arr, at, &names, body);
        }
        if names.len() > 1 || nested_fixed {
            let dims = self.static_dims(at, &names)?;
            return self.unroll_nd(&dims, body);
        }
        let [name] = names.as_slice() else {
            return Err(BuildError::Missing {
                what: "a loop variable of a `foreach` constraint".into(),
            });
        };
        if shape.is_some()
            && at
                .canonical()
                .element_type()
                .is_some_and(|elem| array_shape(elem).is_some())
        {
            return Err(unsupported("a `foreach` over an array of arrays", "C11"));
        }
        let int = Ty::signed(32);
        match shape {
            Some(ArrayShape::Collection) => {
                self.arrays_allowed("a `foreach`")?;
                let array = self.array_of(arr)?;
                let var = self.fresh_loop();
                // A `dist` is fine here: it is built as a template and instanced per
                // element at expansion (`dist::Dist::subject`).
                let (r0, b0, rb0) = (
                    self.real_conds.len() + self.real_dists.len(),
                    self.before.len(),
                    self.real_before.len(),
                );
                let parts = self.in_scope(
                    LoopScope {
                        name: name.clone(),
                        value: LoopBind::Runtime(var, int),
                        index: None,
                    },
                    body,
                )?;
                if self.real_conds.len() + self.real_dists.len() != r0
                    || self.before.len() != b0
                    || self.real_before.len() != rb0
                {
                    return Err(unsupported(
                        "a real `dist` or condition, or a `solve ... before` constraint, inside a \
                         `foreach` over a dynamic array or queue (it would have to hold once per \
                         element)",
                        "C11",
                    ));
                }
                Ok(vec![Expr::Array(ArrayNode::Foreach {
                    array,
                    var,
                    body: Box::new(and_all(parts)),
                })])
            }
            Some(ArrayShape::Assoc) => Err(bad_array(
                "a `foreach` over an associative array: its indices are not randomizable and \
                 it has no constraint form (IEEE 1800-2023 18.4)",
            )),
            Some(ArrayShape::Fixed) => {
                let r = at.canonical().fixed_range();
                self.unroll(name, i64::from(r.left), i64::from(r.right), body)
            }
            None => {
                // A packed vector or packed array: its extent is static.
                let width = u32::try_from(at.bit_width()).map_err(|_| BuildError::Missing {
                    what: "representable width for a `foreach` array".into(),
                })?;
                let g = Geom::of(at, width, "the `foreach` array")?;
                self.unroll(name, g.left, g.right, body)
            }
        }
    }

    /// `foreach (a[i])` / `foreach (a[i, j])` over a fixed-size array of
    /// dynamic arrays or queues (`rand int a[3][]`): `i` is unrolled over the
    /// static dimension, `j` loops row `a[i]` at run time.
    fn foreach_fixed_outer(
        &mut self,
        arr: Expression<'_>,
        at: Type<'_>,
        names: &[String],
        body: Constraint<'_>,
    ) -> Result<Vec<Expr>, BuildError> {
        if names.is_empty() || names.len() > 2 {
            return Err(unsupported(
                format!(
                    "a `foreach` with {} loop variables over a fixed-size array of dynamic \
                     arrays (at most two dimensions)",
                    names.len()
                ),
                "C11",
            ));
        }
        if at
            .canonical()
            .element_type()
            .and_then(|e| e.canonical().element_type())
            .is_some_and(|r| array_shape(r).is_some())
        {
            return Err(unsupported(
                "a `foreach` over an array nested more than two deep",
                "C11",
            ));
        }
        let chain = aggregate_chain(arr, &self.forced_roots).ok_or_else(|| {
            unsupported(
                "a `foreach` over a fixed-size array of dynamic arrays that is not a property \
                 of this class",
                "C11",
            )
        })?;
        let r = at.canonical().fixed_range();
        let (left, right) = (i64::from(r.left), i64::from(r.right));
        let idxs: Vec<i64> = if left >= right {
            (right..=left).rev().collect()
        } else {
            (left..=right).collect()
        };
        let int = Ty::signed(32);
        let mut out = Vec::new();
        for k in idxs {
            let outer_scope = (!names[0].is_empty()).then(|| LoopScope {
                name: names[0].clone(),
                value: LoopBind::Const(k),
                index: None,
            });
            let depth = self.loops.len();
            self.loops.extend(outer_scope);
            let parts = self.fixed_outer_row(&chain, k, names.get(1), int, body);
            self.loops.truncate(depth);
            out.extend(parts?);
        }
        Ok(out)
    }

    /// The body of a `foreach` over a fixed outer dimension at index `k`: the
    /// body itself for a one-variable loop, else a run-time loop over row `k`.
    fn fixed_outer_row(
        &mut self,
        chain: &super::aggregate::Chain<'_>,
        k: i64,
        inner: Option<&String>,
        int: Ty,
        body: Constraint<'_>,
    ) -> Result<Vec<Expr>, BuildError> {
        let Some(inner) = inner else {
            return self.constraint(body);
        };
        self.arrays_allowed("a `foreach`")?;
        let mut row_chain = chain.clone();
        row_chain.steps.push(RawStep::Const(k));
        let row = self.array_from_chain(row_chain)?;
        let vj = self.fresh_loop();
        let (r0, b0, rb0) = (
            self.real_conds.len() + self.real_dists.len(),
            self.before.len(),
            self.real_before.len(),
        );
        let depth = self.loops.len();
        if !inner.is_empty() {
            self.loops.push(LoopScope {
                name: inner.clone(),
                value: LoopBind::Runtime(vj, int),
                index: None,
            });
        }
        let parts = self.constraint(body);
        self.loops.truncate(depth);
        let parts = parts?;
        if self.real_conds.len() + self.real_dists.len() != r0
            || self.before.len() != b0
            || self.real_before.len() != rb0
        {
            return Err(unsupported(
                "a real `dist` or condition, or a `solve ... before` constraint, inside a \
                 `foreach` over a dynamic array row (it would have to hold once per element)",
                "C11",
            ));
        }
        Ok(vec![Expr::Array(ArrayNode::Foreach {
            array: row,
            var: vj,
            body: Box::new(and_all(parts)),
        })])
    }

    /// `foreach (a[i])` / `foreach (a[i, j])` over an array of dynamic arrays
    /// or queues (IEEE 1800-2023 18.5.7.1, 12.7.3): `i` loops the outer array,
    /// `j` the row `a[i]` ([`ArrayNode::RowScope`]). An omitted variable
    /// (`a[, j]`) still loops its dimension.
    fn foreach_nested(
        &mut self,
        arr: Expression<'_>,
        names: &[String],
        body: Constraint<'_>,
    ) -> Result<Vec<Expr>, BuildError> {
        self.arrays_allowed("a `foreach`")?;
        let (outer, rows) = self.array_ref(arr)?;
        if !rows.is_empty() || !self.arrays[outer as usize].nested {
            return Err(unsupported(
                "a `foreach` over an array whose elements are not dynamic arrays",
                "C11",
            ));
        }
        let dims = self.arrays[outer as usize].row_depth as usize + 1;
        if names.is_empty() || names.len() > dims {
            return Err(unsupported(
                format!(
                    "a `foreach` with {} loop variables over an array of dynamic arrays with {} \
                     dimensions",
                    names.len(),
                    dims
                ),
                "C11",
            ));
        }
        let int = Ty::signed(32);
        // `loops[k]` loops dimension `k`; `arrays[k]` is the array it loops (the
        // array itself, then the row template of each level).
        let loops: Vec<LoopId> = names.iter().map(|_| self.fresh_loop()).collect();
        let mut arrays = vec![outer];
        for _ in 1..names.len() {
            let t = self.row_template(*arrays.last().expect("one array"));
            arrays.push(t);
        }
        let scopes: Vec<LoopScope> = names
            .iter()
            .zip(&loops)
            .filter(|(n, _)| !n.is_empty())
            .map(|(n, &v)| LoopScope {
                name: n.clone(),
                value: LoopBind::Runtime(v, int),
                index: None,
            })
            .collect();
        let (r0, b0, rb0) = (
            self.real_conds.len() + self.real_dists.len(),
            self.before.len(),
            self.real_before.len(),
        );
        let depth = self.loops.len();
        self.loops.extend(scopes);
        let parts = self.constraint(body);
        self.loops.truncate(depth);
        let parts = parts?;
        if self.real_conds.len() + self.real_dists.len() != r0
            || self.before.len() != b0
            || self.real_before.len() != rb0
        {
            return Err(unsupported(
                "a real `dist` or condition, or a `solve ... before` constraint, inside a \
                 `foreach` over an array of dynamic arrays (it would have to hold once per \
                 element)",
                "C11",
            ));
        }
        // Innermost dimension first: each deeper one loops the row template of
        // the dimension above, bound to that dimension's loop variable.
        let mut inner = and_all(parts);
        for k in (0..names.len()).rev() {
            inner = Expr::Array(ArrayNode::Foreach {
                array: arrays[k],
                var: loops[k],
                body: Box::new(inner),
            });
            if k > 0 {
                inner = Expr::Array(ArrayNode::RowScope {
                    template: arrays[k],
                    row: Box::new(Expr::Array(ArrayNode::Loop(loops[k - 1], int))),
                    body: Box::new(inner),
                });
            }
        }
        Ok(vec![inner])
    }

    /// The `(name, left, right)` of each dimension a multi-variable `foreach` loops over
    /// (`None` extent for an omitted loop variable), walking `names.len()` dimensions of `ty`.
    fn static_dims(
        &self,
        ty: sv_lang::Type<'_>,
        names: &[String],
    ) -> Result<Vec<(String, i64, i64)>, BuildError> {
        let mut dims = Vec::new();
        let mut cur = ty;
        for (k, name) in names.iter().enumerate() {
            let c = cur.canonical();
            let (left, right) = match array_shape(cur) {
                Some(ArrayShape::Fixed) => {
                    let r = c.fixed_range();
                    (i64::from(r.left), i64::from(r.right))
                }
                None if c.is_integral() => {
                    let width = u32::try_from(c.bit_width()).map_err(|_| BuildError::Missing {
                        what: "representable width for a `foreach` array".into(),
                    })?;
                    let g = Geom::of(cur, width, "the `foreach` array")?;
                    (g.left, g.right)
                }
                _ => {
                    return Err(unsupported(
                        format!(
                            "a multi-dimensional `foreach`: dimension {} is a dynamic array,                              queue or associative array (only fixed-size dimensions unroll)",
                            k + 1
                        ),
                        "C11",
                    ));
                }
            };
            dims.push((name.clone(), left, right));
            if k + 1 < names.len() {
                cur = c.element_type().ok_or_else(|| {
                    unsupported(
                        format!(
                            "a `foreach` with {} loop variables over an array with fewer \
                             dimensions",
                            names.len()
                        ),
                        "C11",
                    )
                })?;
            }
        }
        Ok(dims)
    }

    /// The body of a multi-variable `foreach`, once per index tuple (first variable outermost,
    /// each from its left bound toward its right; LRM 12.7.3).
    fn unroll_nd(
        &mut self,
        dims: &[(String, i64, i64)],
        body: Constraint<'_>,
    ) -> Result<Vec<Expr>, BuildError> {
        let Some((name, left, right)) = dims.first() else {
            return self.constraint(body);
        };
        if name.is_empty() {
            return self.unroll_nd(&dims[1..], body);
        }
        let idxs: Vec<i64> = if left >= right {
            (*right..=*left).rev().collect()
        } else {
            (*left..=*right).collect()
        };
        let mut out = Vec::new();
        for i in idxs {
            self.loops.push(LoopScope {
                name: name.clone(),
                value: LoopBind::Const(i),
                index: None,
            });
            let r = self.unroll_nd(&dims[1..], body);
            self.loops.pop();
            out.extend(r?);
        }
        Ok(out)
    }

    /// The body of a `foreach` over a statically known extent, once per index
    /// from the left bound toward the right (LRM 12.7.3).
    fn unroll(
        &mut self,
        name: &str,
        left: i64,
        right: i64,
        body: Constraint<'_>,
    ) -> Result<Vec<Expr>, BuildError> {
        let idxs: Vec<i64> = if left >= right {
            (right..=left).rev().collect()
        } else {
            (left..=right).collect()
        };
        let mut out = Vec::new();
        for i in idxs {
            out.extend(self.in_scope(
                LoopScope {
                    name: name.to_string(),
                    value: LoopBind::Const(i),
                    index: None,
                },
                body,
            )?);
        }
        Ok(out)
    }

    /// Whether the constraint being built is inside a `foreach` over a
    /// dynamic array or queue (its body holds once per run-time element); a
    /// `foreach` over a static extent is unrolled and is not.
    pub(super) fn in_runtime_loop(&self) -> bool {
        self.loops
            .iter()
            .any(|s| matches!(s.value, LoopBind::Runtime(..)))
    }

    fn scope_of(&self, name: &str) -> Option<&LoopScope> {
        self.loops.iter().rev().find(|s| s.name == name)
    }

    fn bind_expr(&self, b: LoopBind, ty: Ty) -> Result<Expr, BuildError> {
        match b {
            LoopBind::Runtime(id, lt) => {
                let l = Expr::Array(ArrayNode::Loop(id, lt));
                Ok(if lt == ty {
                    l
                } else {
                    Expr::Resize(Box::new(l), ty)
                })
            }
            LoopBind::Const(i) => Ok(iconst(ty, i)),
            LoopBind::Elem(x) => Ok(if x.ty() == ty {
                x
            } else {
                Expr::Resize(Box::new(x), ty)
            }),
        }
    }

    /// A reference to a `foreach` loop variable or a reduction's `item`.
    pub(super) fn loop_ref(&mut self, sym: Symbol<'_>, ty: Ty) -> Result<Expr, BuildError> {
        debug_assert_eq!(sym.kind(), SymbolKind::Iterator);
        let name = sym.name();
        let b = self
            .scope_of(name)
            .ok_or_else(|| BuildError::Missing {
                what: format!("an enclosing `foreach` or array method binding `{name}`"),
            })?
            .value
            .clone();
        if matches!(b, LoopBind::Runtime(..)) {
            self.arrays_allowed("a loop variable")?;
        }
        self.bind_expr(b, ty)
    }

    /// `item.index` inside a reduction's `with` clause.
    pub(super) fn iterator_index(&mut self, e: Expression<'_>, ty: Ty) -> Result<Expr, BuildError> {
        let this = *e.operands().first().ok_or_else(|| BuildError::Missing {
            what: "iterator of `index`".into(),
        })?;
        let name = this
            .referenced_symbol()
            .map(|s| s.name().to_string())
            .ok_or_else(|| BuildError::Missing {
                what: "symbol of the iterator of `index`".into(),
            })?;
        let b = self
            .scope_of(&name)
            .and_then(|s| s.index.clone())
            .ok_or_else(|| BuildError::Missing {
                what: format!("an array method iterator `{name}` for `.index`"),
            })?;
        self.arrays_allowed("an iterator index")?;
        self.bind_expr(b, ty)
    }

    /// `A.sum()`, `.product()`, `.and()`, `.or()`, `.xor()` with an optional
    /// `with (expr)` (IEEE 1800-2023 18.5.7.2, 7.12.3).
    pub(super) fn array_reduction(
        &mut self,
        e: Expression<'_>,
        op: ReduceOp,
        ty: Ty,
    ) -> Result<Expr, BuildError> {
        let arr = e
            .operands()
            .into_iter()
            .find(|o| expr_shape(*o).is_some())
            .ok_or_else(|| BuildError::Missing {
                what: "array operand of a reduction method".into(),
            })?;
        if expr_shape(arr) == Some(ArrayShape::Fixed) {
            return self.fixed_reduction(e, arr, op, ty);
        }
        self.arrays_allowed("an array reduction")?;
        let (array, rows) = self.array_ref(arr)?;
        self.reject_nested(array, "a reduction method")?;
        let elem_ty = self.arrays[array as usize].elem_ty;
        let var = self.fresh_loop();
        let index_var = self.fresh_loop();
        let body = match e.iterator_expr() {
            Some(w) => {
                let iter = e.iterator_var().ok_or_else(|| BuildError::Missing {
                    what: "iterator variable of a reduction's `with` clause".into(),
                })?;
                self.loops.push(LoopScope {
                    name: iter.name().to_string(),
                    value: LoopBind::Runtime(var, elem_ty),
                    index: Some(LoopBind::Runtime(index_var, Ty::signed(32))),
                });
                let b = self.expr(w);
                self.loops.pop();
                b?
            }
            None => Expr::Array(ArrayNode::Loop(var, elem_ty)),
        };
        let body = if body.ty() == ty {
            body
        } else {
            coerce(body, ty)
        };
        Ok(Self::row_scoped(
            rows,
            Expr::Array(ArrayNode::Reduce {
                op,
                array,
                var,
                index_var,
                body: Box::new(body),
            }),
        ))
    }

    /// A reduction method over a fixed-size unpacked array (a property of
    /// this class, or a struct member of one): its extent is known now, so it
    /// unrolls into the fold of its elements, each bound to the iterator
    /// (IEEE 1800-2023 7.12.3, 18.5.7.2).
    fn fixed_reduction(
        &mut self,
        e: Expression<'_>,
        arr: Expression<'_>,
        op: ReduceOp,
        ty: Ty,
    ) -> Result<Expr, BuildError> {
        let at = arr
            .expr_type()
            .ok_or_else(|| BuildError::Missing {
                what: "type of the reduced array".into(),
            })?
            .canonical();
        let r = at.fixed_unpacked_array_range();
        let (lo, hi) = (
            i64::from(r.left).min(i64::from(r.right)),
            i64::from(r.left).max(i64::from(r.right)),
        );
        let et = at.element_type().ok_or_else(|| BuildError::Missing {
            what: "element type of the reduced array".into(),
        })?;
        let elem_ty = ty_of(Some(et), "an element of the reduced array")?;
        let mut acc: Option<Expr> = None;
        for i in lo..=hi {
            let item = self.aggregate_element(arr, i, elem_ty)?;
            let body = match e.iterator_expr() {
                Some(w) => {
                    let iter = e.iterator_var().ok_or_else(|| BuildError::Missing {
                        what: "iterator variable of a reduction's `with` clause".into(),
                    })?;
                    self.loops.push(LoopScope {
                        name: iter.name().to_string(),
                        value: LoopBind::Elem(item),
                        index: Some(LoopBind::Const(i)),
                    });
                    let b = self.expr(w);
                    self.loops.pop();
                    b?
                }
                None => item,
            };
            let body = if body.ty() == ty {
                body
            } else {
                coerce(body, ty)
            };
            acc = Some(match acc {
                None => body,
                Some(a) => {
                    let bop = match op {
                        ReduceOp::Sum => BinOp::Add,
                        ReduceOp::Product => BinOp::Mul,
                        ReduceOp::And => BinOp::And,
                        ReduceOp::Or => BinOp::Or,
                        ReduceOp::Xor => BinOp::Xor,
                    };
                    bin(bop, a, body, ty)
                }
            });
        }
        acc.ok_or_else(|| BuildError::Missing {
            what: "elements of the reduced array".into(),
        })
    }

    /// `left inside {A}` for an array `A` in the set: true when `left` equals
    /// some element of `A` (IEEE 1800-2023 11.4.13, 18.5.3: the array is
    /// traversed and each element is a member of the set). A fixed-size array
    /// unrolls into a disjunction of equalities; a dynamic array or queue is
    /// an `or`-reduction over its run-time elements, so an empty one admits
    /// nothing.
    pub(super) fn inside_array(
        &mut self,
        left: &Expr,
        arr: Expression<'_>,
    ) -> Result<Expr, BuildError> {
        let eq = |left: &Expr, x: Expr| {
            let t = common_ty(left.ty(), x.ty());
            bin(BinOp::Eq, coerce(left.clone(), t), coerce(x, t), Ty::BIT)
        };
        let at = arr.expr_type().ok_or_else(|| BuildError::Missing {
            what: "type of an `inside` array".into(),
        })?;
        match expr_shape(arr) {
            Some(ArrayShape::Fixed) => {
                let c = at.canonical();
                let r = c.fixed_unpacked_array_range();
                let (lo, hi) = (
                    i64::from(r.left).min(i64::from(r.right)),
                    i64::from(r.left).max(i64::from(r.right)),
                );
                let et = c.element_type().ok_or_else(|| BuildError::Missing {
                    what: "element type of an `inside` array".into(),
                })?;
                let elem_ty = ty_of(Some(et), "an element of an `inside` array")?;
                let mut acc: Option<Expr> = None;
                for i in lo..=hi {
                    let item = self.aggregate_element(arr, i, elem_ty)?;
                    let term = eq(left, item);
                    acc = Some(match acc {
                        None => term,
                        Some(prev) => bin(BinOp::LogOr, prev, term, Ty::BIT),
                    });
                }
                acc.ok_or_else(|| BuildError::Missing {
                    what: "elements of an `inside` array".into(),
                })
            }
            Some(ArrayShape::Collection) => {
                self.arrays_allowed("an `inside` over an array")?;
                let (array, rows) = self.array_ref(arr)?;
                self.reject_nested(array, "an `inside` set")?;
                let elem_ty = self.arrays[array as usize].elem_ty;
                let var = self.fresh_loop();
                let index_var = self.fresh_loop();
                let body = eq(left, Expr::Array(ArrayNode::Loop(var, elem_ty)));
                Ok(Self::row_scoped(
                    rows,
                    Expr::Array(ArrayNode::Reduce {
                        op: ReduceOp::Or,
                        array,
                        var,
                        index_var,
                        body: Box::new(body),
                    }),
                ))
            }
            Some(ArrayShape::Assoc) | None => Err(bad_array(
                "an associative array in an `inside` set: its elements are not constraint \
                 operands (IEEE 1800-2023 18.4)",
            )),
        }
    }

    /// The array-level value of a call to a system method on an array, or
    /// `None` for any other call.
    pub(super) fn array_call(
        &mut self,
        e: Expression<'_>,
        ty: Ty,
    ) -> Option<Result<Expr, BuildError>> {
        let sub = e.system_subroutine()?;
        let op = match sub.known_name_id() {
            KnownSystemName::Size | KnownSystemName::ArraySize | KnownSystemName::Num => {
                let arr = Self::size_call_array(e)?;
                return Some(self.array_size(arr));
            }
            KnownSystemName::Index => return Some(self.iterator_index(e, ty)),
            KnownSystemName::Sum => ReduceOp::Sum,
            KnownSystemName::Product => ReduceOp::Product,
            KnownSystemName::And => ReduceOp::And,
            KnownSystemName::Or => ReduceOp::Or,
            KnownSystemName::XOr => ReduceOp::Xor,
            _ => return None,
        };
        Some(self.array_reduction(e, op, ty))
    }
}