vj-sim 0.3.0

//! Real-valued constraints for the [`Builder`] (plan task C9; IEEE 1800-2023
//! 18.5.3 and 18.5.13).
//!
//! `real`/`shortreal`/`realtime` random variables live in their own namespace
//! ([`RealVarInfo`], numbered separately from the integral [`VarInfo`]s) and
//! their constraints become a [`RealProblem`] that [`super::super::real_domain`]
//! solves after the integral variables. A constraint item is wholly real or
//! wholly integral: the integral solver is a bit-vector solver and the real
//! one works on the floating-point grid, and nothing here couples the two.
//!
//! * An expression constraint that reads a real value becomes a [`RealCond`].
//!   An implication or `if` constraint whose predicate or body reads a real
//!   value is built whole as a [`RealCond::Guard`] (18.5.12), so its predicate
//!   keeps the Figure 18-3 evaluation.
//! * `real_var dist { ... }` becomes a [`RealDist`]; the variable must be named
//!   plainly, a range needs `:/` (18.5.3: `:=` on a real range would give each
//!   of infinitely many values the same weight), and one variable has at most
//!   one `dist`.
//! * A real constraint may read an *integral random variable* (`x < a` with a
//!   `rand int a`, or a guard `if (a > 3)`): the integral variables are solved
//!   first, then the real problem is solved with each integral value fixed, as
//!   a state. When that real problem has no solution the integral part is
//!   redrawn (the registry's `solve_expanded`), and the call fails as
//!   unsatisfiable only after many redraws. A real value inside an *integral*
//!   comparison (`a == int'(x)`) stays refused: the integral solver cannot
//!   read a real random value.
//! * `solve a before b` between two real variables orders them; between a real
//!   and an integral variable it has nothing to order (the integral variables
//!   are always solved first) and is ignored (18.5.9: ordering never changes
//!   the solution space).
//! * What the real solver can handle is checked at build time by
//!   [`RealProblem::check`]: every atom affine in one variable, and a guard that
//!   couples two variables needs `solve` ordering them (see the solver's docs).

use super::*;
use crate::constraints::real_domain::{
    CmpOp, FloatKind as Fk, Real, RealCond, RealDist, RealDistItem, RealExpr, RealProblem, RealSpan,
};

/// An active `real`/`shortreal` random variable.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct RealVarInfo {
    /// The declaring symbol's key.
    pub symbol: SymbolId,
    /// Its declared name.
    pub name: String,
    /// `real` (also `realtime`) or `shortreal`.
    pub kind: Fk,
    /// For a leaf of an aggregate property ([`Builder::declare_rand_aggregate`]),
    /// where it sits in the property [`Self::symbol`] names; `None` for a
    /// property itself.
    pub window: Option<Window>,
}

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

/// The grid type of the floating type `t`, `None` for any other type.
pub(super) fn real_kind(t: Option<Type<'_>>) -> Option<Fk> {
    let t = t?;
    if !t.is_floating() {
        return None;
    }
    Some(match t.canonical().floating_kind() {
        sv_lang::FloatKind::ShortReal => Fk::F32,
        sv_lang::FloatKind::Real | sv_lang::FloatKind::RealTime => Fk::F64,
    })
}

/// The type a real state variable is read as: its IEEE bit pattern.
pub(super) fn state_ty(k: Fk) -> Ty {
    Ty::unsigned(k.width())
}

fn constraint_kids<'d>(c: Constraint<'d>) -> Vec<Constraint<'d>> {
    c.children()
        .into_iter()
        .filter_map(|n| n.as_constraint())
        .collect()
}

