sv_sim_sim/constraints/

build.rs

//! The sv-lang `Constraint`/`Expression` to [`ir::Expr`] builder (plan task
//! C2; LRM 18.3 and 18.5).
//!
//! # Contract
//!
//! A [`Builder`] is told which symbols are *active random variables*
//! ([`Builder::declare_rand`]); every other value a constraint reads becomes a
//! *state variable* (LRM 18.3: a non-`rand` variable, or one whose
//! `rand_mode` is off, is a constant during the solve), registered on first
//! use. Constraint blocks are then fed in ([`Builder::add_block`],
//! [`Builder::add_constraint`]); each constraint item becomes one boolean
//! conjunct. [`Builder::finish`] appends the implicit enum-domain conjuncts
//! (LRM 18.3: a `rand` enum variable only takes the enum's named constants)
//! and re-validates every tree, so a builder bug is a loud [`BuildError::Ir`]
//! and never a wrong sample.
//!
//! # Typing
//!
//! slang has already applied LRM 11.6 (context-determined widths) and
//! inserted a `Conversion` node wherever an operand's type differs from its
//! context's, so every arithmetic/bitwise/compare node here sees operands of
//! one type. The conversion's extension rule is the one place a mistake is
//! easy: a `Propagated` conversion extends by the *context's* signedness (a
//! signed operand in an unsigned context is zero-extended, LRM 11.8.2), while
//! an `Implicit`/`Explicit` one extends by the *operand's* (assignment
//! semantics). Both were verified against slang's own constant evaluator.
//!
//! # What is rejected, by name
//!
//! Every construct outside this task's scope is a typed [`BuildError`] naming
//! the construct and the plan task that owns it; nothing is silently dropped
//! (inline `with`, a `rand` handle, ...).
//!
//! # Soft constraints (C15; LRM 18.5.13)
//!
//! A `soft` constraint is an ordinary conjunct wrapped in its discard flag
//! ([`priority::wrap_soft`]) and recorded in [`ConstraintSet::softs`] with its
//! [`Priority`] and the variables it mentions; a `disable soft x` is applied
//! once, in [`Builder::finish`], by marking the lower-priority softs that name
//! `x` as disabled. The relaxation itself is the registry's
//! ([`priority::solve_relaxing`]). Priorities follow the order constraints are
//! fed in (later is higher) and the scope set by
//! [`Builder::set_priority_scope`] (a derived class above its bases, a
//! contained object below its container). A `soft` over a real value, inside a
//! `foreach`, or over a `randc` variable, and a `disable soft` anywhere but at
//! the top level of a block, are refused by name.
//!
//! # Arrays and iterative constraints (C11, C12, C14; LRM 18.4, 18.5.7)
//!
//! Dynamic-array and queue properties become *array-level* IR
//! ([`ir::ArrayNode`]): `A.size`, `A[i]`, `foreach` and the reduction methods
//! with their iterator variables. Expanding them needs the run-time sizes, so
//! it is the registry's job (`super::array`); the limits of what is built here
//! are listed in the `arrays` submodule. A packed struct or union is one
//! integral variable and `s.member` a window of it (18.4). An unpacked struct
//! or fixed-size unpacked array property is flattened to its *leaves*, each a
//! variable windowed into the property's value ([`Builder::declare_rand_aggregate`],
//! the `aggregate` submodule): `rand` makes every element or member random
//! (18.4), a member's own qualifier overrides the inherited one, and `a[i]` at
//! a state or loop index is a run-time choice among the elements
//! ([`ir::ArrayNode::Pick`]).
//!
//! # Real-valued constraints (C9; LRM 18.5.3, 18.5.13)
//!
//! A `rand real`/`shortreal` variable ([`Builder::declare_rand_real`]) lives
//! in its own namespace: its constraints build [`real_domain`](super::real_domain)
//! conditions into [`ConstraintSet::real`] and never an integral conjunct (see
//! the `real` submodule for the supported subset and its limits). A constraint
//! that reads a real random variable is a real constraint; one mixing it with
//! an integral random variable is a named [`BuildError::RealConstraint`].
//!
//! # Uniqueness (C10; LRM 18.5.4)
//!
//! `unique { a, b, c[2:3] }` becomes one [`Expr::AllDistinct`] conjunct whose
//! members are the group's singular variables and the leaf elements of its
//! array members, in source order (see the `unique` submodule). An array
//! element is an IR variable once [`Builder::declare_rand_aggregate`] (or
//! [`Builder::declare_rand_element`]) has declared it.
//!
//! # Guards and object handles (C8; LRM 18.5.5, 18.5.6, 18.5.12)
//!
//! A constraint-level implication and an `if`/`else` build [`Expr::Guard`]
//! (predicate, body, else-body) rather than a plain `Ite`: the solver
//! evaluates the predicate by the Figure 18-3 rules before solving, so a null
//! handle read where no operand decides the guard is an error and a decided
//! guard drops the unselected arm unexamined. A non-`rand` handle read in a
//! constraint is a state variable: `null` is the constant 0, a handle itself
//! a 64-bit state, and `a.x` / `a.next.x` a *path* state variable
//! ([`StateInfo::via`]) the registry walks at randomize time, so a null link
//! is a typed outcome and not a crash. Without an object layout resolver a
//! member read through a handle stays [`BuildError::ForeignObjectAccess`].
//! `solve ... before` is NOT a boolean constraint: it
//! contributes ordering edges ([`ConstraintSet::before`]) and no conjunct
//! (LRM 18.5.9: it never changes the solution space). 4-state operators and
//! literals are [`BuildError::FourStateOperator`]/[`BuildError::FourStateLiteral`]
//! (LRM 18.3: "illegal and shall result in an error"); a `virtual interface`
//! `rand` variable is [`BuildError::VirtualInterfaceRand`].

use super::dist::{DefaultWeight, Dist, Item, SELECTOR_BASE, Span};
use super::func::Func;
use super::ir::{BinOp, Expr, IrError, Ty, UnOp, VarId, mask};
use super::order::{self, OrderError};
use super::priority::{self, Disable, Priority, Soft, SoftKey};
use super::randc::MAX_RANDC_WIDTH;
use super::real_domain::{RealCond, RealDist, RealProblem};
use super::reduce::BlockItems;
use crate::objects::{FieldSlot, Window};
use crate::symid::{SymbolId, SymbolUid};
use core::fmt;
use num_bigint::{BigInt, BigUint};
use num_traits::{One, Zero};
use std::collections::{HashMap, HashSet};
use sv_lang::kinds::{ConstraintKind, ExpressionKind, PatternKind, SymbolKind};
use sv_lang::nodes::{
    ExpressionConstraintSyntax, SolveBeforeConstraintSyntax, ValueRangeExpressionSyntax,
};
use sv_lang::{
    AstNode, BinaryOp, Bit, Constraint, ConstraintBlockFlags, DistWeightKind, Expression, RandMode,
    SVInt, Symbol, SyntaxTree, Type, UnaryOp,
};

mod aggregate;
mod arrays;
mod funcs;
mod real;
mod unique;
pub use aggregate::{Declared, Step, is_aggregate_type, property_is_random};
pub use arrays::ArrayInfo;
use arrays::LoopScope;
pub use real::RealVarInfo;

/// Why a constraint could not be turned into IR.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum BuildError {
    /// A 4-state operator (`===`, `!==`, `==?`, `!=?`): LRM 18.3.
    FourStateOperator {
        /// The operator's spelling.
        op: &'static str,
    },
    /// A literal or constant with an X/Z bit: LRM 18.3.
    FourStateLiteral {
        /// The constant's text.
        text: String,
    },
    /// A `rand` variable of virtual-interface type (plan section 1.5).
    VirtualInterfaceRand {
        /// The variable.
        name: String,
    },
    /// A value that is not an integral bit-vector (real, string, class
    /// handle, unpacked aggregate, ...).
    NonIntegral {
        /// What was found.
        what: String,
    },
    /// A reference through another object (`other.field`) that the joint
    /// solver of plan task C17 does not cover.
    ForeignObjectAccess {
        /// What was referenced.
        what: String,
    },
    /// `declare_rand` on a symbol that is not `rand`.
    NotRand {
        /// The symbol.
        name: String,
    },
    /// A construct this task (or the current plan position) does not build.
    Unsupported {
        /// The construct.
        construct: String,
        /// The plan task that owns it.
        task: &'static str,
    },
    /// A constant select index outside the declared range.
    OutOfRangeSelect {
        /// What was selected.
        what: String,
    },
    /// An sv-lang node lacked an accessor the builder needs.
    Missing {
        /// What was missing.
        what: String,
    },
    /// A `randc` variable wider than the permutation engine supports (LRM
    /// 18.4.2 allows the limit as long as it is at least 8 bits).
    RandcTooWide {
        /// The variable.
        name: String,
        /// Its width.
        width: u32,
        /// The widest supported.
        max: u32,
    },
    /// A `solve ... before` operand that LRM 18.5.9 does not allow (not a
    /// `rand` variable of the class, or a `randc` one).
    BadSolveOperand {
        /// What was wrong with it.
        what: String,
    },
    /// A `dist` (or value range) the LRM does not allow, or one this
    /// implementation cannot weight exactly.
    BadDist {
        /// What was wrong with it.
        what: String,
    },
    /// A `unique` group the LRM does not allow (a `randc` member, members of
    /// different types, something that is not a variable; 18.5.4).
    BadUnique {
        /// What was wrong with it.
        what: String,
    },
    /// A constraint on a `real`/`shortreal` variable the real-domain solver
    /// cannot take (see [`super::real_domain`]), or a real `rand` declaration
    /// the LRM does not allow.
    RealConstraint {
        /// What was wrong with it.
        what: String,
    },
    /// An array constraint the LRM does not allow or that has no meaning
    /// (an associative array's size or elements, a random index; 18.4,
    /// 18.5.7).
    BadArray {
        /// What was wrong with it.
        what: String,
    },
    /// A function called from a constraint that cannot be evaluated before the
    /// solve (18.5.11): a side effect, a construct outside the supported
    /// subset, a read of a random variable that is not an argument.
    BadFunction {
        /// The function.
        function: String,
        /// What was wrong with it.
        what: String,
    },
    /// A `soft` constraint or `disable soft` the LRM does not allow or that
    /// this implementation cannot relax exactly (18.5.13).
    BadSoft {
        /// What was wrong with it.
        what: String,
    },
    /// An `extern constraint name;` prototype with no external constraint
    /// block anywhere in its scope (18.5.1).
    MissingExternBody {
        /// The prototype's name.
        name: String,
    },
    /// The `solve ... before` constraints have no order (a cycle).
    Order(OrderError),
    /// The built tree failed [`Expr::validate`] (a builder bug).
    Ir(IrError),
}

impl fmt::Display for BuildError {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            BuildError::FourStateOperator { op } => write!(
                f,
                "the 4-state operator `{op}` is illegal in a constraint (IEEE 1800-2023 18.3)"
            ),
            BuildError::FourStateLiteral { text } => write!(
                f,
                "the 4-state value `{text}` is illegal in a constraint (IEEE 1800-2023 18.3)"
            ),
            BuildError::VirtualInterfaceRand { name } => write!(
                f,
                "`rand` variable `{name}` has a virtual interface type, which cannot be randomized"
            ),
            BuildError::NonIntegral { what } => {
                write!(
                    f,
                    "{what} is not an integral value; constraints solve integral variables only"
                )
            }
            BuildError::ForeignObjectAccess { what } => write!(
                f,
                "{what}: this reference to another object's members is not covered by the \
                 multi-object solver (constraints plan task C17 follow-up)"
            ),
            BuildError::NotRand { name } => {
                write!(f, "`{name}` is not a `rand`/`randc` variable")
            }
            BuildError::Unsupported { construct, task } => write!(
                f,
                "{construct} in a constraint is not implemented yet (constraints plan {task})"
            ),
            BuildError::OutOfRangeSelect { what } => {
                write!(f, "constant select out of the declared range: {what}")
            }
            BuildError::Missing { what } => write!(f, "sv-lang gave no {what}"),
            BuildError::RandcTooWide { name, width, max } => write!(
                f,
                "`randc` variable `{name}` is {width} bits wide; this implementation cycles \
                 `randc` variables of at most {max} bits (IEEE 1800-2023 18.4.2 permits a \
                 limit of at least 8)"
            ),
            BuildError::BadSolveOperand { what } => write!(
                f,
                "invalid `solve ... before` operand: {what} (IEEE 1800-2023 18.5.9)"
            ),
            BuildError::BadDist { what } => {
                write!(
                    f,
                    "invalid `dist` constraint: {what} (IEEE 1800-2023 18.5.3)"
                )
            }
            BuildError::BadUnique { what } => {
                write!(
                    f,
                    "invalid `unique` constraint: {what} (IEEE 1800-2023 18.5.4)"
                )
            }
            BuildError::RealConstraint { what } => {
                write!(f, "unsupported real-valued constraint: {what}")
            }
            BuildError::BadArray { what } => {
                write!(f, "invalid array constraint: {what}")
            }
            BuildError::BadFunction { function, what } => write!(
                f,
                "function `{function}` cannot be called from a constraint: {what} \
                 (IEEE 1800-2023 18.5.11)"
            ),
            BuildError::BadSoft { what } => {
                write!(
                    f,
                    "invalid soft constraint: {what} (IEEE 1800-2023 18.5.13)"
                )
            }
            BuildError::MissingExternBody { name } => write!(
                f,
                "`extern constraint {name};` has no external constraint block \
                 (IEEE 1800-2023 18.5.1)"
            ),
            BuildError::Order(e) => write!(f, "{e}"),
            BuildError::Ir(e) => write!(f, "{e}"),
        }
    }
}

