vj-sim 0.1.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::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,
}

/// 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)
    }

    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}`"),
            })?;
        let elem_ty = ty_of(Some(et), &format!("an element of the array `{name}`"))?;
        let elem_domain = Self::enum_values(et, elem_ty)?;
        Ok(ArrayInfo {
            symbol,
            name,
            elem_ty,
            rand,
            elem_domain,
            assoc: array_shape(vt) == Some(ArrayShape::Assoc),
        })
    }

    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> {
        let e = strip_conversions(e);
        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()?;
        array_shape(arr.expr_type()?).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 = self.array_of(arr)?;
        Ok(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 shape = base.expr_type().and_then(array_shape);
        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 = self.array_of(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;
                let el = 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(),
        })
    }

    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));
        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)
            }
        }
    }

    /// 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| o.expr_type().is_some_and(|t| array_shape(t).is_some()))
            .ok_or_else(|| BuildError::Missing {
                what: "array operand of a reduction method".into(),
            })?;
        if arr.expr_type().and_then(array_shape) == Some(ArrayShape::Fixed) {
            return self.fixed_reduction(e, arr, op, ty);
        }
        self.arrays_allowed("an array reduction")?;
        let array = self.array_of(arr)?;
        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(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 array_shape(at) {
            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 = self.array_of(arr)?;
                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(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))
    }
}