/// `e` with the conversions slang wrapped around it removed.
pub(super) fn strip_conversions(mut e: Expression<'_>) -> Expression<'_> {
    while e.kind() == ExpressionKind::Conversion {
        match e.conversion_operand() {
            Some(inner) => e = inner,
            None => break,
        }
    }
    e
}

/// Whether `e` is, or contains, a value of floating type.
pub(super) fn reads_real(e: Expression<'_>) -> bool {
    if real_kind(e.expr_type()).is_some() {
        return true;
    }
    let mut kids: Vec<Expression<'_>> = Vec::new();
    kids.extend(e.left());
    kids.extend(e.right());
    kids.extend(e.conversion_operand());
    kids.extend(e.true_value());
    kids.extend(e.false_value());
    kids.extend(e.inside_left());
    kids.extend(e.inside_range_list());
    kids.extend(e.dist_left());
    kids.extend(e.operands());
    kids.extend(e.conditions().into_iter().map(|c| c.expr()));
    kids.into_iter().any(reads_real)
}

/// Whether a constraint item reads a real value anywhere that matters to the
/// namespace it belongs to (its expression, or a guard's predicate or body).
pub(super) fn constraint_reads_real(c: Constraint<'_>) -> bool {
    match c.kind() {
        ConstraintKind::Expression => c.expr().is_some_and(reads_real),
        ConstraintKind::List => constraint_kids(c).into_iter().any(constraint_reads_real),
        ConstraintKind::Implication | ConstraintKind::Conditional => {
            c.predicate().is_some_and(reads_real)
                || constraint_kids(c).into_iter().any(constraint_reads_real)
        }
        // Items that never carry a real value into a solved conjunct: ordering and
        // soft-disable directives name variables only, `foreach` bodies are
        // C14's, and `unique` rejects real members by name in its own handler.
        ConstraintKind::Uniqueness
        | ConstraintKind::SolveBefore
        | ConstraintKind::Foreach
        | ConstraintKind::DisableSoft
        | ConstraintKind::Invalid => false,
        // `ConstraintKind` is `#[non_exhaustive]`: a kind added by a frontend
        // upgrade must be classified here, never silently routed to a namespace.
        other => panic!("constraint kind {other:?} has no real/integral classification"),
    }
}

/// Whether the `dist` expression `e` distributes a real value.
pub(super) fn dist_is_real(e: Expression<'_>) -> bool {
    e.dist_left()
        .is_some_and(|l| real_kind(strip_conversions(l).expr_type()).is_some())
}

/// Whether `b` is the unbounded `$` (slang may wrap it in a conversion).
fn is_unbounded(b: Expression<'_>) -> bool {
    strip_conversions(b).kind() == ExpressionKind::UnboundedLiteral
}

fn cmp_of(op: BinaryOp) -> Option<CmpOp> {
    Some(match op {
        BinaryOp::LessThan => CmpOp::Lt,
        BinaryOp::LessThanEqual => CmpOp::Le,
        BinaryOp::GreaterThan => CmpOp::Gt,
        BinaryOp::GreaterThanEqual => CmpOp::Ge,
        BinaryOp::Equality => CmpOp::Eq,
        BinaryOp::Inequality => CmpOp::Ne,
        _ => return None,
    })
}

impl Builder<'_> {
    /// Registers `sym` (a `rand` `real`/`shortreal`/`realtime` property) as an
    /// active real random variable and returns its id in the real namespace
    /// (idempotent). `randc` is for integral types only (LRM 18.4.2).
    pub fn declare_rand_real(&mut self, sym: Symbol<'_>) -> Result<u32, BuildError> {
        let uid = sym.uid();
        if let Some(&id) = self.real_var_ix.get(&uid) {
            return Ok(id);
        }
        let name = sym.name().to_string();
        match sym.rand_mode() {
            RandMode::None => return Err(BuildError::NotRand { name }),
            RandMode::RandC => {
                return Err(bad(format!(
                    "`randc` variable `{name}` is real; `randc` is for integral types only \
                     (IEEE 1800-2023 18.4.2)"
                )));
            }
            RandMode::Rand => {}
        }
        let kind = real_kind(sym.value_type()).ok_or_else(|| BuildError::Missing {
            what: format!("floating type for `{name}`"),
        })?;
        let id = self.real_vars.len() as u32;
        self.real_vars.push(RealVarInfo {
            symbol: uid.clone(),
            name,
            kind,
            window: None,
        });
        self.real_var_ix.insert(uid, id);
        Ok(id)
    }

    /// Registers `sym` as a real random variable whether or not it is declared
    /// `rand` (LRM 18.11: an argument of `randomize(v)` or `std::randomize(v)`
    /// is random for that call). Idempotent; `randc` does not apply to a real.
    pub fn declare_real_forced(&mut self, sym: Symbol<'_>) -> Result<u32, BuildError> {
        let uid = sym.uid();
        if let Some(&id) = self.real_var_ix.get(&uid) {
            return Ok(id);
        }
        let name = sym.name().to_string();
        let kind = real_kind(sym.value_type()).ok_or_else(|| BuildError::Missing {
            what: format!("floating type for `{name}`"),
        })?;
        let id = self.real_vars.len() as u32;
        self.real_vars.push(RealVarInfo {
            symbol: uid.clone(),
            name,
            kind,
            window: None,
        });
        self.real_var_ix.insert(uid, id);
        Ok(id)
    }

    /// The real problem and variable table, validated; `finish`'s real half.
    pub(super) fn finish_real(&mut self) -> Result<(Vec<RealVarInfo>, RealProblem), BuildError> {
        let problem = RealProblem {
            kinds: self.real_vars.iter().map(|v| v.kind).collect(),
            conds: std::mem::take(&mut self.real_conds),
            dists: std::mem::take(&mut self.real_dists),
            before: std::mem::take(&mut self.real_before),
        };
        problem.validate_ir()?;
        if problem.has_integral_only_filter() {
            return Err(bad(
                "a real expression constrains an integral random variable without a real \
                 random variable to solve for; the integral solve cannot satisfy it \
                 reliably, so bound the variable with an integral expression (`x < int'(f)`)",
            ));
        }
        order::levels(problem.kinds.len(), &problem.before)?;
        problem.check().map_err(|why| {
            let legend: Vec<String> = self
                .real_vars
                .iter()
                .enumerate()
                .map(|(i, v)| format!("#{i} = `{}`", v.name))
                .collect();
            bad(format!("{why} (real variables: {})", legend.join(", ")))
        })?;
        Ok((std::mem::take(&mut self.real_vars), problem))
    }

    /// A state variable holding the bits of a real, as a [`RealExpr`].
    pub(super) fn real_state(&mut self, state: Expr, kind: Fk) -> Result<RealExpr, BuildError> {
        match state {
            Expr::State(id, _) => Ok(RealExpr::State(id, kind)),
            _ => Err(BuildError::Missing {
                what: "state variable for a real read".into(),
            }),
        }
    }

    /// A real-valued expression: random variables, state variables, constants,
    /// `+ - * /`, negation and the conversions between the floating types and
    /// from variable-free integral expressions.
    pub(super) fn real_expr(&mut self, e: Expression<'_>) -> Result<RealExpr, BuildError> {
        let Some(kind) = real_kind(e.expr_type()) else {
            // An integral value where a real one is wanted: a `dist` may mix
            // them (18.5.3), and slang leaves such an item unconverted.
            let i = self.expr(e)?;
            Self::reject_calls(&i)?;
            return Ok(RealExpr::FromInt(Box::new(i)));
        };
        if let Some(f) = e.constant_value().and_then(|c| c.as_f64()) {
            return Ok(RealExpr::Const(Real::new(kind.round(f)), kind));
        }
        match e.kind() {
            ExpressionKind::NamedValue | ExpressionKind::HierarchicalValue => {
                let sym = e.referenced_symbol().ok_or_else(|| BuildError::Missing {
                    what: "symbol of a named value".into(),
                })?;
                if !self.real_var_ix.contains_key(&sym.uid()) && self.is_call_local(e) {
                    // a real local of an inline constraint's call site (LRM 18.7),
                    // captured as its stored bits when the call is made
                    self.not_in_function("a local of an inline constraint's call site")?;
                    let st = self.capture_ref(sym, state_ty(kind));
                    return self.real_state(st, kind);
                }
                self.real_symbol(sym, kind)
            }
            ExpressionKind::ElementSelect => {
                match aggregate::aggregate_chain(e, &self.forced_roots) {
                    Some(chain) if !chain.steps.is_empty() => self.real_aggregate(chain, kind),
                    _ => Err(bad(
                        "an element select that is not of an unpacked array property of this class \
                     as a real value",
                    )),
                }
            }
            ExpressionKind::MemberAccess => {
                if let Some(chain) = aggregate::aggregate_chain(e, &self.forced_roots)
                    && !chain.steps.is_empty()
                {
                    return self.real_aggregate(chain, kind);
                }
                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 {
                    return self.real_symbol(member, kind);
                }
                if is_handle_type(base.expr_type()) {
                    // A real member read through an object handle (18.5.12).
                    let st = self.handle_state(e, state_ty(kind))?;
                    return self.real_state(st, kind);
                }
                Err(bad(format!(
                    "member access `.{}` on a value that is not an object handle",
                    member.name()
                )))
            }
            ExpressionKind::UnaryOp => {
                let op = e.unary_op().ok_or_else(|| BuildError::Missing {
                    what: "operator of a unary expression".into(),
                })?;
                let a = self.real_expr(Self::operand(e, "a unary operator")?)?;
                match op {
                    UnaryOp::Plus => Ok(a),
                    UnaryOp::Minus => Ok(RealExpr::Neg(Box::new(a))),
                    other => Err(bad(format!("the real unary operator {other:?}"))),
                }
            }
            ExpressionKind::BinaryOp => {
                let op = e.binary_op().ok_or_else(|| BuildError::Missing {
                    what: "operator of a binary expression".into(),
                })?;
                let (Some(l), Some(r)) = (e.left(), e.right()) else {
                    return Err(BuildError::Missing {
                        what: "operands of a binary expression".into(),
                    });
                };
                let make: fn(Box<RealExpr>, Box<RealExpr>) -> RealExpr = match op {
                    BinaryOp::Add => RealExpr::Add,
                    BinaryOp::Subtract => RealExpr::Sub,
                    BinaryOp::Multiply => RealExpr::Mul,
                    BinaryOp::Divide => RealExpr::Div,
                    other => {
                        return Err(bad(format!(
                            "the real operator {other:?} (only `+ - * /` build a real value)"
                        )));
                    }
                };
                let l = self.real_expr(l)?;
                let r = self.real_expr(r)?;
                Ok(make(Box::new(l), Box::new(r)))
            }
            ExpressionKind::Conversion => self.real_conversion(e, kind),
            other => Err(bad(format!("a `{other:?}` expression as a real value"))),
        }
    }

    fn real_symbol(&mut self, sym: Symbol<'_>, kind: Fk) -> Result<RealExpr, BuildError> {
        if let Some(&id) = self.real_var_ix.get(&sym.uid()) {
            return Ok(RealExpr::Var(id));
        }
        let st = self.state_ref(sym, &[], 0, state_ty(kind))?;
        self.real_state(st, kind)
    }

    fn real_conversion(&mut self, e: Expression<'_>, to: Fk) -> Result<RealExpr, BuildError> {
        let operand = e.conversion_operand().ok_or_else(|| BuildError::Missing {
            what: "operand of a conversion".into(),
        })?;
        let ck = e.conversion_kind().ok_or_else(|| BuildError::Missing {
            what: "kind of a conversion".into(),
        })?;
        if !matches!(ck, 0 | 1 | 3) {
            return Err(bad(format!(
                "a conversion of kind {ck} in a real expression"
            )));
        }
        match real_kind(operand.expr_type()) {
            Some(from) => {
                let x = self.real_expr(operand)?;
                Ok(if from == Fk::F64 && to == Fk::F32 {
                    RealExpr::ToShort(Box::new(x))
                } else {
                    x
                })
            }
            None => {
                let i = self.expr(operand)?;
                Self::reject_calls(&i)?;
                let x = RealExpr::FromInt(Box::new(i));
                Ok(if to == Fk::F32 {
                    RealExpr::ToShort(Box::new(x))
                } else {
                    x
                })
            }
        }
    }

    /// The bounds of the real value range `item` (`None` for `$`): `[a:b]`,
    /// `[a +/- b]` = `[a-b : a+b]` and `[a +%- b]` = `[a-a*b/100 : a+a*b/100]`
    /// (LRM 11.4.13).
    fn real_bounds(
        &mut self,
        item: Expression<'_>,
    ) -> Result<(Option<RealExpr>, Option<RealExpr>), BuildError> {
        let (Some(l), Some(r)) = (item.left(), item.right()) else {
            return Err(BuildError::Missing {
                what: "bounds of a value range".into(),
            });
        };
        let op = self.range_op(item)?;
        if op == RangeOp::Span {
            let mut side = |b: Expression<'_>| -> Result<Option<RealExpr>, BuildError> {
                if is_unbounded(b) {
                    return Ok(None);
                }
                Ok(Some(self.real_expr(b)?))
            };
            let lo = side(l)?;
            let hi = side(r)?;
            return Ok((lo, hi));
        }
        if is_unbounded(l) || is_unbounded(r) {
            return Err(BuildError::BadDist {
                what: "`$` as an operand of a `+/-` or `+%-` range".into(),
            });
        }
        let kind = real_kind(l.expr_type()).unwrap_or(Fk::F64);
        let a = self.real_expr(l)?;
        let b = self.real_expr(r)?;
        let delta = match op {
            RangeOp::Abs => b,
            _ => RealExpr::Div(
                Box::new(RealExpr::Mul(Box::new(a.clone()), Box::new(b))),
                Box::new(RealExpr::Const(Real::new(100.0), kind)),
            ),
        };
        let lo = RealExpr::Sub(Box::new(a.clone()), Box::new(delta.clone()));
        let hi = RealExpr::Add(Box::new(a), Box::new(delta));
        Ok((Some(lo), Some(hi)))
    }

    /// A boolean condition that reads a real value (or, nested in one, an
    /// integral state expression).
    pub(super) fn real_cond(&mut self, e: Expression<'_>) -> Result<RealCond, BuildError> {
        if let Some(cv) = e.constant_value()
            && let Some(i) = cv.as_integer()
        {
            let ty = ty_of(e.expr_type(), "a constant condition")?;
            return Ok(RealCond::Const(!svint_to_biguint(i, ty)?.is_zero()));
        }
        if !reads_real(e) {
            let x = to_bool(self.expr(e)?);
            Self::reject_calls(&x)?;
            return Ok(RealCond::Int(x));
        }
        match e.kind() {
            ExpressionKind::BinaryOp => {
                let op = e.binary_op().ok_or_else(|| BuildError::Missing {
                    what: "operator of a binary expression".into(),
                })?;
                let (Some(l), Some(r)) = (e.left(), e.right()) else {
                    return Err(BuildError::Missing {
                        what: "operands of a binary expression".into(),
                    });
                };
                if let Some(cmp) = cmp_of(op) {
                    if real_kind(l.expr_type()).is_none() && real_kind(r.expr_type()).is_none() {
                        return Err(bad(
                            "an integral comparison over a value converted from a real (such as \
                             `int'(x)`); compare the real value itself",
                        ));
                    }
                    let l = self.real_expr(l)?;
                    let r = self.real_expr(r)?;
                    return Ok(RealCond::Cmp(cmp, l, r));
                }
                match op {
                    BinaryOp::LogicalAnd => {
                        Ok(RealCond::And(vec![self.real_cond(l)?, self.real_cond(r)?]))
                    }
                    BinaryOp::LogicalOr => {
                        Ok(RealCond::Or(vec![self.real_cond(l)?, self.real_cond(r)?]))
                    }
                    BinaryOp::LogicalImplication => Ok(RealCond::Or(vec![
                        RealCond::Not(Box::new(self.real_cond(l)?)),
                        self.real_cond(r)?,
                    ])),
                    BinaryOp::LogicalEquivalence => {
                        let (a, b) = (self.real_cond(l)?, self.real_cond(r)?);
                        Ok(RealCond::Or(vec![
                            RealCond::And(vec![a.clone(), b.clone()]),
                            RealCond::And(vec![
                                RealCond::Not(Box::new(a)),
                                RealCond::Not(Box::new(b)),
                            ]),
                        ]))
                    }
                    BinaryOp::CaseEquality => Err(BuildError::FourStateOperator { op: "===" }),
                    BinaryOp::CaseInequality => Err(BuildError::FourStateOperator { op: "!==" }),
                    BinaryOp::WildcardEquality => Err(BuildError::FourStateOperator { op: "==?" }),
                    BinaryOp::WildcardInequality => {
                        Err(BuildError::FourStateOperator { op: "!=?" })
                    }
                    other => Err(bad(format!("the operator {other:?} on real operands"))),
                }
            }
            ExpressionKind::UnaryOp if e.unary_op() == Some(UnaryOp::LogicalNot) => Ok(
                RealCond::Not(Box::new(self.real_cond(Self::operand(e, "`!`")?)?)),
            ),
            ExpressionKind::Conversion => {
                let inner = e.conversion_operand().ok_or_else(|| BuildError::Missing {
                    what: "operand of a conversion".into(),
                })?;
                if real_kind(inner.expr_type()).is_some() {
                    return Err(bad(
                        "a real value used as a condition (compare it with `==`, `<`, ... instead)",
                    ));
                }
                self.real_cond(inner)
            }
            ExpressionKind::Inside => self.real_inside(e),
            other => Err(bad(format!(
                "a `{other:?}` expression as a real constraint"
            ))),
        }
    }

    /// `x inside { ... }` over a real value: a disjunction of equality and
    /// range tests (11.4.13).
    fn real_inside(&mut self, e: Expression<'_>) -> Result<RealCond, BuildError> {
        let subject = self.real_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(),
            });
        }
        let mut terms = Vec::new();
        for item in items {
            if item.kind() == ExpressionKind::ValueRange {
                let (lo, hi) = self.real_bounds(item)?;
                let mut both = Vec::new();
                if let Some(lo) = lo {
                    both.push(RealCond::Cmp(CmpOp::Ge, subject.clone(), lo));
                }
                if let Some(hi) = hi {
                    both.push(RealCond::Cmp(CmpOp::Le, subject.clone(), hi));
                }
                terms.push(RealCond::And(both));
            } else {
                let v = self.real_expr(item)?;
                terms.push(RealCond::Cmp(CmpOp::Eq, subject.clone(), v));
            }
        }
        Ok(RealCond::Or(terms))
    }

    /// A constraint item built wholly over the real namespace (the body of a
    /// guard that reads a real value).
    pub(super) fn real_constraint(&mut self, c: Constraint<'_>) -> Result<RealCond, BuildError> {
        match c.kind() {
            ConstraintKind::List => {
                let mut parts = Vec::new();
                for k in constraint_kids(c) {
                    parts.push(self.real_constraint(k)?);
                }
                Ok(RealCond::And(parts))
            }
            ConstraintKind::Expression => {
                if self.is_soft(c)? {
                    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 e = c.expr().ok_or_else(|| BuildError::Missing {
                    what: "expression of an expression constraint".into(),
                })?;
                if e.kind() == ExpressionKind::Dist {
                    return Err(BuildError::BadDist {
                        what: "a `dist` inside a guard that reads a real value is not \
                               supported; state it outside the guard"
                            .into(),
                    });
                }
                self.real_cond(e)
            }
            ConstraintKind::Implication | ConstraintKind::Conditional => {
                let p = c.predicate().ok_or_else(|| BuildError::Missing {
                    what: "predicate of a guard".into(),
                })?;
                let pred = self.real_cond(p)?;
                let arms = constraint_kids(c);
                let implication = c.kind() == ConstraintKind::Implication;
                let max = if implication { 1 } else { 2 };
                if arms.is_empty() || arms.len() > max {
                    return Err(BuildError::Missing {
                        what: format!("one or two arms of a guard (got {})", arms.len()),
                    });
                }
                let then_c = if implication {
                    let mut body = Vec::new();
                    for k in &arms {
                        body.push(self.real_constraint(*k)?);
                    }
                    RealCond::And(body)
                } else {
                    self.real_constraint(arms[0])?
                };
                let else_c = match arms.get(1) {
                    Some(a) if !implication => self.real_constraint(*a)?,
                    _ => RealCond::Const(true),
                };
                Ok(RealCond::Guard(
                    Box::new(pred),
                    Box::new(then_c),
                    Box::new(else_c),
                ))
            }
            ConstraintKind::Uniqueness => Err(bad("a `unique` constraint inside a real guard")),
            ConstraintKind::SolveBefore => Err(bad("`solve ... before` inside a guard")),
            other => Err(bad(format!("a {other:?} constraint inside a real guard"))),
        }
    }

    /// The integral weight expression of a real `dist` item; it must not read
    /// a random variable.
    fn real_weight(&mut self, w: Expression<'_>) -> Result<Expr, BuildError> {
        let x = self.expr(w)?;
        Self::reject_calls(&x)?;
        if has_var(&x) {
            return Err(BuildError::BadDist {
                what: "a random variable in a `dist` weight; weights are fixed values".into(),
            });
        }
        Ok(x)
    }

    /// A bound or value of a real `dist` item; it must not read a random
    /// variable.
    fn real_fixed(&mut self, e: Expression<'_>, what: &str) -> Result<RealExpr, BuildError> {
        let x = self.real_expr(e)?;
        let mut any = false;
        x.for_each_var(&mut |_| any = true);
        if any {
            return Err(BuildError::BadDist {
                what: format!("a random variable in {what}; weights and bounds are fixed values"),
            });
        }
        Ok(x)
    }

    /// `real_var dist { ... }` (18.5.3) as a [`RealDist`].
    pub(super) fn real_dist(&mut self, e: Expression<'_>) -> Result<(), BuildError> {
        let bad_dist = |what: &str| BuildError::BadDist { what: what.into() };
        let left = e.dist_left().ok_or_else(|| BuildError::Missing {
            what: "distributed expression of a `dist`".into(),
        })?;
        let RealExpr::Var(var) = self.real_expr(strip_conversions(left))? else {
            return Err(bad_dist(
                "the distributed expression of a real `dist` must name one `real` random \
                 variable (an expression, or a non-random value, cannot be weighted)",
            ));
        };
        if self.real_dists.iter().any(|d| d.var == var) {
            return Err(bad_dist(
                "a real variable has two `dist` constraints (the second would silently \
                 replace the first's weights)",
            ));
        }
        let mut items = Vec::new();
        for it in e.dist_items() {
            let v = it.value();
            let w = it.weight();
            if v.kind() == ExpressionKind::ValueRange {
                let (lo, hi) = self.real_bounds(v)?;
                for b in [&lo, &hi].into_iter().flatten() {
                    let mut any = false;
                    b.for_each_var(&mut |_| any = true);
                    if any {
                        return Err(bad_dist(
                            "a random variable in a `dist` range bound; bounds are fixed values",
                        ));
                    }
                }
                let Some(w) = w else {
                    return Err(bad_dist(
                        "a range item of a real `dist` needs an explicit `:/` weight",
                    ));
                };
                if w.kind != DistWeightKind::PerRange {
                    return Err(bad_dist(
                        "`:=` on a range of a real `dist` would give each of its infinitely many \
                         values that weight; use `:/` (IEEE 1800-2023 18.5.3)",
                    ));
                }
                items.push(RealDistItem {
                    span: RealSpan::Range { lo, hi },
                    weight: self.real_weight(w.expr)?,
                });
            } else {
                let point = self.real_fixed(v, "a `dist` value")?;
                // LRM 18.5.3: an item without a weight is `:= 1`; for a single
                // value `:=` and `:/` mean the same.
                let weight = match w {
                    Some(w) => self.real_weight(w.expr)?,
                    None => Expr::constant(Ty::unsigned(32), 1u32),
                };
                items.push(RealDistItem {
                    span: RealSpan::Point(point),
                    weight,
                });
            }
        }
        let default = match e.dist_default_weight() {
            Some(w) if w.kind == DistWeightKind::PerRange => Some(self.real_weight(w.expr)?),
            Some(_) => {
                return Err(bad_dist(
                    "`default := w` over every real value not listed would give each of \
                     infinitely many values that weight; use `default :/ w`",
                ));
            }
            None => None,
        };
        if items.is_empty() && default.is_none() {
            return Err(bad_dist("a `dist` with no items"));
        }
        self.real_dists.push(RealDist {
            var,
            items,
            default,
        });
        Ok(())
    }
}

/// Whether `x` reads an integral random variable.
fn has_var(x: &Expr) -> bool {
    let mut any = false;
    x.for_each_var(&mut |_, _| any = true);
    any
}