impl std::error::Error for BuildError {}

impl From<IrError> for BuildError {
    fn from(e: IrError) -> Self {
        BuildError::Ir(e)
    }
}

impl From<OrderError> for BuildError {
    fn from(e: OrderError) -> Self {
        BuildError::Order(e)
    }
}

fn unsupported(construct: impl Into<String>, task: &'static str) -> BuildError {
    BuildError::Unsupported {
        construct: construct.into(),
        task,
    }
}

/// An active random variable.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct VarInfo {
    /// The declaring symbol's key.
    pub symbol: SymbolId,
    /// Its declared name.
    pub name: String,
    /// Its type (a 4-state declaration is solved as 2-state).
    pub ty: Ty,
    /// For an enum-typed variable, the named constants it may take (LRM 18.3).
    pub enum_domain: Option<Vec<BigUint>>,
    /// Whether it is `randc`: drawn from its own cyclic permutation before
    /// every `rand` variable (LRM 18.4.2) instead of from the joint solution
    /// space.
    pub randc: bool,
    /// For one leaf of an aggregate property ([`Builder::declare_rand_aggregate`],
    /// [`Builder::declare_rand_element`]), the steps from the property to it,
    /// outermost first; empty for a property. [`Self::symbol`] is then the
    /// property's key and [`Self::name`] reads `a[2]` or `s.f[1]`.
    pub path: Vec<Step>,
    /// Where that leaf sits in its property's stored value; `None` for a
    /// property itself.
    pub window: Option<Window>,
}

/// One step of a state variable's path through object handles.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct StateHop {
    /// The member's key.
    pub symbol: SymbolId,
    /// Where the member lives in the object the previous step's handle
    /// names, as laid out by the builder's slot resolver.
    pub slot: FieldSlot,
}

/// A state variable: a value read before the solve and fixed during it.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct StateInfo {
    /// The symbol's key: the property of the randomized class that holds
    /// the value, or (when [`Self::via`] is not empty) the object handle the
    /// path starts at.
    pub symbol: SymbolId,
    /// Its name as written: `x`, or `a.x` for a member read through a handle.
    pub name: String,
    /// Its type (a class handle is a 64-bit unsigned value).
    pub ty: Ty,
    /// The members followed from the handle [`Self::symbol`] to the value:
    /// the first is read from the object that handle names, the next from
    /// the object the first one's value names, and so on. A null (or
    /// deleted) handle on the way makes the state unreadable. Empty for a
    /// plain property.
    pub via: Vec<StateHop>,
    /// For a leaf of an aggregate property that is not random (a plain
    /// member of a struct, an element of a non-`rand` array), where it sits in
    /// the property [`Self::symbol`] names; `None` for the whole value.
    pub window: Option<Window>,
    /// The bit of the root handle property the first handle's word starts at:
    /// `64 * i` for `es[i].v` through a fixed array of handles (LRM 18.5.8), 0
    /// otherwise.
    pub root_bit: u32,
    /// The value is the dynamic class template id of the object the handle at
    /// the end of the path names (0 never; a null handle makes the state
    /// unreadable), not the handle itself: the selector of a virtual call
    /// through a handle.
    pub class_of: bool,
}

/// A local of an inline constraint's call site (LRM 18.7): its value is read
/// when the call is made and is a constant of the solve.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct CaptureInfo {
    /// The state variable that stands for it ([`ConstraintSet::states`]).
    pub state: u32,
    /// The local's key (for a member read through a local handle, the handle).
    pub symbol: SymbolId,
    /// The members followed from the local handle [`Self::symbol`] to the
    /// captured value (`o.lim` in a call-site `with { x < o.lim }`, LRM 18.7:
    /// the whole read is one call-site constant); empty for the local itself.
    pub hops: Vec<SymbolId>,
    /// Its name as written.
    pub name: String,
    /// Its type.
    pub ty: Ty,
}

/// Decides whether a name read by an inline constraint resolves in the scope
/// of the `randomize()` call (a *local*, LRM 18.7) rather than in the
/// randomized object's class; see [`Builder::set_local_classifier`].
pub type LocalClassifier<'t> = Box<dyn for<'s> Fn(Expression<'s>) -> bool + 't>;

/// The builder's product: variable tables plus the boolean conjuncts that
/// must all hold.
#[derive(Clone, Debug, PartialEq, Eq, Default)]
pub struct ConstraintSet {
    /// Random variables, indexed by [`super::ir::VarId`].
    pub vars: Vec<VarInfo>,
    /// State variables, indexed by [`super::ir::StateId`].
    pub states: Vec<StateInfo>,
    /// One-bit expressions, all of which must be true (user constraints in
    /// source order, then the implicit enum-domain conjuncts).
    pub conjuncts: Vec<Expr>,
    /// For each variable (indexed like [`Self::vars`]), the index into
    /// [`Self::conjuncts`] of its implicit enum-domain conjunct, if any.
    /// An inactive (`rand_mode(0)`) enum variable behaves as a state
    /// variable (LRM 18.8) and so must not be forced into its enum domain;
    /// the dispatcher drops exactly these conjuncts.
    pub domain_conjunct: Vec<Option<usize>>,
    /// `solve ... before` edges `(first, later)` over [`Self::vars`] (LRM
    /// 18.5.9), in source order. Acyclic: [`Builder::finish`] checks.
    pub before: Vec<(VarId, VarId)>,
    /// The `dist` constraints (LRM 18.5.3). Dist `j`'s hidden selector
    /// variable is `SELECTOR_BASE + j`; its membership conjunct is already in
    /// [`Self::conjuncts`], and the weighting is applied when the solution is
    /// drawn (see [`super::dist`]).
    pub dists: Vec<Dist>,
    /// The `real`/`shortreal` random variables, indexed by the real
    /// namespace's own ids (the `Var` ids of [`Self::real`]).
    pub real_vars: Vec<RealVarInfo>,
    /// The constraints over [`Self::real_vars`], solved after the integral
    /// variables (see [`super::real_domain`]).
    pub real: RealProblem,
    /// The dynamic arrays and queues the constraints reach, indexed by
    /// [`super::ir::ArrayId`] (see [`ArrayInfo`]).
    pub arrays: Vec<ArrayInfo>,
    /// The functions the constraints call, indexed by [`super::ir::FuncId`].
    pub funcs: Vec<Func>,
    /// The soft constraints (LRM 18.5.13): soft `k`'s discard flag is
    /// `SOFT_BASE + k` in [`Self::conjuncts`] (see [`priority`]). Those a
    /// higher-priority `disable soft` reaches are already marked disabled.
    pub softs: Vec<Soft>,
    /// The call-site locals an inline constraint reads (empty outside
    /// [`Builder::set_local_classifier`] mode); each is one of [`Self::states`].
    pub captures: Vec<CaptureInfo>,
    /// One entry per [`Builder::add_block`] call, in call order: which of
    /// [`Self::conjuncts`] the block produced and whether it can be switched
    /// off (see [`BlockInfo`]).
    pub blocks: Vec<BlockInfo>,
    /// How many `disable soft`s the constraints hold (the table
    /// [`Soft::disabled_by`] indexes).
    pub disables: usize,
    /// The target of each `disable soft`, in the order of [`Self::disables`]'s
    /// table: an inline constraint's are applied to the object's own softs
    /// when the fragment is overlaid (LRM 18.5.13.2, 18.7).
    pub disable_keys: Vec<SoftKey>,
}

/// What one constraint block contributed to a [`ConstraintSet`]; the data
/// `constraint_mode(0)` needs (LRM 18.9).
#[derive(Clone, Debug, PartialEq, Eq, Default)]
pub struct BlockInfo {
    /// The block's conjuncts, as a range of [`ConstraintSet::conjuncts`]
    /// (empty for an extern prototype with no body, which is a constraint of
    /// no effect). The implicit enum-domain conjuncts are not part of any
    /// block.
    pub conjuncts: std::ops::Range<usize>,
    /// What the block added besides conjuncts (a `dist`, a `solve ... before`,
    /// a `real` constraint, a `disable soft`), which a call that has the block
    /// switched off must leave out as well.
    pub items: BlockItems,
}

/// The AST to IR builder; see the module docs.
pub struct Builder<'t> {
    trees: &'t [SyntaxTree],
    vars: Vec<VarInfo>,
    var_ix: HashMap<SymbolId, u32>,
    /// Pattern variables (`.n`) in scope while a `matches` conditional is
    /// built, each bound to its subject's expression (LRM 12.6).
    pattern_binds: HashMap<SymbolId, Expr>,
    /// Aggregate leaves declared as random variables, by property and path.
    elem_ix: HashMap<(SymbolId, Vec<Step>), u32>,
    /// Non-property aggregate variables declared random for one call
    /// ([`Builder::declare_aggregate_forced`], `std::randomize`, LRM 18.12).
    forced_roots: HashSet<SymbolId>,
    real_vars: Vec<RealVarInfo>,
    real_var_ix: HashMap<SymbolId, u32>,
    /// Real aggregate leaves declared as random variables, by property and path.
    real_leaf_ix: HashMap<(SymbolId, Vec<Step>), u32>,
    /// State variables that are leaves of an aggregate property.
    leaf_state_ix: HashMap<(SymbolId, Vec<Step>), u32>,
    real_conds: Vec<RealCond>,
    real_dists: Vec<RealDist>,
    real_before: Vec<(u32, u32)>,
    states: Vec<StateInfo>,
    /// State variables by path: the root symbol, then each hop's.
    state_ix: HashMap<(Vec<SymbolId>, u32), u32>,
    slot_of: Option<SlotResolver<'t>>,
    /// The implementation of a virtual function in the randomized object's
    /// own class, when the caller knows it ([`Builder::set_virtual_resolver`]).
    virtual_impl: Option<VirtualResolver<'t>>,
    /// Every implementation a virtual function can have on the objects a
    /// handle of a given static class may name ([`Builder::set_virtual_targets`]).
    virtual_targets: Option<VirtualTargets<'t>>,
    conjuncts: Vec<Expr>,
    before: Vec<(VarId, VarId)>,
    dists: Vec<Dist>,
    /// Dynamic arrays and queues, by id and by symbol.
    arrays: Vec<ArrayInfo>,
    array_ix: HashMap<SymbolId, u32>,
    /// The `foreach` and array-method names in scope, innermost last.
    loops: Vec<LoopScope>,
    next_loop: u32,
    /// Set while building a construct that cannot hold array-level values (a
    /// `dist` item), naming it.
    no_arrays: Option<&'static str>,
    /// The functions called so far, by id and by symbol.
    funcs: Vec<Func>,
    func_ix: HashMap<(SymbolId, Vec<SymbolId>), u32>,
    /// While the body of a function called through an object handle
    /// (`h.f()`, LRM 18.5.12) is built: where that object lives, so the
    /// properties the body reads are state variables read through it.
    fn_base: Option<funcs::FnBase>,
    /// The frame of the function body being built, if any.
    frame: Option<funcs::Frame>,
    /// The soft constraints and `disable soft`s built so far (C15).
    softs: Vec<Soft>,
    disables: Vec<Disable>,
    /// The (object rank, class level) the next constraints are built at, and
    /// the running declaration sequence (see [`Self::set_priority_scope`]).
    scope: (u32, u32),
    seq: u32,
    /// How many implication / `if` constraints enclose the one being built.
    guard_depth: u32,
    /// Inline-constraint mode (C19): which names are locals of the call site,
    /// the locals read so far (by key, into [`Self::captures`]).
    local_of: Option<LocalClassifier<'t>>,
    captures: Vec<CaptureInfo>,
    capture_ix: HashMap<Vec<SymbolId>, usize>,
    /// What each block added ([`ConstraintSet::blocks`]).
    blocks: Vec<BlockInfo>,
}

/// Places a class property in its object's field buffer (the object layout
/// lives in the code generator, so the builder is handed this).
/// Maps `(virtual function, static class of the receiver)` to every
/// `(dynamic class template id, implementation)` pair the call can run.
type VirtualTargets<'t> =
    Box<dyn for<'s> Fn(Symbol<'s>, Symbol<'s>) -> Vec<(u32, Symbol<'t>)> + 't>;
type VirtualResolver<'t> = Box<dyn for<'s> Fn(Symbol<'s>) -> Option<Symbol<'t>> + 't>;
type SlotResolver<'t> = Box<dyn for<'s> Fn(Symbol<'s>) -> Result<FieldSlot, String> + 't>;

/// A `solve ... before` operand, in the namespace of the variable it names.
#[derive(Clone, Copy, Debug)]
enum SolveOperand {
    Int(VarId),
    Real(u32),
    /// `A.size` of a dynamic array or queue (LRM 18.4, 18.5.9).
    Size,
}

/// The type of a class handle value: the object table's 64-bit id, `0` for
/// `null`. Handles are only ever compared in a constraint.
const HANDLE_TY: Ty = Ty::unsigned(64);

/// How a `[a ... b]` value range reads its operands (LRM 11.4.13, 18.5.3).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
enum RangeOp {
    /// `[a:b]`.
    Span,
    /// `[a +/- b]`: `[a - b : a + b]`.
    Abs,
    /// `[a +%- b]`: `[a - a*b/100 : a + a*b/100]`.
    Pct,
}

/// The inclusive bounds of a value range, each with the type the compared
/// value and the bound are converted to (LRM 11.8); `None` is `$`.
struct Bounds {
    lo: Option<(Ty, Expr)>,
    hi: Option<(Ty, Expr)>,
}

/// The type two operands of one comparison are converted to (LRM 11.8.1).
fn common_ty(a: Ty, b: Ty) -> Ty {
    Ty {
        width: a.width.max(b.width),
        signed: a.signed && b.signed,
    }
}

/// Whether `t` is a class handle or the `null` literal's type.
fn is_handle_type(t: Option<Type<'_>>) -> bool {
    t.is_some_and(|t| {
        let c = t.canonical();
        c.is_class() || c.is_null()
    })
}

fn ty_of(t: Option<Type<'_>>, what: &str) -> Result<Ty, BuildError> {
    let t = t.ok_or_else(|| BuildError::Missing {
        what: format!("type for {what}"),
    })?;
    if t.is_virtual_interface() {
        return Err(BuildError::NonIntegral {
            what: format!("{what} of virtual interface type"),
        });
    }
    if !t.is_integral() {
        return Err(BuildError::NonIntegral {
            what: format!("{what} of type `{}`", t.to_sv_string()),
        });
    }
    let width = u32::try_from(t.bit_width()).map_err(|_| BuildError::Missing {
        what: format!("representable width for {what}"),
    })?;
    if width == 0 {
        return Err(BuildError::NonIntegral {
            what: format!("zero-width {what}"),
        });
    }
    Ok(Ty {
        width,
        signed: t.is_signed(),
    })
}

/// A constant of `ty` holding the (possibly negative) `v`, reduced mod
/// `2^width`.
fn iconst(ty: Ty, v: i64) -> Expr {
    let m = BigInt::one() << ty.width;
    let r = ((BigInt::from(v) % &m) + &m) % &m;
    Expr::Const(ty, r.to_biguint().expect("reduced into [0, 2^w)"))
}

fn svint_to_biguint(v: &SVInt, ty: Ty) -> Result<BigUint, BuildError> {
    if v.has_unknown() {
        return Err(BuildError::FourStateLiteral {
            text: format!("{v:?}"),
        });
    }
    let w = v.bit_width();
    let bits = v.bits();
    let mut acc = BigUint::zero();
    for (i, b) in bits.iter().enumerate() {
        if *b == Bit::One {
            acc.set_bit(i as u64, true);
        }
    }
    if ty.width > w && v.is_signed() && bits.last() == Some(&Bit::One) {
        acc |= mask(ty.width) ^ mask(w);
    }
    Ok(acc & mask(ty.width))
}

/// Converts `x` to `to` the way LRM 11.8.2 does when the *context* is `to`:
/// an unsigned context zero-extends even a signed operand.
fn coerce(x: Expr, to: Ty) -> Expr {
    let from = x.ty();
    if from == to {
        return x;
    }
    if !to.signed && from.signed && to.width > from.width {
        let unsigned = Expr::Resize(Box::new(x), Ty::unsigned(from.width));
        return Expr::Resize(Box::new(unsigned), to);
    }
    Expr::Resize(Box::new(x), to)
}

fn to_bool(x: Expr) -> Expr {
    if x.ty() == Ty::BIT {
        return x;
    }
    let zero = Expr::Const(x.ty(), BigUint::zero());
    Expr::Binary(BinOp::Ne, Box::new(x), Box::new(zero), Ty::BIT)
}

fn and_all(mut parts: Vec<Expr>) -> Expr {
    if parts.is_empty() {
        return Expr::Const(Ty::BIT, BigUint::one());
    }
    let first = parts.remove(0);
    parts.into_iter().fold(to_bool(first), |acc, p| {
        Expr::Binary(BinOp::LogAnd, Box::new(acc), Box::new(to_bool(p)), Ty::BIT)
    })
}

/// `base ** exp` (LRM 11.4.3) as square-and-multiply over the exponent's
/// bits, so the solver sees only multiplies and muxes. `base` is already in
/// the context type `ty`; the exponent is self-determined. A negative
/// (signed) exponent follows the LRM's table: `1 ** n` is 1, `(-1) ** n` is
/// -1 for odd `n` and 1 for even `n`, and any other base gives 0 (integer
/// `1 / base^|n|`; `0 ** negative` is `x` in the LRM and 0 in two-state).
fn power(base: Expr, exp: Expr, ty: Ty) -> Expr {
    let one = || Expr::Const(ty, BigUint::from(1u8));
    let ew = exp.ty().width;
    let mag_bits = if exp.ty().signed { ew - 1 } else { ew };
    let bit = |i: u32| Expr::Slice(Box::new(exp.clone()), i, Ty::BIT);
    let mut acc = one();
    let mut sq = base.clone();
    for i in 0..mag_bits {
        acc = Expr::Ite(
            Box::new(bit(i)),
            Box::new(bin(BinOp::Mul, acc.clone(), sq.clone(), ty)),
            Box::new(acc),
            ty,
        );
        if i + 1 < mag_bits {
            sq = bin(BinOp::Mul, sq.clone(), sq, ty);
        }
    }
    if !exp.ty().signed {
        return acc;
    }
    let is = |v: Expr| bin(BinOp::Eq, base.clone(), v, Ty::BIT);
    let mut neg = Expr::Const(ty, BigUint::default());
    if ty.signed {
        let minus_one = Expr::Const(ty, (BigUint::from(1u8) << ty.width) - 1u8);
        let alt = Expr::Ite(
            Box::new(bit(0)),
            Box::new(minus_one.clone()),
            Box::new(one()),
            ty,
        );
        neg = Expr::Ite(Box::new(is(minus_one)), Box::new(alt), Box::new(neg), ty);
    }
    neg = Expr::Ite(Box::new(is(one())), Box::new(one()), Box::new(neg), ty);
    Expr::Ite(Box::new(bit(ew - 1)), Box::new(neg), Box::new(acc), ty)
}

fn bin(op: BinOp, l: Expr, r: Expr, ty: Ty) -> Expr {
    Expr::Binary(op, Box::new(l), Box::new(r), ty)
}

/// Declared select geometry of a packed value, in elements of `ew` bits.
struct Geom {
    left: i64,
    right: i64,
    ew: u32,
}

impl Geom {
    fn descending(&self) -> bool {
        self.left >= self.right
    }
    fn elems(&self) -> i64 {
        (self.left - self.right).abs() + 1
    }
    /// Physical element position of declared index `i`.
    fn pos(&self, i: i64) -> i64 {
        if self.descending() {
            i - self.right
        } else {
            self.right - i
        }
    }
    fn of(ty: Type<'_>, width: u32, what: &str) -> Result<Geom, BuildError> {
        if ty.is_packed_array() {
            let r = ty.packed_array_range();
            let ew = ty
                .element_type()
                .map_or(1, |e| u32::try_from(e.bit_width()).unwrap_or(1).max(1));
            if u64::from(r.width()) * u64::from(ew) == u64::from(width) {
                return Ok(Geom {
                    left: i64::from(r.left),
                    right: i64::from(r.right),
                    ew,
                });
            }
        } else if ty.is_integral() && !ty.is_struct() {
            let r = ty.bit_vector_range();
            if r.width() == width {
                return Ok(Geom {
                    left: i64::from(r.left),
                    right: i64::from(r.right),
                    ew: 1,
                });
            }
        }
        Err(unsupported(
            format!("a select into {what} of type `{}`", ty.to_sv_string()),
            "C11",
        ))
    }
}

/// The uids along a handle chain `a.b.c` (`[a, b, c]`), for matching a
/// captured member read to its occurrence in the constraint ([`CaptureInfo::hops`]).
pub fn handle_path_uids(e: Expression<'_>) -> Option<Vec<SymbolId>> {
    Builder::handle_path(e)
        .ok()
        .map(|p| p.iter().map(|s| s.uid()).collect())
}

impl<'t> Builder<'t> {
    /// A builder reading `soft` markers from `trees` (the design's syntax
    /// trees; `soft` is not exposed by the AST, plan decision E7).
    pub fn new(trees: &'t [SyntaxTree]) -> Self {
        Builder {
            trees,
            vars: Vec::new(),
            var_ix: HashMap::new(),
            pattern_binds: HashMap::new(),
            elem_ix: HashMap::new(),
            forced_roots: HashSet::new(),
            real_vars: Vec::new(),
            real_var_ix: HashMap::new(),
            real_leaf_ix: HashMap::new(),
            leaf_state_ix: HashMap::new(),
            real_conds: Vec::new(),
            real_dists: Vec::new(),
            real_before: Vec::new(),
            states: Vec::new(),
            state_ix: HashMap::new(),
            slot_of: None,
            virtual_impl: None,
            virtual_targets: None,
            conjuncts: Vec::new(),
            before: Vec::new(),
            dists: Vec::new(),
            arrays: Vec::new(),
            array_ix: HashMap::new(),
            loops: Vec::new(),
            next_loop: 0,
            no_arrays: None,
            funcs: Vec::new(),
            func_ix: HashMap::new(),
            fn_base: None,
            frame: None,
            softs: Vec::new(),
            disables: Vec::new(),
            scope: (0, 0),
            seq: 0,
            guard_depth: 0,
            local_of: None,
            captures: Vec::new(),
            capture_ix: HashMap::new(),
            blocks: Vec::new(),
        }
    }

    /// Puts the builder in *inline-constraint* mode (constraints plan C19, LRM
    /// 18.7): the constraints fed in next are those of a `randomize() with
    /// {...}` call, and `classify` says which names they read resolve in the
    /// scope of the call (a local variable, a subroutine argument, a property
    /// of the calling class, or anything `local::`-qualified) and not in the
    /// randomized object's class. Each such local becomes a *captured* state
    /// variable ([`ConstraintSet::captures`]): a constant of the solve whose
    /// value the call supplies. Only integral locals can be read. A `disable
    /// soft` is recorded ([`ConstraintSet::disable_keys`]) and reaches the
    /// object's own soft constraints when the fragment is overlaid.
    pub fn set_local_classifier(&mut self, classify: impl for<'s> Fn(Expression<'s>) -> bool + 't) {
        self.local_of = Some(Box::new(classify));
    }

    /// The state variable standing for the call-site local `sym` of type `ty`,
    /// registered on first use.
    fn capture_ref(&mut self, sym: Symbol<'_>, ty: Ty) -> Expr {
        self.capture_path(sym, &[], ty)
    }

    /// The state variable for the call-site value `sym.hops...` (a local, or a
    /// member read through a local object handle).
    fn capture_path(&mut self, sym: Symbol<'_>, hops: &[Symbol<'_>], ty: Ty) -> Expr {
        let uid = sym.uid();
        let key: Vec<SymbolId> = std::iter::once(uid.clone())
            .chain(hops.iter().map(|h| h.uid()))
            .collect();
        if let Some(&ix) = self.capture_ix.get(&key) {
            let state = self.captures[ix].state;
            return Expr::State(state, self.states[state as usize].ty);
        }
        let name = hops
            .iter()
            .fold(sym.name().to_string(), |n, h| format!("{n}.{}", h.name()));
        let state = self.states.len() as u32;
        self.states.push(StateInfo {
            root_bit: 0,
            symbol: uid.clone(),
            name: name.clone(),
            ty,
            via: Vec::new(),
            window: None,
            class_of: false,
        });
        self.capture_ix.insert(key, self.captures.len());
        self.captures.push(CaptureInfo {
            state,
            symbol: uid,
            hops: hops.iter().map(|h| h.uid()).collect(),
            name,
            ty,
        });
        Expr::State(state, ty)
    }

    /// Sets the priority scope of the constraints added from now on (LRM
    /// 18.5.13.1): the rank of the object they belong to (an object a `rand`
    /// handle contains ranks below its container, see
    /// [`priority::object_order`]) and their class level (a derived class's
    /// level is above its bases'). Within a scope a later soft constraint
    /// is higher; the default scope is `(0, 0)`.
    pub fn set_priority_scope(&mut self, object: u32, level: u32) {
        self.scope = (object, level);
    }

    fn next_priority(&mut self) -> Priority {
        let p = Priority {
            object: self.scope.0,
            level: self.scope.1,
            seq: self.seq,
        };
        self.seq += 1;
        p
    }

    /// The soft constraint `body` (already built; `dists` is the range of
    /// [`Self::dists`] it created), recorded and wrapped in its discard flag.
    fn make_soft(&mut self, body: Expr, dists: std::ops::Range<usize>) -> Result<Expr, BuildError> {
        if self.in_runtime_loop() || self.frame.is_some() {
            return Err(BuildError::BadSoft {
                what: "a `soft` constraint inside a `foreach` over a dynamic array or queue is \
                       not supported: it would be one soft constraint per run-time element"
                    .into(),
            });
        }
        let dist_refs: Vec<&Dist> = self.dists[dists.clone()].iter().collect();
        let keys = priority::keys_of(&body, &dist_refs);
        for k in &keys {
            if let SoftKey::Var(v) = k
                && self.vars[*v as usize].randc
            {
                return Err(BuildError::BadSoft {
                    what: format!(
                        "a `soft` constraint on the `randc` variable `{}` (soft constraints \
                         apply to `rand` variables only)",
                        self.vars[*v as usize].name
                    ),
                });
            }
        }
        let id = self.softs.len() as u32;
        let priority = self.next_priority();
        self.softs.push(Soft {
            priority,
            dists: dists.map(|d| d as u32).collect(),
            keys,
            disabled: false,
            disabled_by: Vec::new(),
        });
        Ok(priority::wrap_soft(id, body))
    }

    /// `disable soft target;` (18.5.13.2).
    fn disable_soft(&mut self, c: Constraint<'_>) -> Result<(), BuildError> {
        if self.guard_depth > 0 || self.in_runtime_loop() {
            return Err(BuildError::BadSoft {
                what: "a `disable soft` inside an implication, an `if` or a `foreach` over a \
                       dynamic array or queue is not supported (it discards unconditionally)"
                    .into(),
            });
        }
        let target = c
            .children()
            .into_iter()
            .find_map(|n| n.as_expression())
            .ok_or_else(|| BuildError::Missing {
                what: "target expression of `disable soft`".into(),
            })?;
        let key = if let Some(arr) = Self::size_call_array(target) {
            SoftKey::ArraySize(self.array_of(arr)?)
        } else if let Some(chain) = aggregate::aggregate_chain(target, &self.forced_roots)
            && !chain.steps.is_empty()
        {
            let (leaf, declared) = self.declared_leaf(chain, "the target of `disable soft`")?;
            match declared {
                Some(Declared::Int(id)) => SoftKey::Var(id),
                Some(Declared::Real(_)) => {
                    return Err(BuildError::BadSoft {
                        what: "`disable soft` of a real variable is not supported (soft \
                               constraints are relaxed over integral variables only)"
                            .into(),
                    });
                }
                None => {
                    return Err(BuildError::BadSoft {
                        what: format!(
                            "`disable soft` names `{}`, which is not a `rand` variable of this \
                             class",
                            leaf.name
                        ),
                    });
                }
            }
        } else {
            let sym = match target.kind() {
                ExpressionKind::NamedValue => target.referenced_symbol(),
                ExpressionKind::MemberAccess => {
                    let base = Self::operand(target, "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: "the target of `disable soft`".into(),
                        });
                    }
                    target.member_symbol()
                }
                other => {
                    return Err(BuildError::BadSoft {
                        what: format!(
                            "a `{other:?}` expression as the target of `disable soft` (name a \
                             whole variable, `this.v` or `A.size`)"
                        ),
                    });
                }
            };
            let sym = sym.ok_or_else(|| BuildError::Missing {
                what: "symbol of the target of `disable soft`".into(),
            })?;
            let uid = sym.uid();
            if let Some(&id) = self.var_ix.get(&uid) {
                SoftKey::Var(id)
            } else if self.array_ix.contains_key(&uid) {
                SoftKey::Array(self.array_of(target)?)
            } else if self.real_var_ix.contains_key(&uid) {
                return Err(BuildError::BadSoft {
                    what: "`disable soft` of a real variable is not supported (soft constraints \
                           are relaxed over integral variables only)"
                        .into(),
                });
            } else {
                return Err(BuildError::BadSoft {
                    what: format!(
                        "`disable soft` names `{}`, which is not a `rand` variable of this class",
                        sym.name()
                    ),
                });
            }
        };
        let priority = self.next_priority();
        self.disables.push(Disable { priority, key });
        Ok(())
    }

    /// Lets constraints read members of *other* objects through non-`rand`
    /// handles (`a.x`, `next.n`; LRM 18.5.12): each such read becomes a state
    /// variable whose [`StateInfo::via`] path `resolver` places. Without a
    /// resolver, such a read is [`BuildError::ForeignObjectAccess`].
    pub fn set_slot_resolver(
        &mut self,
        resolver: impl for<'s> Fn(Symbol<'s>) -> Result<FieldSlot, String> + 't,
    ) {
        self.slot_of = Some(Box::new(resolver));
    }

    /// Tells the builder which function a call to a `virtual` function runs: the
    /// constraints are built for one concrete class, so the override that
    /// class (or its nearest base) declares is the one an object of it calls
    /// (LRM 8.20). `resolver` maps the statically named function to that
    /// implementation, or `None` when it cannot. Without a resolver, a call to
    /// a virtual function is refused.
    pub fn set_virtual_resolver(
        &mut self,
        resolver: impl for<'s> Fn(Symbol<'s>) -> Option<Symbol<'t>> + 't,
    ) {
        self.virtual_impl = Some(Box::new(resolver));
    }

    /// Tells the builder, for a call to a `virtual` function through an object
    /// handle (the object's dynamic class is known only at solve time, LRM
    /// 8.20), every `(template id, implementation)` pair of the classes a handle
    /// of the given static class can name. The call is then built as a
    /// run-time pick among the implementations on the object's template id.
    pub fn set_virtual_targets(
        &mut self,
        resolver: impl for<'s> Fn(Symbol<'s>, Symbol<'s>) -> Vec<(u32, Symbol<'t>)> + 't,
    ) {
        self.virtual_targets = Some(Box::new(resolver));
    }

    /// Registers `sym` as an active random variable and returns its id
    /// (idempotent).
    pub fn declare_rand(&mut self, sym: Symbol<'_>) -> Result<u32, BuildError> {
        let uid = sym.uid();
        if let Some(&id) = self.var_ix.get(&uid) {
            return Ok(id);
        }
        let name = sym.name().to_string();
        let randc = match sym.rand_mode() {
            RandMode::None => return Err(BuildError::NotRand { name }),
            RandMode::RandC => true,
            RandMode::Rand => false,
        };
        let vt = sym.value_type().ok_or_else(|| BuildError::Missing {
            what: format!("value type for `{name}`"),
        })?;
        let id = self.new_rand_var(uid.clone(), name, vt, randc, Vec::new(), None)?;
        self.var_ix.insert(uid, id);
        Ok(id)
    }

    /// Registers `sym` as a random variable whether or not it is declared
    /// `rand` (LRM 18.11: an argument of `randomize(v1, v2)` is random for that
    /// call). The argument list does not change the cyclic nature of a `randc`
    /// property, which stays `randc`; a non-`rand` property is never `randc`.
    /// Idempotent, and returns the id [`Self::declare_rand`] would also have
    /// given a `rand` property.
    pub fn declare_var_forced(&mut self, sym: Symbol<'_>) -> Result<u32, BuildError> {
        let uid = sym.uid();
        if let Some(&id) = self.var_ix.get(&uid) {
            return Ok(id);
        }
        let name = sym.name().to_string();
        let randc = matches!(sym.rand_mode(), RandMode::RandC);
        let vt = sym.value_type().ok_or_else(|| BuildError::Missing {
            what: format!("value type for `{name}`"),
        })?;
        let id = self.new_rand_var(uid.clone(), name, vt, randc, Vec::new(), None)?;
        self.var_ix.insert(uid, id);
        Ok(id)
    }

    /// The named constants of an enum type `vt` as values of `ty` (LRM 18.3:
    /// a `rand` enum only takes these), or `None` for any other type.
    fn enum_values(vt: Type<'_>, ty: Ty) -> Result<Option<Vec<BigUint>>, BuildError> {
        if !vt.is_enum() {
            return Ok(None);
        }
        let mut vals = Vec::new();
        for m in vt.canonical().enum_members() {
            let cv = m.constant_value().ok_or_else(|| BuildError::Missing {
                what: format!("value of enum member `{}`", m.name()),
            })?;
            let i = cv.as_integer().ok_or_else(|| BuildError::Missing {
                what: format!("integer value of enum member `{}`", m.name()),
            })?;
            vals.push(svint_to_biguint(i, ty)?);
        }
        Ok(Some(vals))
    }

    /// Appends a random variable of type `vt` (its declaring symbol's key
    /// `uid`; `path` and `window` place it when it is a leaf of an aggregate
    /// property, and are empty / `None` for a property itself).
    fn new_rand_var(
        &mut self,
        uid: SymbolId,
        name: String,
        vt: Type<'_>,
        randc: bool,
        path: Vec<Step>,
        window: Option<Window>,
    ) -> Result<u32, BuildError> {
        if vt.is_virtual_interface() {
            return Err(BuildError::VirtualInterfaceRand { name });
        }
        let ty = ty_of(Some(vt), &format!("`rand` variable `{name}`"))?;
        if randc && ty.width > MAX_RANDC_WIDTH {
            return Err(BuildError::RandcTooWide {
                name,
                width: ty.width,
                max: MAX_RANDC_WIDTH,
            });
        }
        let enum_domain = Self::enum_values(vt, ty)?;
        let id = self.vars.len() as u32;
        self.vars.push(VarInfo {
            symbol: uid,
            name,
            ty,
            enum_domain,
            randc,
            path,
            window,
        });
        Ok(id)
    }

    /// Adds every constraint of the named constraint block `block`.
    pub fn add_block(&mut self, block: Symbol<'_>) -> Result<(), BuildError> {
        let start = self.conjuncts.len();
        let from = [
            self.dists.len(),
            self.softs.len(),
            self.before.len(),
            self.real_conds.len(),
            self.real_dists.len(),
            self.real_before.len(),
            self.disables.len(),
        ];
        self.add_block_body(block)?;
        self.blocks.push(BlockInfo {
            conjuncts: start..self.conjuncts.len(),
            items: BlockItems {
                dists: from[0]..self.dists.len(),
                softs: from[1]..self.softs.len(),
                before: from[2]..self.before.len(),
                real_conds: from[3]..self.real_conds.len(),
                real_dists: from[4]..self.real_dists.len(),
                real_before: from[5]..self.real_before.len(),
                disables: from[6]..self.disables.len(),
            },
        });
        Ok(())
    }

    fn add_block_body(&mut self, block: Symbol<'_>) -> Result<(), BuildError> {
        let tree = block
            .constraint_block_constraints()
            .ok_or_else(|| BuildError::Missing {
                what: format!("bound body for constraint block `{}`", block.name()),
            })?;
        let c = tree.as_constraint().ok_or_else(|| BuildError::Missing {
            what: format!("constraint body of block `{}`", block.name()),
        })?;
        // A constraint prototype whose external block was never provided
        // (18.5.1): the explicit form `extern constraint p;` is an error, the
        // implicit form `constraint p;` is an empty constraint (one with no
        // effect on randomization, "equivalent to a constraint block
        // containing the constant expression 1"). `pure` prototypes carry no
        // body by definition and are skipped by the caller.
        let flags = block.constraint_block_flags();
        if c.kind() == ConstraintKind::Invalid
            && flags.contains(ConstraintBlockFlags::EXTERN)
            && !flags.contains(ConstraintBlockFlags::PURE)
        {
            if flags.contains(ConstraintBlockFlags::EXPLICIT_EXTERN) {
                return Err(BuildError::MissingExternBody {
                    name: block.name().to_string(),
                });
            }
            return Ok(());
        }
        self.add_constraint(c)
    }

    /// Adds one constraint (a block body, a list, or a single item).
    pub fn add_constraint(&mut self, c: Constraint<'_>) -> Result<(), BuildError> {
        let mut out = self.constraint(c)?;
        self.conjuncts.append(&mut out);
        Ok(())
    }

    /// Finishes: appends the implicit enum-domain conjuncts and validates.
    pub fn finish(mut self) -> Result<ConstraintSet, BuildError> {
        let mut domain_conjunct = vec![None; self.vars.len()];
        for (i, v) in self.vars.iter().enumerate() {
            let Some(domain) = &v.enum_domain else {
                continue;
            };
            let var = Expr::Var(i as u32, v.ty);
            let mut any: Option<Expr> = None;
            for val in domain {
                let eq = bin(
                    BinOp::Eq,
                    var.clone(),
                    Expr::Const(v.ty, val.clone()),
                    Ty::BIT,
                );
                any = Some(match any {
                    None => eq,
                    Some(prev) => bin(BinOp::LogOr, prev, eq, Ty::BIT),
                });
            }
            if let Some(e) = any {
                domain_conjunct[i] = Some(self.conjuncts.len());
                self.conjuncts.push(e);
            }
        }
        for c in &self.conjuncts {
            c.validate()?;
        }
        for d in &self.dists {
            d.validate()?;
        }
        order::levels(self.vars.len(), &self.before)?;
        let (real_vars, real) = self.finish_real()?;
        priority::apply_disables(&mut self.softs, &self.disables);
        Ok(ConstraintSet {
            vars: self.vars,
            states: self.states,
            conjuncts: self.conjuncts,
            domain_conjunct,
            before: self.before,
            dists: self.dists,
            real_vars,
            real,
            arrays: self.arrays,
            funcs: self.funcs,
            softs: self.softs,
            captures: self.captures,
            blocks: self.blocks,
            disables: self.disables.len(),
            disable_keys: self.disables.iter().map(|d| d.key).collect(),
        })
    }

    /// How many of a `solve ... before` constraint's operands are on the
    /// `solve` side. The semantic node lists both sides' expressions in one
    /// run, so the split comes from the syntax.
    fn solve_side_len(&self, c: Constraint<'_>) -> Result<usize, BuildError> {
        for tree in self.trees {
            if let Some(node) = c.syntax(tree) {
                let s =
                    SolveBeforeConstraintSyntax::cast(node).ok_or_else(|| BuildError::Missing {
                        what: "`solve ... before` syntax for a SolveBefore constraint".into(),
                    })?;
                return Ok(s.before_expr().iter().count());
            }
        }
        Err(BuildError::Missing {
            what: "syntax node for a constraint (is its syntax tree passed to the builder?)".into(),
        })
    }

    /// The random variable a `solve ... before` operand names (LRM 18.5.9:
    /// `rand` only, integral or real; a `randc` variable is always solved
    /// first and is not allowed here).
    fn solve_operand(&mut self, e: Expression<'_>) -> Result<SolveOperand, BuildError> {
        // A member of an unpacked struct or an element of an unpacked array
        // property, at constant indices.
        if let Some(chain) = aggregate::aggregate_chain(e, &self.forced_roots)
            && !chain.steps.is_empty()
        {
            let (leaf, declared) = self.declared_leaf(chain, "a `solve ... before` operand")?;
            if leaf.randc() {
                return Err(BuildError::BadSolveOperand {
                    what: format!(
                        "`{}` is `randc`, which is always solved before every `rand` variable",
                        leaf.name
                    ),
                });
            }
            return match declared {
                Some(Declared::Int(id)) => Ok(SolveOperand::Int(id)),
                Some(Declared::Real(id)) => Ok(SolveOperand::Real(id)),
                None => Err(BuildError::BadSolveOperand {
                    what: format!("`{}` is not a `rand` variable of this class", leaf.name),
                }),
            };
        }
        let sym = match e.kind() {
            ExpressionKind::NamedValue => 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!(
                            "`solve ... before` operand `.{}`",
                            e.member_symbol()
                                .map_or(String::new(), |m| m.name().to_string())
                        ),
                    });
                }
                e.member_symbol()
            }
            ExpressionKind::Call => {
                let Some(arr) = Self::size_call_array(e) else {
                    return Err(unsupported(
                        "a call other than `array.size` as a `solve ... before` operand",
                        "C11",
                    ));
                };
                self.arrays_allowed("an array size")?;
                self.array_of(arr)?;
                return Ok(SolveOperand::Size);
            }
            other => {
                return Err(unsupported(
                    format!("a `{other:?}` expression as a `solve ... before` operand"),
                    "C11",
                ));
            }
        };
        let sym = sym.ok_or_else(|| BuildError::Missing {
            what: "symbol of a `solve ... before` operand".into(),
        })?;
        let name = sym.name().to_string();
        if sym.rand_mode() == RandMode::RandC {
            return Err(BuildError::BadSolveOperand {
                what: format!(
                    "`{name}` is `randc`, which is always solved before every `rand` variable"
                ),
            });
        }
        let uid = sym.uid();
        if let Some(&id) = self.var_ix.get(&uid) {
            return Ok(SolveOperand::Int(id));
        }
        match self.real_var_ix.get(&uid) {
            Some(&id) => Ok(SolveOperand::Real(id)),
            None => Err(BuildError::BadSolveOperand {
                what: format!("`{name}` is not a `rand` variable of this class"),
            }),
        }
    }

    fn is_soft(&self, c: Constraint<'_>) -> Result<bool, BuildError> {
        for tree in self.trees {
            if let Some(node) = c.syntax(tree) {
                return Ok(
                    ExpressionConstraintSyntax::cast(node).is_some_and(|s| s.soft().is_some())
                );
            }
        }
        Err(BuildError::Missing {
            what: "syntax node for a constraint (is its syntax tree passed to the builder?)".into(),
        })
    }

    fn constraint(&mut self, c: Constraint<'_>) -> Result<Vec<Expr>, BuildError> {
        fn kids<'d>(c: Constraint<'d>) -> Vec<Constraint<'d>> {
            c.children()
                .into_iter()
                .filter_map(|n| n.as_constraint())
                .collect()
        }
        match c.kind() {
            ConstraintKind::List => {
                let mut out = Vec::new();
                for k in kids(c) {
                    out.extend(self.constraint(k)?);
                }
                Ok(out)
            }
            ConstraintKind::Expression => {
                let soft = self.is_soft(c)?;
                let e = c.expr().ok_or_else(|| BuildError::Missing {
                    what: "expression of an expression constraint".into(),
                })?;
                if soft
                    && (real::reads_real(e)
                        || (e.kind() == ExpressionKind::Dist && real::dist_is_real(e)))
                {
                    return Err(BuildError::BadSoft {
                        what: "a `soft` constraint over a real value is not supported (soft \
                               constraints are relaxed over integral variables only)"
                            .into(),
                    });
                }
                let dists_from = self.dists.len();
                let built = if e.kind() == ExpressionKind::Dist {
                    if real::dist_is_real(e) {
                        self.real_dist(e)?;
                        return Ok(Vec::new());
                    }
                    self.dist(e)?
                } else {
                    if real::reads_real(e) {
                        let cond = self.real_cond(e)?;
                        self.real_conds.push(cond);
                        return Ok(Vec::new());
                    }
                    to_bool(self.expr(e)?)
                };
                if soft {
                    let dists = dists_from..self.dists.len();
                    return Ok(vec![self.make_soft(built, dists)?]);
                }
                Ok(vec![built])
            }
            // A guard that reads a real value is built whole over the real
            // namespace (its arms may not mix in integral variables).
            ConstraintKind::Implication | ConstraintKind::Conditional
                if real::constraint_reads_real(c) =>
            {
                let cond = self.real_constraint(c)?;
                self.real_conds.push(cond);
                Ok(Vec::new())
            }
            ConstraintKind::Implication => {
                let p = c.predicate().ok_or_else(|| BuildError::Missing {
                    what: "predicate of an implication".into(),
                })?;
                let pred = to_bool(self.expr(p)?);
                let mut body = Vec::new();
                self.guard_depth += 1;
                for k in kids(c) {
                    match self.constraint(k) {
                        Ok(b) => body.extend(b),
                        Err(e) => {
                            self.guard_depth -= 1;
                            return Err(e);
                        }
                    }
                }
                self.guard_depth -= 1;
                // A guard, not a plain `->`: its predicate follows the
                // LRM 18.5.12 three-valued evaluation.
                Ok(vec![Expr::Guard(
                    Box::new(pred),
                    Box::new(and_all(body)),
                    Box::new(Expr::Const(Ty::BIT, BigUint::one())),
                    Ty::BIT,
                )])
            }
            ConstraintKind::Conditional => {
                let p = c.predicate().ok_or_else(|| BuildError::Missing {
                    what: "predicate of an if constraint".into(),
                })?;
                let pred = to_bool(self.expr(p)?);
                let arms = kids(c);
                if arms.is_empty() || arms.len() > 2 {
                    return Err(BuildError::Missing {
                        what: format!("one or two arms of an if constraint (got {})", arms.len()),
                    });
                }
                self.guard_depth += 1;
                let arms_built = arms
                    .iter()
                    .map(|a| self.constraint(*a).map(and_all))
                    .collect::<Result<Vec<_>, _>>();
                self.guard_depth -= 1;
                let mut arms_built = arms_built?.into_iter();
                let then_c = arms_built.next().ok_or_else(|| BuildError::Missing {
                    what: "the then arm of an if constraint".into(),
                })?;
                let else_c = arms_built
                    .next()
                    .unwrap_or_else(|| Expr::Const(Ty::BIT, BigUint::one()));
                Ok(vec![Expr::Guard(
                    Box::new(pred),
                    Box::new(then_c),
                    Box::new(else_c),
                    Ty::BIT,
                )])
            }
            ConstraintKind::Uniqueness => self.unique(c),
            ConstraintKind::SolveBefore => {
                // No boolean constraint: only the solve order (LRM 18.5.9:
                // ordering never changes the solution space).
                let split = self.solve_side_len(c)?;
                let mut ids = Vec::new();
                for k in c.children() {
                    let e = k.as_expression().ok_or_else(|| BuildError::Missing {
                        what: "expression operand of `solve ... before`".into(),
                    })?;
                    ids.push(self.solve_operand(e)?);
                }
                if split > ids.len() {
                    return Err(BuildError::Missing {
                        what: "operands of `solve ... before` matching its syntax".into(),
                    });
                }
                let (first, later) = ids.split_at(split);
                for &a in first {
                    for &b in later {
                        match (a, b) {
                            (SolveOperand::Int(a), SolveOperand::Int(b)) => {
                                self.before.push((a, b));
                            }
                            (SolveOperand::Real(a), SolveOperand::Real(b)) => {
                                self.real_before.push((a, b));
                            }
                            // LRM 18.4: the sizes are decided first, as one
                            // sub-problem (`array::solve_sizes`), before any
                            // element or scalar is drawn. `solve A.size before
                            // x` is therefore the order the solver already
                            // has; the reverse, and an order between two
                            // sizes, would change the distribution and is not
                            // modelled, so it fails loudly.
                            (SolveOperand::Size, SolveOperand::Int(_) | SolveOperand::Real(_)) => {}
                            (SolveOperand::Int(_) | SolveOperand::Real(_), SolveOperand::Size)
                            | (SolveOperand::Size, SolveOperand::Size) => {
                                return Err(unsupported(
                                    "`solve ... before` placing a variable or another array size \
                                     before an array `.size()`",
                                    "array sizes are always solved first, as one joint sub-problem",
                                ));
                            }
                            // The integral variables are always solved first
                            // and nothing couples the two namespaces, so an
                            // order between them changes nothing (18.5.9).
                            _ => {}
                        }
                    }
                }
                Ok(Vec::new())
            }
            ConstraintKind::Invalid => Err(BuildError::Missing {
                what: "well-formed constraint (the frontend diagnosed an error in it)".into(),
            }),
            ConstraintKind::DisableSoft => {
                // No boolean constraint: it discards softs (see `finish`).
                self.disable_soft(c)?;
                Ok(Vec::new())
            }
            ConstraintKind::Foreach => self.foreach(c),
            other => Err(unsupported(format!("constraint kind {other:?}"), "C2")),
        }
    }

    fn symbol_ref(&mut self, sym: Symbol<'_>, ty: Ty) -> Result<Expr, BuildError> {
        // A property read by a function called through a handle belongs to the
        // object that handle names, never to the randomized one.
        if self.frame.is_some()
            && sym.kind() == SymbolKind::ClassProperty
            && let Some(base) = self.fn_base.clone()
        {
            return self.based_state(&base, &[sym], ty);
        }
        let uid = sym.uid();
        if let Some(x) = self.pattern_binds.get(&uid) {
            return Ok(x.clone());
        }
        if let Some(&id) = self.var_ix.get(&uid) {
            if self.frame.is_some() {
                return Err(self.rand_read_in_function(sym.name()));
            }
            return Ok(Expr::Var(id, self.vars[id as usize].ty));
        }
        self.state_ref(sym, &[], 0, ty)
    }

    /// The state variable for `root` (a property of the randomized class)
    /// followed through the handle members `hops`, registered on first use.
    fn state_ref(
        &mut self,
        root: Symbol<'_>,
        hops: &[Symbol<'_>],
        root_bit: u32,
        ty: Ty,
    ) -> Result<Expr, BuildError> {
        let key: Vec<SymbolId> = std::iter::once(root.uid())
            .chain(hops.iter().map(|h| h.uid()))
            .collect();
        let key = (key, root_bit);
        if let Some(&id) = self.state_ix.get(&key) {
            return Ok(Expr::State(id, self.states[id as usize].ty));
        }
        let mut name = root.name().to_string();
        let mut via = Vec::with_capacity(hops.len());
        for h in hops {
            name = format!("{name}.{}", h.name());
            let resolver =
                self.slot_of
                    .as_ref()
                    .ok_or_else(|| BuildError::ForeignObjectAccess {
                        what: format!(
                            "read of `{name}` (this builder was given no object layout to place \
                         another object's members)"
                        ),
                    })?;
            let slot = resolver(*h).map_err(|why| BuildError::Missing {
                what: format!("field slot of `{name}`: {why}"),
            })?;
            via.push(StateHop {
                symbol: h.uid(),
                slot,
            });
        }
        let id = self.states.len() as u32;
        self.states.push(StateInfo {
            symbol: root.uid(),
            name,
            ty,
            via,
            window: None,
            root_bit,
            class_of: false,
        });
        self.state_ix.insert(key, id);
        Ok(Expr::State(id, ty))
    }

    /// The named value a handle chain starts at (`o` in `o.a.b`), unless it
    /// is `this`.
    fn local_handle_root<'d>(mut e: Expression<'d>) -> Option<Expression<'d>> {
        // A predicate, not a lowering: any other expression kind is simply not
        // a handle chain with a named root.
        loop {
            let kind = e.kind();
            if kind == ExpressionKind::MemberAccess {
                e = e.left()?;
            } else if kind == ExpressionKind::Conversion {
                e = e.conversion_operand()?;
            } else if kind == ExpressionKind::NamedValue
                || kind == ExpressionKind::HierarchicalValue
            {
                return e
                    .referenced_symbol()
                    .is_some_and(|s| s.name() != "this")
                    .then_some(e);
            } else {
                return None;
            }
        }
    }

    /// The members from a handle chain's root property to its end:
    /// `a.b.c` is `[a, b, c]`; a leading `this.` is transparent (LRM 8.11).
    fn handle_path<'d>(e: Expression<'d>) -> Result<Vec<Symbol<'d>>, BuildError> {
        match e.kind() {
            ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue => {
                let sym = e.referenced_symbol().ok_or_else(|| BuildError::Missing {
                    what: "symbol of a named value".into(),
                })?;
                Ok(if sym.name() == "this" {
                    Vec::new()
                } else {
                    vec![sym]
                })
            }
            ExpressionKind::MemberAccess => {
                let mut path = Self::handle_path(Self::operand(e, "a member access")?)?;
                path.push(e.member_symbol().ok_or_else(|| BuildError::Missing {
                    what: "member symbol of a member access".into(),
                })?);
                Ok(path)
            }
            ExpressionKind::Conversion => {
                let inner = e.conversion_operand().ok_or_else(|| BuildError::Missing {
                    what: "operand of a conversion".into(),
                })?;
                Self::handle_path(inner)
            }
            // An element of a fixed array of handles (`es[i]`): the array
            // property is the root; [`Self::handle_root_element`] places the element.
            ExpressionKind::ElementSelect => {
                let arr = e.select_value().ok_or_else(|| BuildError::Missing {
                    what: "array of an element select".into(),
                })?;
                match arr.kind() {
                    ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue => {
                        Self::handle_path(arr)
                    }
                    other => Err(unsupported(
                        format!(
                            "an element of a `{other:?}` array of handles as the object of a member access"
                        ),
                        "C17 follow-up",
                    )),
                }
            }
            other => Err(unsupported(
                format!("a `{other:?}` expression as the object of a member access"),
                "C17 follow-up",
            )),
        }
    }

    /// The element of a fixed array of handles a handle chain starts at
    /// (`es[i]` in `es[i].v`), as the bit of the array property it sits at and
    /// the property's width; `None` when the chain starts at a plain handle.
    /// The index must be constant here (a literal, or an unrolled `foreach`
    /// variable): a computed index would pick among objects.
    fn handle_root_element(&mut self, e: Expression<'_>) -> Result<Option<(u32, u32)>, BuildError> {
        let mut cur = e;
        // Any other kind is a plain handle (no element of an array): a
        // predicate answer, not a lowering.
        loop {
            let kind = cur.kind();
            if kind == ExpressionKind::MemberAccess {
                cur = Self::operand(cur, "a member access")?;
            } else if kind == ExpressionKind::Conversion {
                cur = cur
                    .conversion_operand()
                    .ok_or_else(|| BuildError::Missing {
                        what: "operand of a conversion".into(),
                    })?;
            } else if kind == ExpressionKind::ElementSelect {
                break;
            } else {
                return Ok(None);
            }
        }
        let arr = cur.select_value().ok_or_else(|| BuildError::Missing {
            what: "array of an element select".into(),
        })?;
        let at = arr
            .expr_type()
            .map(|t| t.canonical())
            .ok_or_else(|| BuildError::Missing {
                what: "type of an array of handles".into(),
            })?;
        if !at.is_unpacked_array() || at.fixed_unpacked_array_range().width() == 0 {
            return Err(unsupported(
                "an element of a dynamic array, queue or associative array of handles in a constraint",
                "C17 follow-up",
            ));
        }
        let sel = cur.selector().ok_or_else(|| BuildError::Missing {
            what: "index of an element select".into(),
        })?;
        let ix = self.expr(sel)?;
        let i = Self::constant_index(&ix).ok_or_else(|| {
            unsupported(
                "an element of an array of handles at a computed index",
                "C17 follow-up",
            )
        })?;
        let r = at.fixed_unpacked_array_range();
        let lo = i64::from(r.left).min(i64::from(r.right));
        let n = i64::from(r.width());
        if !(0..n).contains(&(i - lo)) {
            return Err(BuildError::OutOfRangeSelect {
                what: format!("handle array index {i} outside [{}:{}]", r.left, r.right),
            });
        }
        Ok(Some((((i - lo) * 64) as u32, (n * 64) as u32)))
    }

    /// A value read through object handles (`a.x`, `next.next.n`, `h`): a
    /// state variable per LRM 18.5.12 (a handle that is not `rand` is not
    /// randomized, so what it designates is fixed during the solve).
    fn handle_state(&mut self, e: Expression<'_>, ty: Ty) -> Result<Expr, BuildError> {
        let path = Self::handle_path(e)?;
        if path.is_empty() {
            return Err(unsupported("a bare `this` as a value", "C17 follow-up"));
        }
        if self.frame.is_some()
            && let Some(base) = self.fn_base.clone()
        {
            // `this.p.q` in a function called through a handle: relative to
            // that handle's object.
            return self.based_state(&base, &path, ty);
        }
        let Some((root, hops)) = path.split_first() else {
            return Err(unsupported("a bare `this` as a value", "C17 follow-up"));
        };
        if self.var_ix.contains_key(&root.uid()) {
            return Err(unsupported(
                format!("the randomized handle `{}` in a constraint", root.name()),
                "C17 follow-up",
            ));
        }
        // Every step but the last must itself be a handle, or the path is
        // not a chain of objects.
        let elem = self.handle_root_element(e)?;
        for (i, step) in path[..path.len() - 1].iter().enumerate() {
            let is_handle = (i == 0 && elem.is_some())
                || step.value_type().is_some_and(|t| t.canonical().is_class());
            if !is_handle {
                return Err(unsupported(
                    format!(
                        "a member access through `{}` (step {i}), which is not a class handle",
                        step.name()
                    ),
                    "C17 follow-up",
                ));
            }
        }
        let bit = elem.map_or(0, |(b, _)| b);
        let out = self.state_ref(*root, hops, bit, ty)?;
        if let (Some((bit, whole)), true, Expr::State(id, _)) = (elem, hops.is_empty(), &out) {
            // The handle itself (`es[1] == null`) is one window of the array.
            self.states[*id as usize].window = Some(Window {
                bit,
                width: 64,
                field_width: whole,
            });
        }
        Ok(out)
    }

    /// A class-handle expression (LRM 18.5.12 compares handles only): `null`
    /// is `0`, a handle property or member a 64-bit state variable.
    fn handle_value(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        match e.kind() {
            ExpressionKind::NullLiteral => Ok(Expr::Const(HANDLE_TY, BigUint::zero())),
            // `null` or a derived handle converted to the compared type: the
            // handle value itself is unchanged.
            ExpressionKind::Conversion => {
                let inner = e.conversion_operand().ok_or_else(|| BuildError::Missing {
                    what: "operand of a conversion".into(),
                })?;
                self.handle_value(inner)
            }
            ExpressionKind::NamedValue
            | ExpressionKind::HierarchicalValue
            | ExpressionKind::ElementSelect
            | ExpressionKind::MemberAccess => self.handle_state(e, HANDLE_TY),
            other => Err(unsupported(
                format!("a `{other:?}` class-handle expression"),
                "C17 follow-up",
            )),
        }
    }

    /// Builds the IR for one integral expression (values read are random or
    /// state variables per the module docs).
    pub fn build_expr(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        let out = self.expr(e)?;
        out.validate()?;
        Ok(out)
    }

    fn operand<'d>(e: Expression<'d>, what: &str) -> Result<Expression<'d>, BuildError> {
        e.left().ok_or_else(|| BuildError::Missing {
            what: format!("operand of {what}"),
        })
    }

    fn expr(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        let kind = e.kind();
        if is_handle_type(e.expr_type()) {
            return self.handle_value(e);
        }
        let ty = ty_of(e.expr_type(), &format!("a `{kind:?}` expression"))?;
        // slang folds `rand_var matches p ? t : f` to its false arm (the match
        // of a non-constant subject "fails" at constant-evaluation time), so a
        // conditional with a pattern is never read through its constant value.
        let pattern_cond = kind == ExpressionKind::ConditionalOp
            && e.conditions().iter().any(|c| c.pattern().is_some());
        if !pattern_cond
            && let Some(cv) = e.constant_value()
            && let Some(i) = cv.as_integer()
        {
            return Ok(Expr::Const(ty, svint_to_biguint(i, ty)?));
        }
        match kind {
            ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue => {
                let sym = e.referenced_symbol().ok_or_else(|| BuildError::Missing {
                    what: "symbol of a named value".into(),
                })?;
                if let Some(local) = self.frame_var(sym) {
                    return Ok(local);
                }
                if sym.kind() == SymbolKind::Iterator {
                    self.not_in_function("an iterator variable")?;
                    return self.loop_ref(sym, ty);
                }
                if self.local_of.as_ref().is_some_and(|c| c(e)) {
                    self.not_in_function("a local of an inline constraint's call site")?;
                    return Ok(self.capture_ref(sym, ty));
                }
                self.symbol_ref(sym, ty)
            }
            ExpressionKind::MemberAccess => {
                // A member of an unpacked struct property (LRM 18.4), or of an
                // element of an unpacked array property.
                if let Some(chain) = aggregate::aggregate_chain(e, &self.forced_roots)
                    && !chain.steps.is_empty()
                {
                    return self.aggregate_value(chain, ty);
                }
                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");
                let member = e.member_symbol().ok_or_else(|| BuildError::Missing {
                    what: "member symbol of a member access".into(),
                })?;
                if !is_this {
                    if is_handle_type(base.expr_type()) {
                        // A member read through a handle that is a local of the
                        // call site is one constant of the call (LRM 18.7).
                        if let Some(root) = Self::local_handle_root(base)
                            && self.local_of.as_ref().is_some_and(|c| c(root))
                        {
                            self.not_in_function("a local of an inline constraint's call site")?;
                            let path = Self::handle_path(e)?;
                            let (r, hops) =
                                path.split_first().ok_or_else(|| BuildError::Missing {
                                    what: "handle path of a member read".into(),
                                })?;
                            return Ok(self.capture_path(*r, hops, ty));
                        }
                        // A member read through an object handle (LRM 18.5.12).
                        return self.handle_state(e, ty);
                    }
                    // A packed struct or union is one integral variable (LRM
                    // 18.4): a member read is a window of the whole value.
                    let base_ty = base.expr_type();
                    if !base_ty.is_some_and(|t| t.is_integral() && (t.is_struct() || t.is_union()))
                    {
                        let what = format!("member access `.{}`", member.name());
                        return Err(unsupported(
                            format!(
                                "{what} on a value that is neither a class handle, a packed \
                                 struct or union, nor a member of an unpacked struct property \
                                 of this class"
                            ),
                            "C14",
                        ));
                    }
                    let whole = self.expr(base)?;
                    let low = u32::try_from(member.field_bit_offset()).map_err(|_| {
                        BuildError::Missing {
                            what: format!("bit offset of packed member `{}`", member.name()),
                        }
                    })?;
                    let slice = Expr::Slice(Box::new(whole), low, Ty::unsigned(ty.width));
                    return Ok(if slice.ty() == ty {
                        slice
                    } else {
                        Expr::Resize(Box::new(slice), ty)
                    });
                }
                self.symbol_ref(member, ty)
            }
            ExpressionKind::UnaryOp => {
                let op = e.unary_op().ok_or_else(|| BuildError::Missing {
                    what: "operator of a unary expression".into(),
                })?;
                let a = self.expr(Self::operand(e, "a unary operator")?)?;
                let (uop, rty) = match op {
                    UnaryOp::Plus => return Ok(a),
                    UnaryOp::Minus => (UnOp::Neg, ty),
                    UnaryOp::BitwiseNot => (UnOp::BitNot, ty),
                    UnaryOp::BitwiseAnd => (UnOp::RedAnd, Ty::BIT),
                    UnaryOp::BitwiseOr => (UnOp::RedOr, Ty::BIT),
                    UnaryOp::BitwiseXor => (UnOp::RedXor, Ty::BIT),
                    UnaryOp::BitwiseNand => (UnOp::RedNand, Ty::BIT),
                    UnaryOp::BitwiseNor => (UnOp::RedNor, Ty::BIT),
                    UnaryOp::BitwiseXnor => (UnOp::RedXnor, Ty::BIT),
                    UnaryOp::LogicalNot => (UnOp::LogNot, Ty::BIT),
                    other => {
                        return Err(unsupported(
                            format!("the side-effecting operator {other:?}"),
                            "C2",
                        ));
                    }
                };
                Ok(Expr::Unary(uop, Box::new(a), rty))
            }
            ExpressionKind::BinaryOp => self.binary(e, ty),
            ExpressionKind::ConditionalOp => {
                let mut bound = Vec::new();
                let r = self.conditional(e, ty, &mut bound);
                for uid in bound {
                    self.pattern_binds.remove(&uid);
                }
                r
            }
            ExpressionKind::Conversion => self.conversion(e, ty),
            ExpressionKind::Concatenation => {
                let mut parts = Vec::new();
                let mut w = 0u32;
                for o in e.operands() {
                    let p = self.expr(o)?;
                    w += p.ty().width;
                    parts.push(p);
                }
                Ok(Expr::Concat(parts, Ty::unsigned(w)))
            }
            ExpressionKind::Replication => {
                let n = e
                    .replication_count()
                    .and_then(|c| c.constant_value())
                    .and_then(|c| c.as_i64())
                    .ok_or_else(|| BuildError::Missing {
                        what: "constant count of a replication".into(),
                    })?;
                if n < 1 {
                    return Err(unsupported("a replication with a count below 1", "C2"));
                }
                let inner =
                    self.expr(e.replication_concat().ok_or_else(|| BuildError::Missing {
                        what: "operand of a replication".into(),
                    })?)?;
                let w = inner.ty().width * n as u32;
                Ok(Expr::Concat(vec![inner; n as usize], Ty::unsigned(w)))
            }
            ExpressionKind::Inside => self.inside(e),
            ExpressionKind::ElementSelect => self.element_select(e, ty),
            ExpressionKind::RangeSelect => self.range_select(e, ty),
            ExpressionKind::Call => {
                if e.is_system_call() == Some(true)
                    && self.frame.is_none()
                    && let Some(r) = self.array_call(e, ty)
                {
                    return r;
                }
                let name = e.call_subroutine_name().unwrap_or_default();
                if e.is_system_call() == Some(true) && (name == "$signed" || name == "$unsigned") {
                    let args = e.operands();
                    let [arg] = args.as_slice() else {
                        return Err(BuildError::Missing {
                            what: format!("single argument of {name}"),
                        });
                    };
                    let a = self.expr(*arg)?;
                    return Ok(Expr::Resize(Box::new(a), ty));
                }
                if e.is_system_call() == Some(true)
                    && let Some(r) = self.bit_count_call(e, ty)
                {
                    return r;
                }
                if e.is_system_call() == Some(true) {
                    return Err(unsupported(format!("a call to `{name}`"), "C13"));
                }
                self.user_call(e, ty)
            }
            ExpressionKind::LValueReference => self.lvalue_reference(),
            ExpressionKind::Dist => Err(BuildError::BadDist {
                what: "a `dist` nested inside another expression (it is a constraint item, \
                       never an operand)"
                    .into(),
            }),
            ExpressionKind::UnboundedLiteral => Err(unsupported(
                "an unbounded `$` outside an `inside` range",
                "C2",
            )),
            other => Err(unsupported(format!("a `{other:?}` expression"), "C2")),
        }
    }

    /// `c1 &&& c2 ... ? t : f` (LRM 11.4.11, 12.6): every condition is a
    /// plain boolean or `expr matches pattern`, tested in order; a pattern
    /// variable bound by one is visible to the later conditions and to the
    /// true arm only. The variables bound are appended to `bound` so the
    /// caller can unbind them.
    fn conditional(
        &mut self,
        e: Expression<'_>,
        ty: Ty,
        bound: &mut Vec<SymbolId>,
    ) -> Result<Expr, BuildError> {
        let mut tests = Vec::new();
        for c in e.conditions() {
            let subject = self.expr(c.expr())?;
            tests.push(match c.pattern() {
                None => to_bool(subject),
                Some(p) => self.pattern_test(&p, subject, bound)?,
            });
        }
        let t = self.expr(e.true_value().ok_or_else(|| BuildError::Missing {
            what: "true arm of a conditional".into(),
        })?)?;
        // The false arm sees none of the bindings.
        for uid in bound.drain(..) {
            self.pattern_binds.remove(&uid);
        }
        let f = self.expr(e.false_value().ok_or_else(|| BuildError::Missing {
            what: "false arm of a conditional".into(),
        })?)?;
        Ok(Expr::Ite(
            Box::new(and_all(tests)),
            Box::new(t),
            Box::new(f),
            ty,
        ))
    }

    /// Whether `subject` matches `pat` (LRM 12.6.1), a one-bit test. A
    /// constant pattern is `==` at the common type of the two (the LRM makes
    /// them the same type); `.*` always matches; `.n` always matches and binds
    /// `n` to the subject. Tagged-union and structure patterns need a
    /// subject that is a tagged union or an unpacked struct, neither of which
    /// the solver can take as a random variable, so they fail by name.
    fn pattern_test(
        &mut self,
        pat: &sv_lang::Pattern<'_>,
        subject: Expr,
        bound: &mut Vec<SymbolId>,
    ) -> Result<Expr, BuildError> {
        match pat.kind() {
            PatternKind::Constant => {
                let v = self.expr(pat.value_expr().ok_or_else(|| BuildError::Missing {
                    what: "value of a constant pattern".into(),
                })?)?;
                let (a, b) = (subject.ty(), v.ty());
                let ct = Ty {
                    width: a.width.max(b.width),
                    signed: a.signed && b.signed,
                };
                Ok(bin(BinOp::Eq, coerce(subject, ct), coerce(v, ct), Ty::BIT))
            }
            PatternKind::Wildcard => Ok(Expr::Const(Ty::BIT, BigUint::one())),
            PatternKind::Variable => {
                if let Some(var) = pat.variable()
                    && !var.name().is_empty()
                {
                    let uid = var.uid();
                    self.pattern_binds.insert(uid.clone(), subject);
                    bound.push(uid);
                }
                Ok(Expr::Const(Ty::BIT, BigUint::one()))
            }
            other => Err(unsupported(
                format!(
                    "a {other:?} pattern in a constraint (it matches a tagged union or an \
                     unpacked struct, which is never a random variable)"
                ),
                "C2",
            )),
        }
    }

    fn binary(&mut self, e: Expression<'_>, ty: Ty) -> Result<Expr, BuildError> {
        let op = e.binary_op().ok_or_else(|| BuildError::Missing {
            what: "operator of a binary expression".into(),
        })?;
        let (lhs, rhs) = match (e.left(), e.right()) {
            (Some(l), Some(r)) => (l, r),
            _ => {
                return Err(BuildError::Missing {
                    what: "operands of a binary expression".into(),
                });
            }
        };
        let (bop, rty) = match op {
            BinaryOp::CaseEquality => return Err(BuildError::FourStateOperator { op: "===" }),
            BinaryOp::CaseInequality => return Err(BuildError::FourStateOperator { op: "!==" }),
            BinaryOp::WildcardEquality => return Err(BuildError::FourStateOperator { op: "==?" }),
            BinaryOp::WildcardInequality => {
                return Err(BuildError::FourStateOperator { op: "!=?" });
            }
            BinaryOp::Power => {
                let l = self.expr(lhs)?;
                let r = self.expr(rhs)?;
                return Ok(power(l, r, ty));
            }
            BinaryOp::Add => (BinOp::Add, ty),
            BinaryOp::Subtract => (BinOp::Sub, ty),
            BinaryOp::Multiply => (BinOp::Mul, ty),
            BinaryOp::Divide => (BinOp::Div, ty),
            BinaryOp::Mod => (BinOp::Mod, ty),
            BinaryOp::BinaryAnd => (BinOp::And, ty),
            BinaryOp::BinaryOr => (BinOp::Or, ty),
            BinaryOp::BinaryXor => (BinOp::Xor, ty),
            BinaryOp::BinaryXnor => (BinOp::Xnor, ty),
            BinaryOp::Equality => (BinOp::Eq, Ty::BIT),
            BinaryOp::Inequality => (BinOp::Ne, Ty::BIT),
            BinaryOp::GreaterThanEqual => (BinOp::Ge, Ty::BIT),
            BinaryOp::GreaterThan => (BinOp::Gt, Ty::BIT),
            BinaryOp::LessThanEqual => (BinOp::Le, Ty::BIT),
            BinaryOp::LessThan => (BinOp::Lt, Ty::BIT),
            BinaryOp::LogicalAnd => (BinOp::LogAnd, Ty::BIT),
            BinaryOp::LogicalOr => (BinOp::LogOr, Ty::BIT),
            BinaryOp::LogicalImplication => (BinOp::LogImpl, Ty::BIT),
            BinaryOp::LogicalEquivalence => (BinOp::LogEquiv, Ty::BIT),
            BinaryOp::LogicalShiftLeft | BinaryOp::ArithmeticShiftLeft => (BinOp::Shl, ty),
            BinaryOp::LogicalShiftRight => (BinOp::Shr, ty),
            BinaryOp::ArithmeticShiftRight => (BinOp::Ashr, ty),
        };
        // `a == b` / `a != b` over whole fixed-size unpacked arrays (LRM 11.4.5:
        // equivalent array types compare element by element): both operands'
        // leaves as one bit-stream each, so the comparison is equal exactly
        // when every element pair is (the element types are equivalent, so
        // the streams are laid out alike).
        let whole = |t: Option<Type<'_>>| {
            t.is_some_and(|t| {
                let c = t.canonical();
                c.is_unpacked_array() || c.is_unpacked_struct()
            })
        };
        if matches!(bop, BinOp::Eq | BinOp::Ne) && whole(lhs.expr_type()) && whole(rhs.expr_type())
        {
            let chains = aggregate::aggregate_chain(lhs, &self.forced_roots)
                .zip(aggregate::aggregate_chain(rhs, &self.forced_roots));
            let Some((lc, rc)) = chains else {
                return Err(unsupported(
                    "an array comparison whose operand is not a property (or a member of a \
                     struct property) of this class",
                    "C14",
                ));
            };
            let l = self.aggregate_bitstream(lc)?;
            let r = self.aggregate_bitstream(rc)?;
            return Ok(bin(bop, l, r, rty));
        }
        // `s == t` / `s != t` over strings (LRM 11.4.5, 6.16.6): strings are
        // interned, so equal contents are equal ids; a string is only ever a
        // state variable or a constant in a constraint.
        let is_string =
            |e: Expression<'_>| e.expr_type().is_some_and(|t| t.canonical().is_string());
        if is_string(lhs) || is_string(rhs) {
            if !matches!(bop, BinOp::Eq | BinOp::Ne) {
                return Err(unsupported(
                    format!("the string operator {op:?} (only `==` and `!=` compare strings)"),
                    "C13",
                ));
            }
            let l = self.string_id(lhs)?;
            let r = self.string_id(rhs)?;
            return Ok(bin(bop, l, r, rty));
        }
        let l = self.expr(lhs)?;
        let r = self.expr(rhs)?;
        Ok(bin(bop, l, r, rty))
    }

    /// A string operand of a comparison as its interned id: a constant is
    /// interned now, a string property is a 64-bit state variable (the
    /// property holds the id).
    fn string_id(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        if let Some(cv) = e.constant_value()
            && let Some(s) = cv.as_str()
        {
            let id = crate::strings::intern(s.as_bytes());
            return Ok(Expr::Const(HANDLE_TY, BigUint::from(id)));
        }
        match e.kind() {
            ExpressionKind::Conversion => {
                let inner = e.conversion_operand().ok_or_else(|| BuildError::Missing {
                    what: "operand of a conversion".into(),
                })?;
                self.string_id(inner)
            }
            ExpressionKind::NamedValue
            | ExpressionKind::HierarchicalValue
            | ExpressionKind::MemberAccess => {
                let sym = e.referenced_symbol().or_else(|| e.member_symbol());
                if sym.is_some_and(|s| self.var_ix.contains_key(&s.uid())) {
                    return Err(unsupported("a `rand` string", "C13"));
                }
                self.handle_state(e, HANDLE_TY)
            }
            other => Err(unsupported(
                format!("a `{other:?}` string operand of a comparison"),
                "C13",
            )),
        }
    }

    fn conversion(&mut self, e: Expression<'_>, to: Ty) -> Result<Expr, BuildError> {
        let operand = e.conversion_operand().ok_or_else(|| BuildError::Missing {
            what: "operand of a conversion".into(),
        })?;
        let kind = e.conversion_kind().ok_or_else(|| BuildError::Missing {
            what: "kind of a conversion".into(),
        })?;
        // A bit-stream cast (LRM 6.24.3) of an unpacked struct or fixed-size
        // array property: its leaves concatenated. (A streaming concatenation
        // operand never reaches here: slang rejects one in a constraint.)
        if operand.expr_type().is_some_and(|t| !t.is_integral())
            && let Some(chain) = aggregate::aggregate_chain(operand, &self.forced_roots)
        {
            let x = self.aggregate_bitstream(chain)?;
            return Ok(if x.ty() == to {
                x
            } else {
                Expr::Resize(Box::new(x), to)
            });
        }
        let x = self.expr(operand)?;
        match kind {
            // Propagated: the context's signedness decides the extension.
            1 => Ok(coerce(x, to)),
            // Implicit / Explicit: assignment semantics, the operand's own.
            0 | 3 => Ok(if x.ty() == to {
                x
            } else {
                Expr::Resize(Box::new(x), to)
            }),
            other => Err(unsupported(
                format!("a conversion of kind {other} (streaming or bit-stream cast)"),
                "C2",
            )),
        }
    }

    /// How the value range `item` combines its operands, from its syntax (the
    /// semantic node does not keep the operator).
    fn range_op(&self, item: Expression<'_>) -> Result<RangeOp, BuildError> {
        for tree in self.trees {
            if let Some(node) = item.syntax(tree) {
                let r =
                    ValueRangeExpressionSyntax::cast(node).ok_or_else(|| BuildError::Missing {
                        what: "value-range syntax for a ValueRange expression".into(),
                    })?;
                let op = r.op().ok_or_else(|| BuildError::Missing {
                    what: "operator of a value range".into(),
                })?;
                return match op.text() {
                    ":" => Ok(RangeOp::Span),
                    "+/-" => Ok(RangeOp::Abs),
                    "+%-" => Ok(RangeOp::Pct),
                    other => Err(unsupported(
                        format!("the value-range operator `{other}`"),
                        "C7",
                    )),
                };
            }
        }
        Err(BuildError::Missing {
            what: "syntax node for a value range (is its syntax tree passed to the builder?)"
                .into(),
        })
    }

    /// The inclusive bounds of the value range `item`, for a value of type
    /// `subject`. `[a +/- b]` and `[a +%- b]` are computed in a signed type
    /// wide enough that the arithmetic cannot wrap, and compared there.
    fn value_range(&mut self, item: Expression<'_>, subject: Ty) -> Result<Bounds, BuildError> {
        let (l, r) = match (item.left(), item.right()) {
            (Some(l), Some(r)) => (l, r),
            _ => {
                return Err(BuildError::Missing {
                    what: "bounds of a value range".into(),
                });
            }
        };
        let op = self.range_op(item)?;
        // slang may wrap a `$` in a conversion to the range type.
        let is_unbounded = |b: Expression<'_>| {
            let mut peeled = b;
            while peeled.kind() == ExpressionKind::Conversion {
                match peeled.conversion_operand() {
                    Some(inner) => peeled = inner,
                    None => break,
                }
            }
            peeled.kind() == ExpressionKind::UnboundedLiteral
        };
        if op == RangeOp::Span {
            let mut side = |b: Expression<'_>| -> Result<Option<(Ty, Expr)>, BuildError> {
                if is_unbounded(b) {
                    return Ok(None);
                }
                let bx = self.expr(b)?;
                let t = common_ty(subject, bx.ty());
                Ok(Some((t, coerce(bx, t))))
            };
            let lo = side(l)?;
            let hi = side(r)?;
            return Ok(Bounds { lo, hi });
        }
        if is_unbounded(l) || is_unbounded(r) {
            return Err(BuildError::BadDist {
                what: "`$` as an operand of a `+/-` or `+%-` range".into(),
            });
        }
        let a = self.expr(l)?;
        let b = self.expr(r)?;
        let wide = Ty::signed(2 * subject.width.max(a.ty().width).max(b.ty().width) + 8);
        let (a, b) = (coerce(a, wide), coerce(b, wide));
        let delta = match op {
            RangeOp::Abs => b,
            _ => {
                let hundred = iconst(wide, 100);
                bin(
                    BinOp::Div,
                    bin(BinOp::Mul, a.clone(), b, wide),
                    hundred,
                    wide,
                )
            }
        };
        let lo = bin(BinOp::Sub, a.clone(), delta.clone(), wide);
        let hi = bin(BinOp::Add, a, delta, wide);
        Ok(Bounds {
            lo: Some((wide, lo)),
            hi: Some((wide, hi)),
        })
    }

    /// `x dist { ... }` as a constraint item (LRM 18.5.3; module docs of
    /// [`super::dist`]): registers the [`Dist`] and returns its membership
    /// conjunct over the dist's hidden selector variable.
    fn dist(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        // Inside a `foreach` over a dynamic array or queue the dist is a template
        // that `array::expand` instances once per element (module docs of
        // `super::dist`), so its subject may name the loop variable and elements.
        let runtime = self.in_runtime_loop();
        let saved = if runtime {
            self.no_arrays
        } else {
            self.no_arrays.replace("a `dist` constraint")
        };
        let r = self.dist_item(e, runtime);
        self.no_arrays = saved;
        r
    }

    fn dist_item(&mut self, e: Expression<'_>, runtime: bool) -> Result<Expr, BuildError> {
        let bad = |what: &str| BuildError::BadDist { what: what.into() };
        let left = e.dist_left().ok_or_else(|| BuildError::Missing {
            what: "distributed expression of a `dist`".into(),
        })?;
        // slang converts the distributed expression to the comparison type of
        // the whole `dist`; the weights are over the expression's own values
        // (a `default` covers the values of *its* type), and every comparison
        // below re-converts to its own common type, so the conversion is dropped.
        let mut left = left;
        while left.kind() == ExpressionKind::Conversion {
            match left.conversion_operand() {
                Some(inner) => left = inner,
                None => break,
            }
        }
        let subject = self.expr(left)?;
        let mut vars: Vec<VarId> = Vec::new();
        let mut randc: Option<VarId> = None;
        subject.for_each_var(&mut |v, _| {
            vars.push(v);
            if self.vars[v as usize].randc {
                randc = Some(v);
            }
        });
        vars.sort_unstable();
        vars.dedup();
        if let Some(v) = randc {
            return Err(BuildError::BadDist {
                what: format!(
                    "`randc` variable `{}` in a `dist` (randc variables take no weights)",
                    self.vars[v as usize].name
                ),
            });
        }
        let plain_var = match &subject {
            Expr::Var(v, _) => Some(*v),
            _ => None,
        };
        let sty = subject.ty();
        let state_only = |x: &Expr, what: &str| -> Result<(), BuildError> {
            let mut has_var = false;
            x.for_each_var(&mut |_, _| has_var = true);
            if has_var {
                return Err(BuildError::BadDist {
                    what: format!(
                        "a random variable in {what}; weights and bounds are fixed values"
                    ),
                });
            }
            Ok(())
        };
        let weight_of = |this: &mut Self,
                         w: Option<sv_lang::DistWeight<'_>>|
         -> Result<(Expr, bool), BuildError> {
            match w {
                // LRM 18.5.3: an item without a weight is `:= 1`.
                None => Ok((Expr::constant(Ty::unsigned(32), 1u32), false)),
                Some(w) => {
                    let x = this.expr(w.expr)?;
                    state_only(&x, "a `dist` weight")?;
                    Ok((x, w.kind == DistWeightKind::PerRange))
                }
            }
        };
        let mut items = Vec::new();
        for it in e.dist_items() {
            let v = it.value();
            let (member, ty, span) = if v.kind() == ExpressionKind::ValueRange {
                let b = self.value_range(v, sty)?;
                // Bounds of different types are each compared in their own
                // common type; `Dist::weights` reads the types off the bounds.
                let ty = match (&b.lo, &b.hi) {
                    (Some((t, _)), _) | (_, Some((t, _))) => *t,
                    (None, None) => sty,
                };
                let mut conj = Vec::new();
                for (bound, cmp) in [(&b.lo, BinOp::Ge), (&b.hi, BinOp::Le)] {
                    if let Some((t, x)) = bound {
                        state_only(x, "a `dist` range bound")?;
                        conj.push(bin(cmp, coerce(subject.clone(), *t), x.clone(), Ty::BIT));
                    }
                }
                (
                    and_all(conj),
                    ty,
                    Span::Range {
                        lo: b.lo.map(|(_, x)| x),
                        hi: b.hi.map(|(_, x)| x),
                    },
                )
            } else {
                let x = self.expr(v)?;
                state_only(&x, "a `dist` value")?;
                let t = common_ty(sty, x.ty());
                let x = coerce(x, t);
                let m = bin(BinOp::Eq, coerce(subject.clone(), t), x.clone(), Ty::BIT);
                (m, t, Span::Point(x))
            };
            let (w, per_range) = weight_of(self, it.weight())?;
            items.push(Item {
                member,
                ty,
                span,
                weight: w,
                per_range,
            });
        }
        let default = match e.dist_default_weight() {
            Some(w) => {
                let (weight, per_range) = weight_of(self, Some(w))?;
                Some(DefaultWeight { weight, per_range })
            }
            None => None,
        };
        if items.is_empty() && default.is_none() {
            return Err(bad("a `dist` with no items"));
        }
        let d = Dist {
            subject_ty: sty,
            plain_var,
            vars,
            items,
            default,
            subject: runtime.then_some(subject),
        };
        let sel = SELECTOR_BASE + self.dists.len() as u32;
        let conjunct = d.conjunct(sel);
        self.dists.push(d);
        Ok(conjunct)
    }

    fn inside(&mut self, e: Expression<'_>) -> Result<Expr, BuildError> {
        let left = self.expr(e.inside_left().ok_or_else(|| BuildError::Missing {
            what: "left operand of `inside`".into(),
        })?)?;
        let items = e.inside_range_list();
        if items.is_empty() {
            return Err(BuildError::Missing {
                what: "candidates of `inside`".into(),
            });
        }
        // LRM 11.4.13 / 18.3: the set is a plain disjunction of equality and
        // range tests, so every member is one value-region of the BDD and the
        // solver picks uniformly over the satisfying *values*; unlike `dist`
        // (18.5.3) no member carries a weight.
        let mut acc: Option<Expr> = None;
        for item in items {
            let term = if item.kind() == ExpressionKind::ValueRange {
                // `[a:b]`, `[a +/- b]` and `[a +%- b]` (11.4.13); a bound is
                // compared in the common type of it and the tested value.
                let b = self.value_range(item, left.ty())?;
                let mut conj: Vec<Expr> = Vec::new();
                for (bound, cmp) in [(b.lo, BinOp::Ge), (b.hi, BinOp::Le)] {
                    if let Some((t, x)) = bound {
                        conj.push(bin(cmp, coerce(left.clone(), t), x, Ty::BIT));
                    }
                }
                and_all(conj)
            } else if item
                .expr_type()
                .is_some_and(|t| arrays::array_shape(t).is_some())
            {
                self.inside_array(&left, item)?
            } else {
                let ix = self.expr(item)?;
                let t = common_ty(left.ty(), ix.ty());
                bin(BinOp::Eq, coerce(left.clone(), t), coerce(ix, t), Ty::BIT)
            };
            acc = Some(match acc {
                None => term,
                Some(prev) => bin(BinOp::LogOr, prev, term, Ty::BIT),
            });
        }
        Ok(acc.expect("candidates non-empty, checked above"))
    }

    /// The selected value's expression and geometry, shared by both selects.
    fn select_base(&mut self, e: Expression<'_>) -> Result<(Expr, Geom), BuildError> {
        let base = e.select_value().ok_or_else(|| BuildError::Missing {
            what: "base of a select".into(),
        })?;
        let bt = base.expr_type().ok_or_else(|| BuildError::Missing {
            what: "type of a select base".into(),
        })?;
        let bx = self.expr(base)?;
        let geom = Geom::of(bt, bx.ty().width, "a select base")?;
        Ok((bx, geom))
    }

    /// Widens a dynamic index so offset arithmetic cannot wrap, as a signed
    /// value (an unsigned index zero-extends).
    fn wide_index(&mut self, idx: Expression<'_>) -> Result<(Expr, Ty), BuildError> {
        let ix = self.expr(idx)?;
        let wide = Ty::signed(ix.ty().width.max(32) + 2);
        Ok((Expr::Resize(Box::new(ix), wide), wide))
    }

    /// `base >> (pos * ew)` truncated to `ty`: the dynamic-window gadget.
    fn dyn_window(base: Expr, pos: Expr, wide: Ty, ew: u32, out_width: u32, ty: Ty) -> Expr {
        let off = if ew > 1 {
            bin(BinOp::Mul, pos, iconst(wide, i64::from(ew)), wide)
        } else {
            pos
        };
        let bty = base.ty();
        let shifted = bin(BinOp::Shr, base, off, bty);
        Expr::Resize(
            Box::new(Expr::Resize(Box::new(shifted), Ty::unsigned(out_width))),
            ty,
        )
    }

    fn static_window(
        base: Expr,
        geom: &Geom,
        lo_idx: i64,
        hi_idx: i64,
        what: &str,
        ty: Ty,
    ) -> Result<Expr, BuildError> {
        let (pl, ph) = (geom.pos(lo_idx), geom.pos(hi_idx));
        let (low, high) = (pl.min(ph), pl.max(ph));
        if low < 0 || high >= geom.elems() {
            return Err(BuildError::OutOfRangeSelect {
                what: format!(
                    "{what}[{lo_idx}..{hi_idx}] outside [{}:{}]",
                    geom.left, geom.right
                ),
            });
        }
        let width = (high - low + 1) as u32 * geom.ew;
        let slice = Expr::Slice(Box::new(base), low as u32 * geom.ew, Ty::unsigned(width));
        Ok(if slice.ty() == ty {
            slice
        } else {
            Expr::Resize(Box::new(slice), ty)
        })
    }

    fn element_select(&mut self, e: Expression<'_>, ty: Ty) -> Result<Expr, BuildError> {
        // An element of a fixed-size unpacked array property (LRM 18.4).
        if let Some(chain) = aggregate::aggregate_chain(e, &self.forced_roots)
            && !chain.steps.is_empty()
        {
            return self.aggregate_value(chain, ty);
        }
        if let Some(arr) = e.select_value()
            && arr
                .expr_type()
                .is_some_and(|t| arrays::array_shape(t).is_some())
        {
            self.not_in_function("an array element")?;
            return self.array_element(e, arr, ty);
        }
        let (base, geom) = self.select_base(e)?;
        let sel = e.selector().ok_or_else(|| BuildError::Missing {
            what: "index of an element select".into(),
        })?;
        if let Some(i) = sel.constant_value().and_then(|c| c.as_i64()) {
            return Self::static_window(base, &geom, i, i, "element select", ty);
        }
        let (idx, wide) = self.wide_index(sel)?;
        let pos = if geom.descending() {
            bin(BinOp::Sub, idx, iconst(wide, geom.right), wide)
        } else {
            bin(BinOp::Sub, iconst(wide, geom.right), idx, wide)
        };
        Ok(Self::dyn_window(base, pos, wide, geom.ew, ty.width, ty))
    }

    fn range_select(&mut self, e: Expression<'_>, ty: Ty) -> Result<Expr, BuildError> {
        let (base, geom) = self.select_base(e)?;
        let kind = e
            .range_selection_kind()
            .ok_or_else(|| BuildError::Missing {
                what: "kind of a range select".into(),
            })?;
        let (l, r) = match (e.range_left(), e.range_right()) {
            (Some(l), Some(r)) => (l, r),
            _ => {
                return Err(BuildError::Missing {
                    what: "bounds of a range select".into(),
                });
            }
        };
        let const_of = |x: Expression<'_>| x.constant_value().and_then(|c| c.as_i64());
        if kind == 0 {
            let (Some(a), Some(b)) = (const_of(l), const_of(r)) else {
                return Err(BuildError::Missing {
                    what: "constant bounds of a `[l:r]` select".into(),
                });
            };
            return Self::static_window(base, &geom, a.min(b), a.max(b), "range select", ty);
        }
        let w = const_of(r)
            .filter(|w| *w >= 1)
            .ok_or_else(|| BuildError::Missing {
                what: "constant width of an indexed part select".into(),
            })?;
        // Lowest and highest declared index relative to the base index.
        let (dlo, dhi) = if kind == 1 { (0, w - 1) } else { (-(w - 1), 0) };
        if let Some(b) = const_of(l) {
            return Self::static_window(base, &geom, b + dlo, b + dhi, "part select", ty);
        }
        let (idx, wide) = self.wide_index(l)?;
        let pos = if geom.descending() {
            bin(BinOp::Add, idx, iconst(wide, dlo - geom.right), wide)
        } else {
            bin(BinOp::Sub, iconst(wide, geom.right - dhi), idx, wide)
        };
        Ok(Self::dyn_window(base, pos, wide, geom.ew, ty.width, ty))
    }
}