vj_sim/constraints/

registry.rs

//! Run-time dispatch of `obj.randomize()` (plan C3.5; LRM 18.6.1, 18.6.3).
//!
//! # What this is
//!
//! Compiling a class (`vj-codegen`'s `classes_randomize`) turns its `rand`
//! fields and constraint blocks into a [`Program`]: the constraint IR plus,
//! for every random and state variable, *where its value lives* in an object's
//! flat field buffer. The program is registered per [`ClassTemplateId`] in a
//! process-wide table (the same shape and lifetime as the other per-template
//! tables in [`crate::objects`]), and a compiled `obj.randomize()` is one
//! `sv_rt_obj(Randomize, h, ..)` call that lands in [`randomize`] here.
//!
//! # Dispatch is by dynamic class
//!
//! [`randomize`] looks the program up under the object's *dynamic* template
//! ([`objects::dynamic_template`]), so `base_handle.randomize()` on a derived
//! object solves the derived class's constraints (LRM 18.6.1: `randomize` is
//! virtual). No vtable slot is involved: the object already carries its own
//! template id, and a program is registered for every class template, so
//! "dispatch" is a table lookup, which is virtual in effect and cannot collide
//! with a user method.
//!
//! # Semantics implemented here
//!
//! * A `rand_mode(0)` variable is inactive and "treated the same as any other
//!   state variable" (LRM 18.8): it is fixed at its current value for the
//!   solve, and a variable that is not rand-active is not forced into its
//!   enum domain either.
//! * A state variable (or an inactive random variable) holding an X/Z bit is
//!   an error ([`Outcome::StateUnknown`], IEEE 1800-2023 18.3), never a silent
//!   0.
//! * Success writes every active random variable (2-state value, no unknown
//!   bits) and stores the advanced PRNG state back to the object.
//! * Failure of any kind writes **nothing** and does not advance the object's
//!   PRNG (LRM 18.6.3: "if randomize fails, the constraints are infeasible
//!   and the random variables retain their previous values"). The solver
//!   consumes no draws for an unsatisfiable problem, and the seed is only
//!   stored on success, so the second property holds for every error.
//!
//! * A `randc` variable is drawn first, from its own cyclic permutation (LRM
//!   18.4.2; [`super::randc`]). Its cycle state belongs to the object that
//!   owns the field (the randomized object for an instance property, the class's
//!   static-property object for a `static randc`, so every instance shares one
//!   cycle) and is committed only when the call succeeds. A pick never fails:
//!   the LRM allows `randc` combined with other constraints to "sometimes cause
//!   randomize() to fail", but this implementation starts a new cycle instead
//!   whenever nothing left in the current one is feasible, so a satisfiable
//!   problem always solves.
//! * A `static` property is not in the randomized object: the call site passes
//!   the handle of each static-property object it can reach and a program
//!   that needs one it was not given fails with [`Outcome::StaticUnavailable`].
//!
//! `pre_randomize()`/`post_randomize()` are not run here: they are compiled
//! subroutines, so the call site runs them around this call
//! ([`super::walk`], C18). What a call site adds to its class's constraints is a
//! [`Spec`] (C19, C20): the inline constraints of `with {}` as a fragment
//! program laid over the object's program by [`joint::overlay`], the values of
//! the call's local variables as constants, and the variable list of
//! `randomize(v, ...)` as the complete set of random variables
//! ([`joint::restrict`]). [`randomize_spec`] is the entry point.

use super::array;
use super::bdd::BddBuildError;
use super::dist::{Dist, DistError, SELECTOR_BASE};
use super::func::{self, Func, FuncError};
use super::func_order;
use super::guard;
use super::ir::{Assignment, ConstraintEvalError, Expr, Ty, eval, mask};
use super::joint;
use super::order;
use super::priority::{self, Soft};
use super::randc::RandcState;
use super::real_domain::{self, FloatKind, RealError, RealProblem};
use super::reduce::{self, BlockItems};
use super::solve::{Engine, Group, Measure, Plan, SolveError, Weighted};
use crate::collections;
use crate::netlist::ClassTemplateId;
use crate::objects::{self, FieldSlot, Window};
use num_bigint::BigUint;
use num_traits::{ToPrimitive, Zero};
use std::collections::HashMap;
use std::sync::atomic::{AtomicU32, Ordering};
use std::sync::{Arc, Mutex, OnceLock};

/// Which heap object a [`FieldSlot`] of a [`Program`] is an offset into.
#[derive(Clone, Copy, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub enum Home {
    /// The object being randomized (an instance property).
    Instance,
    /// The static-property singleton of one class specialization (LRM 8.9),
    /// named by an id that is only meaningful within one compile. The
    /// `randomize()` call site passes the handle of each singleton the
    /// program needs as an `(id, handle)` pair ([`randomize`]'s `statics`).
    Static(u32),
    /// One named heap object: a contained `rand` object of a joint solve
    /// (Task C17, LRM 18.5.8). Only a transient program that [`super::joint`]
    /// merged for one call holds this; a registered program never does.
    Object(u64),
}

/// A `rand` class-handle member of a [`Program`]: the object it designates is
/// randomized together with its container when the handle is active and not
/// null (Task C17, LRM 18.5.8).
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct ProgHandle {
    /// Where the handle (one word) lives, as an offset into [`Self::home`].
    pub slot: FieldSlot,
    /// The object [`Self::slot`] is an offset into.
    pub home: Home,
    /// As [`ProgVar::prop_index`]: the handle's `rand_mode` bit, so
    /// `h.rand_mode(0)` takes the object out of the joint solve (LRM 18.8).
    pub prop_index: Option<usize>,
    /// The handle's LSB within the property's value bits: 0 for a `rand` handle
    /// property, `64 * i` for element `i` of a `rand` fixed array of handles
    /// (LRM 18.4, 18.5.8: every element's object is randomized with its container).
    pub bit: u32,
}

/// A random variable of a [`Program`].
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct ProgVar {
    /// Declared type (the solver's 2-state view of it).
    pub ty: Ty,
    /// Where its (4-state packed) value lives, as an offset into [`Self::home`].
    pub slot: FieldSlot,
    /// The object [`Self::slot`] is an offset into.
    pub home: Home,
    /// Index of this property in the template's [`objects::rand_props`]
    /// order, which is also the index into the object's `rand_mode` vector.
    /// `None` for a `static` property: it belongs to the class, not to an
    /// object, so it has no per-object `rand_mode` bit and is always active.
    pub prop_index: Option<usize>,
    /// Index into [`Program::conjuncts`] of this variable's implicit enum
    /// domain constraint, if it has one (dropped while the variable is
    /// inactive).
    pub domain_conjunct: Option<usize>,
    /// Whether the variable is `randc` (LRM 18.4.2): drawn first, from its own
    /// cyclic permutation, instead of from the joint solution space.
    pub randc: bool,
    /// For a member of an unpacked struct or an element of a fixed-size unpacked
    /// array held in a property (XC-059, LRM 18.4): [`Self::slot`] is then the
    /// whole property and the variable is this window of it. `None` for a
    /// variable that is a whole property.
    pub window: Option<Window>,
}

impl ProgVar {
    /// The key of this variable's `randc` cycle in its object
    /// ([`objects::randc_state`]): its property's word offset, with the window's
    /// bit position above bit 32 so two leaves of one property have two cycles.
    fn randc_key(&self) -> usize {
        randc_key(self.slot, self.window)
    }
}

/// The `randc` cycle key of the leaf `window` of property `slot` (see
/// [`ProgVar::randc_key`]).
fn randc_key(slot: FieldSlot, window: Option<Window>) -> usize {
    match window {
        None => slot.offset,
        Some(w) => slot.offset | ((w.bit as usize + 1) << 32),
    }
}

/// A state variable of a [`Program`] (a non-rand field read by a constraint).
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct ProgState {
    /// Declared type.
    pub ty: Ty,
    /// Where its (4-state packed) value lives, as an offset into [`Self::home`].
    pub slot: FieldSlot,
    /// As [`ProgVar::window`]: the value is this window of the property at the
    /// end of [`Self::via`] (or of [`Self::slot`] when there is none).
    pub window: Option<Window>,
    /// The object [`Self::slot`] is an offset into.
    pub home: Home,
    /// For a value read through object handles (`a.x`, `next.next.n`; LRM
    /// 18.5.12): [`Self::slot`] is then the *root handle* property and these
    /// are the member slots followed from it, one per `.`, the last holding the
    /// value of type [`Self::ty`]. Empty for a plain property.
    pub via: Vec<FieldSlot>,
    /// The bit of [`Self::slot`] the root handle's word starts at: 0 for a
    /// handle property, `64 * i` for element `i` of a fixed array of handles
    /// (`es[i].v`, LRM 18.5.8).
    pub root_bit: u32,
    /// The value is the dynamic class template id of the object the handle
    /// [`Self::slot`] / [`Self::via`] reach names (a virtual call's selector).
    #[serde(default)]
    pub class_of: bool,
}

/// One class template's solver input, resolved to object-field locations.
#[derive(Clone, Debug, Default, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct Program {
    /// Random variables, indexed by the IR's `VarId`.
    pub vars: Vec<ProgVar>,
    /// State variables, indexed by the IR's `StateId`.
    pub states: Vec<ProgState>,
    /// One-bit expressions that must all hold.
    pub conjuncts: Vec<Expr>,
    /// `solve ... before` edges `(first, later)` over [`Self::vars`] (LRM
    /// 18.5.9). Acyclic (the builder checks). An edge whose variable is
    /// inactive (`rand_mode(0)`) is ignored for that call: it is a constant
    /// then, and there is nothing to order.
    pub before: Vec<(u32, u32)>,
    /// The `dist` constraints (LRM 18.5.3). Dist `j`'s hidden selector variable
    /// appears in [`Self::conjuncts`] as `Var(SELECTOR_BASE + j)`; it is not a
    /// field and is numbered after the active variables for each call.
    pub dists: Vec<Dist>,
    /// The `real`/`shortreal` random variables, indexed by the real
    /// problem's variable ids (their own numbering, separate from
    /// [`Self::vars`]).
    pub real_vars: Vec<ProgRealVar>,
    /// The constraints over [`Self::real_vars`] (Task C9), solved after the
    /// integral variables with the same PRNG stream.
    pub real: RealProblem,
    /// The dynamic arrays and queues the constraints reach (Task C14), indexed
    /// by the IR's [`super::ir::ArrayId`].
    pub arrays: Vec<ProgArray>,
    /// The functions the constraints call (Task C13), indexed by the IR's
    /// [`super::ir::FuncId`].
    pub funcs: Vec<Func>,
    /// The soft constraints (Task C15, LRM 18.5.13): soft `k`'s discard flag
    /// appears in [`Self::conjuncts`] as `Var(SOFT_BASE + k)` (see
    /// [`super::priority`]). Empty for a class with none.
    pub softs: Vec<Soft>,
    /// The `rand` class-handle members (Task C17): the objects a joint solve
    /// reaches from an object of this class ([`super::joint`]).
    pub rand_handles: Vec<ProgHandle>,
    /// The named constraint blocks, by ordinal (Task C20): what
    /// `constraint_mode(0)` takes out of the solve. Empty for a program that
    /// did not come from a class (a fragment, a scope randomization).
    pub blocks: Vec<ProgBlock>,
    /// How many `disable soft`s the program holds: the table
    /// [`Soft::disabled_by`] indexes and [`BlockItems::disables`] ranges over.
    pub n_disables: usize,
    /// The targets of an inline fragment's `disable soft`s (empty for a class
    /// program), in the order of the last [`Self::n_disables`] entries: the
    /// overlay discards the base softs they reach (LRM 18.5.13.2, 18.7).
    pub disable_keys: Vec<super::priority::SoftKey>,
}

/// A named constraint block of a [`Program`] (LRM 18.9).
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct ProgBlock {
    /// The object whose `constraint_mode()` state holds the block's mode: the
    /// instance for an ordinary block, the class's static-property object for a
    /// `static` one (its mode is shared by every instance, LRM 18.9).
    pub home: Home,
    /// The block's ordinal among the named blocks of the class, base class
    /// first (a derived override keeps the base block's ordinal): the key into
    /// [`objects::constraint_mode_of`].
    pub ordinal: u32,
    /// The block's conjuncts, a range of [`Program::conjuncts`].
    pub conjuncts: std::ops::Range<usize>,
    /// What the block holds besides conjuncts (a `dist`, a `solve ... before`,
    /// a `real` constraint, a `soft` constraint, a `disable soft`): a call with
    /// the block switched off leaves those out too ([`reduce`]).
    pub items: BlockItems,
}

/// A dynamic array or queue property of a [`Program`] (LRM 18.4, 18.5.7).
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct ProgArray {
    /// Element type (the solver's 2-state view of it).
    pub elem_ty: Ty,
    /// 64-bit words per stored element (`ceil(2 * width / 64)`, 4-state packed:
    /// the same layout the collection store and codegen use).
    pub elem_words: usize,
    /// Where the collection handle lives, as an offset into [`Self::home`].
    pub slot: FieldSlot,
    /// The object [`Self::slot`] is an offset into.
    pub home: Home,
    /// Whether the property is `rand`. A non-`rand` array a constraint reads
    /// is state.
    pub rand: bool,
    /// As [`ProgVar::prop_index`]; one `rand_mode` bit covers the whole array.
    pub prop_index: Option<usize>,
    /// The enum values every element must be one of, for an array of an enum
    /// type (LRM 6.19.3: a `rand` enum is limited to its named values).
    pub elem_domain: Option<Vec<BigUint>>,
    /// An associative array: its keys (hence its size) are never randomized,
    /// only the values at the keys it already has (LRM 18.4), so the solved
    /// values are written back by key instead of resizing a sequence.
    pub assoc: bool,
    /// An array of dynamic arrays or queues (`rand int a[][]`, LRM 18.4): the
    /// property's elements are row handles, and [`Self::elem_ty`] /
    /// [`Self::elem_words`] describe the leaf elements of the rows.
    #[serde(default)]
    pub nested: bool,
    /// For the row template of the array of arrays with this id
    /// ([`super::ir::ArrayNode::RowScope`]): the array exists only in the
    /// constraints, so it has no property ([`Self::slot`] and [`Self::home`] are
    /// placeholders).
    #[serde(default)]
    pub template_of: Option<u32>,
    /// For an array of FIXED-size rows (`rand int b[][4]`, LRM 7.4.5): the rows'
    /// element count `N`. Every row is `N` elements stored inline in its outer
    /// element (one flat 4-state value of `N` leaf elements, lowest index
    /// first) instead of a row collection handle; zero for dynamic rows.
    #[serde(default)]
    pub inner_fixed: u32,
    /// How many levels of rows lie below the array (0 unless [`Self::nested`]):
    /// `rand int a[][][]` is 2. Every level but the last holds row handles
    /// (collections of handles); the last holds the leaf elements, or with
    /// [`Self::inner_fixed`] the inline fixed-size rows.
    #[serde(default)]
    pub row_depth: u32,
    /// When the collection handle is not the whole property but one leaf of an
    /// aggregate (a row of `rand int a[3][]`, a `rand` queue member of an
    /// unpacked struct, LRM 18.4): where it sits in the property's value.
    #[serde(default)]
    pub window: Option<Window>,
}

/// A `real` or `shortreal` random variable of a [`Program`].
#[derive(Clone, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct ProgRealVar {
    /// `real` or `shortreal`.
    pub kind: FloatKind,
    /// Where its (4-state packed) value lives, as an offset into [`Self::home`]:
    /// the IEEE bit pattern in the low 64 (32) bits.
    pub slot: FieldSlot,
    /// The object [`Self::slot`] is an offset into.
    pub home: Home,
    /// As [`ProgVar::prop_index`].
    pub prop_index: Option<usize>,
    /// As [`ProgVar::window`].
    pub window: Option<Window>,
}

/// The result of one [`randomize`] call; the discriminant is the ABI value
/// `ObjOp::Randomize` returns.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
#[repr(u64)]
pub enum Outcome {
    /// The constraints are unsatisfiable: `randomize()` returns 0, nothing
    /// was changed (LRM 18.6.3).
    Unsatisfiable = 0,
    /// A solution was written; `randomize()` returns 1.
    Solved = 1,
    /// The handle is null or stale.
    DeadHandle = 2,
    /// The object's class has no usable program (its constraints could not be
    /// built, or none was registered).
    NoProgram = 3,
    /// A constraint reads a variable holding an X/Z bit.
    StateUnknown = 4,
    /// The constraint BDD exceeded its node budget (the SAT fallback is a
    /// later task).
    TooLarge = 5,
    /// Any other solver or program failure (a malformed program).
    Failed = 6,
    /// The program reads or writes a `static` property of a class whose
    /// static-property object the call site did not pass (a `randomize()`
    /// through a base-class handle on an object of a derived class that
    /// declares its own static `rand`/`randc` variable or constraint state).
    StaticUnavailable = 7,
    /// A `dist` weight evaluated to a negative number, or a weight or bound
    /// divided by zero (IEEE 1800-2023 18.5.3).
    BadDistWeight = 8,
    /// A constraint guard evaluated to `ERROR` (IEEE 1800-2023 18.5.12): a
    /// null handle or X/Z value read where nothing short-circuits it.
    GuardError = 9,
    /// A constraint outside any guard reads a member through a null or deleted
    /// object handle (IEEE 1800-2023 18.5.12: "randomize() fails").
    NullHandle = 10,
    /// A real constraint evaluated to NaN or divided by zero (Task C9).
    RealDomain = 11,
    /// The size constraints of a dynamic array or queue can only be met by a
    /// size beyond the supported maximum (65536 elements).
    ArraySizeTooLarge = 12,
    /// A constraint reads an array element outside `0..size` (IEEE 1800-2023
    /// 18.5.7.1) where no guard excludes it.
    ArrayIndexOutOfRange = 13,
    /// Every array size satisfying the size constraints alone made the full
    /// problem unsatisfiable, and the bounded search for another one gave up.
    ArraySizeSearch = 14,
    /// A function called from a constraint failed (division by zero, a runaway
    /// loop, recursion past the supported depth; IEEE 1800-2023 18.5.11).
    FunctionFailed = 15,
    /// The implicit order the random arguments of function calls impose is
    /// circular (IEEE 1800-2023 18.5.11).
    ImplicitOrderCycle = 16,
    /// A constraint compares the results of function calls over several random
    /// variables, and no draw tried satisfied it (the bounded search gave up).
    FunctionSearch = 17,
    /// The objects of a joint solve (a `rand` object member, IEEE 1800-2023
    /// 18.5.8) use something the joint solver does not combine yet: `real`
    /// random variables, or a `static` random variable two members of the tree share.
    GlobalUnsupported = 18,
    /// The constraint problem exceeded the BDD node budget and the SAT fallback
    /// ([`super::sat`]) did not finish within its time limit.
    SatTimeout = 19,
    /// The constraint problem exceeded the BDD node budget and needs something
    /// the SAT fallback cannot sample faithfully (a `dist` weighted by a count
    /// of more than 512 models, a `dist` over a variable wider than 32 bits or
    /// with more than 1024 feasible values per range, a `randc` variable wider
    /// than 10 bits).
    SatUnsupported = 20,
}

impl Outcome {
    /// The ABI value.
    pub fn code(self) -> u64 {
        self as u64
    }

    /// The outcome with ABI value `code`, if any.
    pub fn from_code(code: u64) -> Option<Outcome> {
        [
            Outcome::Unsatisfiable,
            Outcome::Solved,
            Outcome::DeadHandle,
            Outcome::NoProgram,
            Outcome::StateUnknown,
            Outcome::TooLarge,
            Outcome::Failed,
            Outcome::StaticUnavailable,
            Outcome::BadDistWeight,
            Outcome::GuardError,
            Outcome::NullHandle,
            Outcome::RealDomain,
            Outcome::ArraySizeTooLarge,
            Outcome::ArrayIndexOutOfRange,
            Outcome::ArraySizeSearch,
            Outcome::FunctionFailed,
            Outcome::ImplicitOrderCycle,
            Outcome::FunctionSearch,
            Outcome::GlobalUnsupported,
            Outcome::SatTimeout,
            Outcome::SatUnsupported,
        ]
        .into_iter()
        .find(|o| o.code() == code)
    }

    /// The diagnostic a compiled call site prints for this outcome, if it is
    /// an error rather than an ordinary result (an unsatisfiable problem is
    /// not an error: `randomize()` just returns 0, LRM 18.6.3).
    pub fn error_message(self) -> Option<&'static str> {
        match self {
            Outcome::Unsatisfiable | Outcome::Solved => None,
            Outcome::DeadHandle => Some("randomize() on a null or deleted object"),
            Outcome::NoProgram => Some(
                "randomize(): the constraints of this object's class could not be compiled \
                 (see the class's constraint blocks)",
            ),
            Outcome::StateUnknown => Some(
                "randomize(): a constraint reads a variable with an X or Z bit; a 4-state \
                 value in a constraint is an error (IEEE 1800-2023 18.3)",
            ),
            Outcome::TooLarge => Some(
                "randomize(): the constraint problem is too large for both the BDD solver \
                 (node budget exceeded) and its SAT fallback (clause limit exceeded)",
            ),
            Outcome::SatTimeout => Some(
                "randomize(): the constraint problem is too large for the BDD solver and \
                 the SAT fallback did not find a solution within its time limit",
            ),
            Outcome::SatUnsupported => Some(
                "randomize(): the constraint problem is too large for the BDD solver and \
                 uses a `dist` over an expression with more than 512 feasible assignments, a `dist` \
                 over a variable wider than 32 bits or with more than 1024 feasible values per \
                 range, or a `randc` variable wider than 10 bits, which the SAT fallback does \
                 not support",
            ),
            Outcome::Failed => Some("randomize(): internal solver failure on a malformed program"),
            Outcome::StaticUnavailable => Some(
                "randomize(): the object's class declares a static property used by its \
                 constraints or `rand`/`randc` variables that this call site cannot reach \
                 (it is declared in a class derived from the handle's static type); call \
                 randomize() through a handle of that class",
            ),
            Outcome::BadDistWeight => Some(
                "randomize(): a `dist` weight is negative, or a weight or range bound \
                 divides by zero (IEEE 1800-2023 18.5.3)",
            ),
            Outcome::GuardError => Some(
                "randomize(): the guard of an implication or `if` constraint evaluated to \
                 ERROR (a null object handle, or an X/Z value, read where no operand \
                 decides it; IEEE 1800-2023 18.5.12)",
            ),
            Outcome::NullHandle => Some(
                "randomize(): a constraint reads a member through a null or deleted object \
                 handle (IEEE 1800-2023 18.5.12)",
            ),
            Outcome::RealDomain => Some(
                "randomize(): a constraint on a real variable evaluates to NaN or divides by \
                 zero, so it has no well-defined set of solutions",
            ),
            Outcome::ArraySizeTooLarge => Some(
                "randomize(): the constraints on the size of a dynamic array or queue can \
                 only be met by a size above 65536 elements, which is not supported",
            ),
            Outcome::ArrayIndexOutOfRange => Some(
                "randomize(): a constraint reads an array element outside the array's \
                 bounds (guard it with an `if` on the size, IEEE 1800-2023 18.5.7.1)",
            ),
            Outcome::ArraySizeSearch => Some(
                "randomize(): no array size tried satisfied both the size constraints and \
                 the element constraints (the bounded search over sizes gave up)",
            ),
            Outcome::FunctionFailed => Some(
                "randomize(): a function called from a constraint failed (division by zero, \
                 a runaway loop or recursion that is too deep)",
            ),
            Outcome::ImplicitOrderCycle => Some(
                "randomize(): the random arguments of function calls in the constraints \
                 impose a circular solve order (IEEE 1800-2023 18.5.11)",
            ),
            Outcome::FunctionSearch => Some(
                "randomize(): no draw satisfied a constraint that compares the results of \
                 function calls over several random variables (the bounded search gave up)",
            ),
            Outcome::GlobalUnsupported => Some(
                "randomize(): the object tree being randomized together (a `rand` object \
                 member, IEEE 1800-2023 18.5.8) has `real` random variables, or a `static` \
                 random variable that two objects of the tree share, which the joint solver \
                 does not combine yet",
            ),
        }
    }
}

type ProgramTable = HashMap<ClassTemplateId, Arc<Result<Program, String>>>;

fn table() -> &'static Mutex<ProgramTable> {
    static T: OnceLock<Mutex<ProgramTable>> = OnceLock::new();
    T.get_or_init(|| Mutex::new(HashMap::new()))
}

/// Registers (replacing any earlier registration) `template`'s program, or
/// the reason it could not be built. A failure here must not fail the compile
/// by itself: a class whose constraints this build cannot yet handle is fine
/// as long as nothing calls `randomize()` on it; the compiler records the
/// failure and reports it at a call site that could reach the class.
pub fn register_program(template: ClassTemplateId, program: Result<Program, String>) {
    table()
        .lock()
        .unwrap_or_else(|e| e.into_inner())
        .insert(template, Arc::new(program));
}

/// `template`'s registered program, or the reason there is none.
pub fn program(template: ClassTemplateId) -> Option<Arc<Result<Program, String>>> {
    table()
        .lock()
        .unwrap_or_else(|e| e.into_inner())
        .get(&template)
        .cloned()
}

/// What a design image carries of the solver: the program of each class
/// template and every call site's [`Spec`], by the ids baked into the machine
/// code (see [`snapshot`], [`preload`]).
#[derive(serde::Serialize, serde::Deserialize)]
struct Snapshot {
    /// `(template id, program or the reason there is none)`, ascending by id.
    programs: Vec<(u32, Result<Program, String>)>,
    /// `(spec id, spec)`, ascending by id.
    specs: Vec<(u32, Spec)>,
}

/// The solver state `obj.randomize()` and `std::randomize()` call sites of the
/// design just compiled depend on, as bytes: the program registered for each of
/// `templates` and every spec registered in this process. Empty when there is
/// neither (a design that never randomizes carries nothing). Deterministic:
/// ascending ids, and `postcard` has no hash-order or padding.
pub fn snapshot(templates: &[ClassTemplateId]) -> Vec<u8> {
    let mut ids: Vec<u32> = templates.iter().map(|t| t.0).collect();
    ids.sort_unstable();
    ids.dedup();
    let programs: Vec<(u32, Result<Program, String>)> = ids
        .into_iter()
        .filter_map(|id| program(ClassTemplateId(id)).map(|p| (id, Result::clone(&p))))
        .collect();
    let specs: Vec<(u32, Spec)> = all_specs()
        .into_iter()
        .map(|(id, s)| (id, Spec::clone(&s)))
        .collect();
    if programs.is_empty() && specs.is_empty() {
        return Vec::new();
    }
    postcard::to_allocvec(&Snapshot { programs, specs })
        .expect("a constraint program is plain data and always serializes")
}

/// Registers what [`snapshot`] captured, under the same ids. Empty bytes
/// register nothing.
pub fn preload(bytes: &[u8]) -> Result<(), String> {
    if bytes.is_empty() {
        return Ok(());
    }
    let snap: Snapshot =
        postcard::from_bytes(bytes).map_err(|e| format!("randomize section: {e}"))?;
    for (id, p) in snap.programs {
        register_program(ClassTemplateId(id), p);
    }
    for (id, s) in snap.specs {
        register_spec_at(id, s);
    }
    Ok(())
}

/// The 4-state packed field `words` of a `width`-bit value as `(val, unk)`.
pub(super) fn unpack(words: &[u64], width: u32) -> (BigUint, BigUint) {
    let mut n = BigUint::zero();
    for (i, w) in words.iter().enumerate() {
        n |= BigUint::from(*w) << (64 * i);
    }
    let m = mask(width);
    (&n & &m, (n >> width) & m)
}

/// A 2-state `val` as `words` packed words (all unknown bits zero), or `None`
/// if it does not fit.
fn pack(val: &BigUint, words: usize) -> Option<Vec<u64>> {
    let mut d = val.to_u64_digits();
    if d.len() > words {
        return None;
    }
    d.resize(words, 0);
    Some(d)
}

/// The current 2-state value of the field `slot` (or its leaf `window`) of
/// width `ty`; `Ok(None)` if it has an X/Z bit, `Err` if `h` is dead.
fn read(
    h: u64,
    slot: FieldSlot,
    window: Option<Window>,
    ty: Ty,
) -> Result<Option<BigUint>, Outcome> {
    let (val, unk) = read_unknown(h, slot, window, ty.width)?;
    Ok(if unk.is_zero() { Some(val) } else { None })
}

/// The `(value, unknown bits)` of the field `slot` (or its leaf `window`) as a
/// `width`-bit value; `Err` if `h` is dead.
fn read_unknown(
    h: u64,
    slot: FieldSlot,
    window: Option<Window>,
    width: u32,
) -> Result<(BigUint, BigUint), Outcome> {
    match window {
        None => {
            let mut buf = vec![0u64; slot.words];
            if !objects::field_get(h, slot, &mut buf) {
                return Err(Outcome::DeadHandle);
            }
            Ok(unpack(&buf, width))
        }
        Some(w) => {
            let n = (w.width as usize).div_ceil(64);
            let (mut val, mut unk) = (vec![0u64; n], vec![0u64; n]);
            if !objects::field_get_window(h, slot, w, &mut val, &mut unk) {
                return Err(Outcome::DeadHandle);
            }
            let m = mask(width);
            let to_big = |ws: &[u64]| {
                ws.iter().enumerate().fold(BigUint::zero(), |a, (i, x)| {
                    a | (BigUint::from(*x) << (64 * i))
                })
            };
            Ok((to_big(&val) & &m, to_big(&unk) & &m))
        }
    }
}

/// What reading a state variable found.
enum Reading {
    /// The value, or `None` if it has an X/Z bit.
    Value(Option<BigUint>),
    /// An object handle on the way to it was null (or its object deleted).
    NullHandle,
}

/// Reads state `s`, owned by object `owner`, following its handle chain
/// ([`ProgState::via`]). A null handle on the chain is a [`Reading::NullHandle`],
/// an X/Z handle an unreadable value, and a dead `owner` itself an error.
fn read_state(owner: u64, s: &ProgState) -> Result<Reading, Outcome> {
    let (mut obj, mut slot) = (owner, s.slot);
    for (i, hop) in s.via.iter().enumerate() {
        let mut buf = vec![0u64; slot.words];
        let bit = if i == 0 { s.root_bit } else { 0 };
        if !objects::field_get(obj, slot, &mut buf) {
            return if i == 0 {
                Err(Outcome::DeadHandle)
            } else {
                Ok(Reading::NullHandle)
            };
        }
        // A handle is one word of the value half; element `bit / 64` of a fixed
        // array of handles has its unknown bits at the same offset of the upper
        // half (as `joint::read_handle`).
        let w = (bit / 64) as usize;
        let half = slot.words / 2;
        let (Some(&v), Some(&u)) = (buf.get(w), buf.get(half + w)) else {
            return Err(Outcome::Failed);
        };
        let (val, unk) = (BigUint::from(v), BigUint::from(u));
        if !unk.is_zero() {
            return Ok(Reading::Value(None));
        }
        match val.to_u64() {
            Some(0) => return Ok(Reading::NullHandle),
            Some(next) => obj = next,
            None => return Err(Outcome::Failed),
        }
        slot = *hop;
    }
    if s.class_of {
        let (val, unk) = match read_unknown(obj, slot, None, 64) {
            Ok(r) => r,
            Err(_) if s.via.is_empty() => return Err(Outcome::DeadHandle),
            Err(_) => return Ok(Reading::NullHandle),
        };
        if !unk.is_zero() {
            return Ok(Reading::Value(None));
        }
        return match val.to_u64() {
            Some(0) => Ok(Reading::NullHandle),
            Some(h) => Ok(match objects::dynamic_template(h) {
                Some(t) => Reading::Value(Some(BigUint::from(t.0))),
                None => Reading::NullHandle,
            }),
            None => Err(Outcome::Failed),
        };
    }
    match read_unknown(obj, slot, s.window, s.ty.width) {
        Ok((val, unk)) => Ok(Reading::Value(if unk.is_zero() { Some(val) } else { None })),
        Err(_) if s.via.is_empty() => Err(Outcome::DeadHandle),
        Err(_) => Ok(Reading::NullHandle),
    }
}

/// The heap object `home` names for a call on `h`, given the static-property
/// objects the call site passed.
pub(super) fn owner(home: Home, h: u64, statics: &[(u32, u64)]) -> Result<u64, Outcome> {
    match home {
        Home::Instance => Ok(h),
        Home::Object(o) => Ok(o),
        Home::Static(id) => statics
            .iter()
            .find(|(i, s)| *i == id && *s != 0)
            .map(|&(_, s)| s)
            .ok_or(Outcome::StaticUnavailable),
    }
}

/// Whether the unreadable state `id` is so because of a null handle.
fn unreadable_outcome(id: u32, null_state: &[bool]) -> Outcome {
    if null_state.get(id as usize).copied().unwrap_or(false) {
        Outcome::NullHandle
    } else {
        Outcome::StateUnknown
    }
}

/// The solver's failure `e` as the call's outcome.
fn outcome_of(e: SolveError, null_state: &[bool]) -> Outcome {
    match e {
        SolveError::Unsatisfiable => Outcome::Unsatisfiable,
        SolveError::Build(BddBuildError::StateUnknown(id)) => unreadable_outcome(id, null_state),
        SolveError::Build(BddBuildError::TooLarge { .. } | BddBuildError::CnfTooLarge { .. }) => {
            Outcome::TooLarge
        }
        SolveError::SatTimeout => Outcome::SatTimeout,
        SolveError::SatUnsupported { .. } => Outcome::SatUnsupported,
        SolveError::Build(_)
        | SolveError::BadOrder { .. }
        | SolveError::BadPlan { .. }
        | SolveError::SatModelRejected
        | SolveError::SatSolverFailure { .. } => Outcome::Failed,
    }
}

/// A `dist` weight failure `e` as the call's outcome.
fn outcome_of_dist(e: DistError, null_state: &[bool]) -> Outcome {
    match e {
        DistError::Eval(ConstraintEvalError::StateUnknown(id)) => {
            unreadable_outcome(id, null_state)
        }
        DistError::Eval(ConstraintEvalError::DivideByZero) | DistError::NegativeWeight => {
            Outcome::BadDistWeight
        }
        DistError::Eval(
            ConstraintEvalError::UnboundVar(_)
            | ConstraintEvalError::UnboundState(_)
            | ConstraintEvalError::Unexpanded,
        ) => Outcome::Failed,
    }
}

/// A real solver failure `e` as the call's outcome.
fn outcome_of_real(e: RealError, null_state: &[bool]) -> Outcome {
    match e {
        RealError::Unsatisfiable => Outcome::Unsatisfiable,
        RealError::GuardError => Outcome::GuardError,
        RealError::StateUnreadable(id) => unreadable_outcome(id, null_state),
        RealError::NonFinite(_) => Outcome::RealDomain,
        RealError::BadWeight => Outcome::BadDistWeight,
        RealError::Shape(_) => Outcome::Failed,
    }
}

/// One solved value to store: a whole property, or one leaf `window` of it.
struct Write {
    owner: u64,
    slot: FieldSlot,
    window: Option<Window>,
    /// The value, packed for the property (`slot.words`) or the leaf
    /// (`ceil(width/64)`).
    words: Vec<u64>,
}

impl Write {
    /// The write of `val` to the field `slot` (or its leaf `window`) of `owner`;
    /// `None` when `val` does not fit.
    fn new(owner: u64, slot: FieldSlot, window: Option<Window>, val: &BigUint) -> Option<Write> {
        let n = match window {
            None => slot.words,
            Some(w) => (w.width as usize).div_ceil(64),
        };
        Some(Write {
            owner,
            slot,
            window,
            words: pack(val, n)?,
        })
    }

    /// Stores the value; `false` when the object is dead.
    fn apply(&self) -> bool {
        match self.window {
            None => objects::field_set(self.owner, self.slot, &self.words),
            Some(w) => objects::field_set_window(self.owner, self.slot, w, &self.words),
        }
    }
}

/// Solves the real variables of `program` (Task C9) and returns the field
/// writes for the active ones; nothing is written here.
/// An inactive (`rand_mode(0)`) real variable is a constant holding its field's
/// current value, and an X/Z bit in it is a [`Outcome::StateUnknown`].
#[allow(clippy::too_many_arguments)]
fn run_real(
    program: &Program,
    h: u64,
    rand_mode: &[bool],
    statics: &[(u32, u64)],
    states: &[Option<BigUint>],
    null_state: &[bool],
    ints: Option<(&[Option<u32>], &[BigUint])>,
    seed: &mut u64,
) -> Result<Vec<Write>, Outcome> {
    if program.real_vars.is_empty() {
        return Ok(Vec::new());
    }
    if program.real_vars.len() != program.real.kinds.len() {
        return Err(Outcome::Failed);
    }
    let mut owners = Vec::with_capacity(program.real_vars.len());
    let mut known = Vec::with_capacity(program.real_vars.len());
    for v in &program.real_vars {
        let o = owner(v.home, h, statics)?;
        let active = match v.prop_index {
            Some(i) => rand_mode.get(i).copied().ok_or(Outcome::Failed)?,
            None => true,
        };
        known.push(if active {
            None
        } else {
            match read(o, v.slot, v.window, Ty::unsigned(v.kind.width()))? {
                Some(bits) => Some(v.kind.from_bits(&bits)),
                None => return Err(Outcome::StateUnknown),
            }
        });
        owners.push(o);
    }
    // A real condition that reads an integral random variable (LRM 18.5.13)
    // reads the value the integral solve drew for it, as a state: an active
    // variable's drawn value, an inactive one's state (module docs of
    // [`super::build::real`]).
    let (lowered, ext);
    let (problem, states) = match ints {
        Some((var_new, values)) if program.real.reads_int_vars() => {
            let mut e = states.to_vec();
            let mut ix = Vec::with_capacity(var_new.len());
            let mut inactive = program.states.len();
            for d in var_new {
                match d {
                    Some(d) => {
                        ix.push(e.len() as u32);
                        e.push(Some(
                            values.get(*d as usize).ok_or(Outcome::Failed)?.clone(),
                        ));
                    }
                    None => {
                        ix.push(inactive as u32);
                        inactive += 1;
                    }
                }
            }
            lowered = program
                .real
                .with_int_vars(|v, t| Expr::State(ix[v as usize], t));
            ext = e;
            (&lowered, &ext[..])
        }
        _ => (&program.real, states),
    };
    let solved = real_domain::solve(problem, &known, states, seed)
        .map_err(|e| outcome_of_real(e, null_state))?;
    let mut writes = Vec::new();
    for ((v, o), x) in program.real_vars.iter().zip(owners).zip(solved) {
        let Some(x) = x else { continue };
        match Write::new(o, v.slot, v.window, &BigUint::from(v.kind.to_bits(x))) {
            Some(w) => writes.push(w),
            None => return Err(Outcome::Failed),
        }
    }
    Ok(writes)
}

/// Everything about one `randomize()` call that does not depend on the array
/// sizes it will choose.
struct Call<'a> {
    program: &'a Program,
    h: u64,
    rand_mode: &'a [bool],
    statics: &'a [(u32, u64)],
    var_owner: Vec<u64>,
    /// Dense number of each program variable that is active this call.
    var_new: Vec<Option<u32>>,
    /// Types of the active variables, in dense order.
    var_tys: Vec<Ty>,
    /// Program index of each active variable, in dense order.
    active_ids: Vec<usize>,
    /// Each program array as this call sees it.
    arrays: Vec<array::ArrayState>,
    array_owner: Vec<u64>,
    /// The program's states, then the inactive variables read as states.
    states: Vec<Option<BigUint>>,
    /// Which unreadable states are so because of a null handle (not X/Z).
    null_state: Vec<bool>,
    /// Set when the last attempt's integral part was solved and its real part
    /// was not (see [`solve_expanded`]).
    real_unsat: std::cell::Cell<bool>,
}

/// What one successful attempt drew.
struct Solution {
    /// A value per active variable, then per element variable.
    values: Vec<BigUint>,
    randc_keys: Vec<(u64, usize)>,
    randc_work: Vec<RandcState>,
    real_writes: Vec<Write>,
}

/// Reads program array `a` (owned by `owner`) as the call sees it.
fn read_array(a: &ProgArray, owner: u64, active: bool) -> Result<array::ArrayState, Outcome> {
    if let Some(outer) = a.template_of {
        // A row template exists only in the constraints.
        return Ok(array::ArrayState {
            elem_ty: a.elem_ty,
            active: false,
            cur: Vec::new(),
            domain: None,
            rows: None,
            template_of: Some(outer),
        });
    }
    let (handle, unk) = read_unknown(owner, a.slot, a.window, 64)?;
    if !unk.is_zero() {
        return Err(Outcome::Failed);
    }
    let handle = handle.to_u64().ok_or(Outcome::Failed)?;
    let leaves = |h: u64| -> Vec<Option<BigUint>> {
        collections::elements(h)
            .iter()
            .map(|words| {
                let (val, unk) = unpack(words, a.elem_ty.width);
                if unk.is_zero() { Some(val) } else { None }
            })
            .collect()
    };
    if a.nested {
        return read_rows(a, handle, a.row_depth.max(1), active, &leaves);
    }
    Ok(array::ArrayState::flat(a.elem_ty, active, leaves(handle))
        .with_domain(a.elem_domain.clone()))
}

/// Reads the rows of the array of arrays `a` held in `handle`, `levels` levels
/// of rows deep (LRM 1800-2023 7.5, 7.10; 18.5.8): each element of the
/// collection is the handle of a row, which is a leaf collection when `levels`
/// is 1 and a collection of rows otherwise.
fn read_rows(
    a: &ProgArray,
    handle: u64,
    levels: u32,
    active: bool,
    leaves: &dyn Fn(u64) -> Vec<Option<BigUint>>,
) -> Result<array::ArrayState, Outcome> {
    let mut cur_rows = Vec::new();
    let mut deeper = Vec::new();
    for words in collections::elements(handle) {
        if levels == 1 && a.inner_fixed > 0 {
            // The row is stored inline: `inner_fixed` leaf elements in one
            // flat 4-state value (value bits, then unknown bits).
            let w = a.elem_ty.width;
            let (val, unk) = unpack(&words, w * a.inner_fixed);
            let m = mask(w);
            cur_rows.push(
                (0..a.inner_fixed)
                    .map(|e| {
                        let sh = u64::from(e * w);
                        ((&unk >> sh) & &m).is_zero().then(|| (&val >> sh) & &m)
                    })
                    .collect(),
            );
            continue;
        }
        let (row, unk) = unpack(&words, 64);
        if !unk.is_zero() {
            return Err(Outcome::Failed);
        }
        let row = row.to_u64().ok_or(Outcome::Failed)?;
        if levels == 1 {
            cur_rows.push(leaves(row));
        } else {
            deeper.push(read_rows(a, row, levels - 1, active, leaves)?);
        }
    }
    let n = cur_rows.len().max(deeper.len());
    Ok(array::ArrayState {
        elem_ty: a.elem_ty,
        active,
        cur: vec![Some(BigUint::from(0u8)); n],
        domain: a.elem_domain.clone(),
        rows: Some(array::RowsState::new(levels, cur_rows, deeper)),
        template_of: None,
    })
}

/// The call's outcome for a failed function call `e`.
fn outcome_of_func(e: FuncError, null_state: &[bool]) -> Outcome {
    match e {
        FuncError::Eval(ConstraintEvalError::StateUnknown(id)) => {
            unreadable_outcome(id, null_state)
        }
        FuncError::Eval(ConstraintEvalError::DivideByZero)
        | FuncError::TooDeep { .. }
        | FuncError::StepLimit { .. } => Outcome::FunctionFailed,
        FuncError::Eval(
            ConstraintEvalError::UnboundVar(_)
            | ConstraintEvalError::UnboundState(_)
            | ConstraintEvalError::Unexpanded,
        )
        | FuncError::Malformed(_) => Outcome::Failed,
    }
}

/// The call's outcome for an expansion failure `e`.
fn outcome_of_expand(e: array::ExpandError, null_state: &[bool]) -> Outcome {
    match e {
        array::ExpandError::IndexOutOfRange { .. }
        | array::ExpandError::LeafIndexOutOfRange { .. } => Outcome::ArrayIndexOutOfRange,
        array::ExpandError::GuardError => Outcome::GuardError,
        array::ExpandError::StateUnknown(id) => unreadable_outcome(id, null_state),
        array::ExpandError::Func(e) => outcome_of_func(e, null_state),
        array::ExpandError::NonConstantIndex
        | array::ExpandError::DistRandomBound
        | array::ExpandError::Malformed(_) => Outcome::Failed,
    }
}

/// The call's outcome for a size-solve failure `e`.
fn outcome_of_size(e: array::SizeError, null_state: &[bool]) -> Outcome {
    match e {
        array::SizeError::Unsatisfiable => Outcome::Unsatisfiable,
        array::SizeError::TooLarge => Outcome::ArraySizeTooLarge,
        array::SizeError::GuardError => Outcome::GuardError,
        array::SizeError::Solve(e) => outcome_of(e, null_state),
    }
}

/// How many draws a stage with a check (a constraint comparing function results
/// over its own random variables) may try before the search is given up.
const MAX_CHECK_TRIES: usize = 4096;

/// Whether every check holds for the draw `drawn` of the stage's variables: the
/// calls are evaluated on the drawn argument values.
fn checks_hold(
    checks: &[Expr],
    drawn: &[BigUint],
    funcs: &[Func],
    states: &[Option<BigUint>],
    null_state: &[bool],
) -> Result<bool, Outcome> {
    let asg = Assignment {
        vars: drawn.to_vec(),
        states: states.to_vec(),
    };
    for c in checks {
        let c = c.substitute_vars(&mut |v, t| match drawn.get(v as usize) {
            Some(val) => Expr::Const(t, val.clone()),
            None => Expr::Var(v, t),
        });
        let c = func::fold_ground_calls(&c, funcs, states)
            .map_err(|e| outcome_of_func(e, null_state))?;
        let v = eval(&c, &asg).map_err(|e| outcome_of_func(FuncError::Eval(e), null_state))?;
        if v.is_zero() {
            return Ok(false);
        }
    }
    Ok(true)
}

/// Solves the scalar problem `x` (the expansion of the program's constraints
/// for one choice of array sizes). [`Outcome::Unsatisfiable`] is an ordinary
/// result the caller may retry with other sizes.
///
/// The real variables are solved after the integral ones (LRM 18.5.13). When a
/// real condition reads an integral random variable the integral draw may leave
/// the real part with no solution (`x < a` with `a == 0` and `x >= 0.0`), so
/// the integral part is redrawn, up to [`REAL_JOINT_TRIES`] times, before the
/// call is [`Outcome::Unsatisfiable`]: a joint solution is found whenever the
/// draws land on one (every such program is sampled by rejection, so a joint
/// solution that a tiny fraction of the integral draws allow may be missed).
fn solve_expanded(
    call: &Call<'_>,
    x: &array::Expanded,
    seed: &mut u64,
) -> Result<Solution, Outcome> {
    let joint = call.program.real.reads_int_vars();
    let tries = if joint { REAL_JOINT_TRIES } else { 1 };
    for _ in 1..tries {
        call.real_unsat.set(false);
        match solve_expanded_once(call, x, seed) {
            Err(Outcome::Unsatisfiable) if call.real_unsat.get() => {}
            r => return r,
        }
    }
    solve_expanded_once(call, x, seed)
}

/// How many integral draws a joint integral/real solve makes before giving up.
const REAL_JOINT_TRIES: usize = 4096;

fn solve_expanded_once(
    call: &Call<'_>,
    x: &array::Expanded,
    seed: &mut u64,
) -> Result<Solution, Outcome> {
    let program = call.program;
    let n_active = call.var_tys.len();
    let n_real = n_active + x.elem_vars.len();
    let mut states = call.states.clone();
    states.extend(x.extra_states.iter().cloned());
    let mut null_state = call.null_state.clone();
    null_state.resize(states.len(), false);
    let mut var_tys = call.var_tys.clone();
    var_tys.extend(x.elem_tys.iter().copied());

    // The dists' hidden selector variables are numbered after every real
    // variable, the elements included (module docs of `super::dist`).
    let conjuncts: Vec<Expr> = x
        .conjuncts
        .iter()
        .map(|c| {
            c.substitute_vars(&mut |v, t| {
                if v >= SELECTOR_BASE {
                    Expr::Var(n_real as u32 + (v - SELECTOR_BASE), t)
                } else {
                    Expr::Var(v, t)
                }
            })
        })
        .collect();
    let assignment = Assignment {
        vars: Vec::new(),
        states: states.clone(),
    };

    // Function calls (Task C13, LRM 18.5.11): the random arguments of a call
    // are solved first, so the variables are solved in stages (module docs of
    // [`super::func_order`]); a program without a call over random variables
    // is one stage, solved exactly as before.
    let has_calls = conjuncts.iter().any(func::has_call);
    let stage_of: Vec<u32> = if has_calls {
        func_order::stages(n_real, &conjuncts).map_err(|_| Outcome::ImplicitOrderCycle)?
    } else {
        vec![0; n_real]
    };
    let n_stages = stage_of.iter().max().map_or(1, |m| *m as usize + 1);
    // A constraint is solved with the latest stage of the variables it holds;
    // a selector variable is solved with its constraint.
    let mut conj_stage: Vec<usize> = Vec::with_capacity(conjuncts.len());
    // The program's dists, then the instances of its `foreach` templates the
    // expansion made (selector slots in that order; a template's own slot is
    // never planned).
    let n_prog_dists = program.dists.len();
    let all_dists: Vec<&Dist> = program.dists.iter().chain(&x.extra_dists).collect();
    let mut dist_stage: Vec<usize> = vec![0; all_dists.len()];
    for c in &conjuncts {
        let mut s = 0usize;
        c.for_each_var(&mut |v, _| {
            if let Some(&st) = stage_of.get(v as usize) {
                s = s.max(st as usize);
            }
        });
        c.for_each_var(&mut |v, _| {
            if let Some(j) = (v as usize).checked_sub(n_real)
                && let Some(d) = dist_stage.get_mut(j)
            {
                *d = s;
            }
        });
        conj_stage.push(s);
    }

    // Ordering between the active variables only, renumbered like them.
    let mut edges: Vec<(u32, u32)> = Vec::with_capacity(program.before.len());
    for &(a, b) in &program.before {
        let (Some(&na), Some(&nb)) = (call.var_new.get(a as usize), call.var_new.get(b as usize))
        else {
            return Err(Outcome::Failed);
        };
        if let (Some(na), Some(nb)) = (na, nb) {
            edges.push((na, nb));
        }
    }

    // The active `randc` variables are drawn first, each from its own cycle
    // (LRM 18.4.2), so they leave the ordered groups. Their cycle states are
    // worked on as copies and committed only if the whole call succeeds.
    let mut randc_dense: Vec<u32> = Vec::new();
    let mut randc_keys: Vec<(u64, usize)> = Vec::new();
    let mut randc_work: Vec<RandcState> = Vec::new();
    for (dense, &i) in call.active_ids.iter().enumerate() {
        let v = &program.vars[i];
        if !v.randc {
            continue;
        }
        let Some(st) = objects::randc_state(call.var_owner[i], v.randc_key()) else {
            return Err(Outcome::DeadHandle);
        };
        randc_dense.push(dense as u32);
        randc_keys.push((call.var_owner[i], v.randc_key()));
        randc_work.push(st);
    }
    // Every `dist`'s weights, evaluated once, and its selector variable.
    let mut dist_weights = Vec::with_capacity(all_dists.len());
    for d in &all_dists {
        if d.subject.is_some() {
            dist_weights.push(Vec::new());
        } else {
            match d.weights(&states) {
                Ok(w) => dist_weights.push(w),
                Err(e) => return Err(outcome_of_dist(e, &null_state)),
            }
        }
        var_tys.push(d.selector_ty());
    }

    let mut values: Vec<BigUint> = vec![BigUint::zero(); n_real];
    let mut known: Vec<Option<BigUint>> = vec![None; n_real];
    for stage in 0..n_stages {
        let in_stage = |v: u32| {
            stage_of
                .get(v as usize)
                .is_some_and(|s| *s as usize == stage)
        };
        // This stage's constraints: the earlier stages' variables are fixed,
        // so they are constants, and a call over them is evaluated. A call
        // that is left is over this stage's own variables (one constraint
        // comparing results of calls): it is a check on each draw.
        let mut plain: Vec<Expr> = Vec::new();
        let mut checks: Vec<Expr> = Vec::new();
        for (c, _) in conjuncts
            .iter()
            .zip(&conj_stage)
            .filter(|(_, s)| **s == stage)
        {
            let mut c = c.clone();
            if has_calls {
                if stage > 0 {
                    c = c.substitute_vars(&mut |v, t| match known.get(v as usize) {
                        Some(Some(val)) => Expr::Const(t, val.clone()),
                        _ => Expr::Var(v, t),
                    });
                }
                c = func::fold_ground_calls(&c, &program.funcs, &states)
                    .map_err(|e| outcome_of_func(e, &null_state))?;
            }
            if func::has_call(&c) {
                checks.push(c);
                continue;
            }
            // Resolve the guards of implication / `if` constraints against
            // the state values (LRM 18.5.12); an ERROR guard fails the call.
            match guard::resolve(&c, &assignment) {
                Ok(r) => plain.push(r),
                Err(_) => return Err(Outcome::GuardError),
            }
        }

        let stage_edges: Vec<(u32, u32)> = edges
            .iter()
            .copied()
            .filter(|&(a, b)| in_stage(a) && in_stage(b))
            .collect();
        let Ok(groups) = order::groups(n_real, &stage_edges) else {
            return Err(Outcome::Failed);
        };
        // The stage's `randc` variables, as indices into the call's lists.
        let stage_randc: Vec<usize> = (0..randc_dense.len())
            .filter(|&k| in_stage(randc_dense[k]))
            .collect();
        let stage_randc_dense: Vec<u32> = stage_randc.iter().map(|&k| randc_dense[k]).collect();
        // One weighted selector per `dist`, drawn with the first group that
        // holds a variable of its subject (so the subject is still undrawn), or
        // with the last group when the subject has no active variable.
        let mut plan_groups: Vec<Group> = groups
            .into_iter()
            .map(|g| Group {
                vars: g
                    .into_iter()
                    .filter(|v| in_stage(*v) && !randc_dense.contains(v))
                    .collect(),
                weighted: Vec::new(),
            })
            .collect();
        let stage_dists: Vec<usize> = (0..all_dists.len())
            .filter(|&j| dist_stage[j] == stage && all_dists[j].subject.is_none())
            .collect();
        if !stage_dists.is_empty() && plan_groups.is_empty() {
            plan_groups.push(Group::default());
        }
        for &j in &stage_dists {
            let d = all_dists[j];
            // An instance's variables are the expansion's own dense ids.
            let dense = |v: u32| {
                if j >= n_prog_dists {
                    Some(v)
                } else {
                    call.var_new.get(v as usize).copied().flatten()
                }
            };
            let subject: Vec<u32> = d
                .vars
                .iter()
                .filter_map(|&v| dense(v))
                .filter(|&v| in_stage(v))
                .collect();
            let gi = plan_groups
                .iter()
                .position(|g| g.vars.iter().any(|v| subject.contains(v)))
                .unwrap_or(plan_groups.len() - 1);
            let measure = match (
                d.plain_var.and_then(dense).filter(|&v| in_stage(v)),
                subject.is_empty(),
            ) {
                (Some(s), _) => Measure::Distinct(s),
                (None, false) => Measure::Models,
                (None, true) => Measure::Flat,
            };
            plan_groups[gi].weighted.push(Weighted {
                var: (n_real + j) as u32,
                weights: dist_weights[j].clone(),
                measure,
            });
        }
        let plan = Plan {
            groups: plan_groups
                .into_iter()
                .filter(|g| !g.vars.is_empty() || !g.weighted.is_empty())
                .collect(),
            randc: stage_randc_dense,
        };

        let solver =
            Engine::new(&var_tys, &states, &plain).map_err(|e| outcome_of(e, &null_state))?;
        let mut tries = 0;
        let drawn = loop {
            let mut work: Vec<RandcState> =
                stage_randc.iter().map(|&k| randc_work[k].clone()).collect();
            let drawn = solver
                .sample_plan(&plan, &mut work, seed)
                .map_err(|e| outcome_of(e, &null_state))?;
            if checks_hold(&checks, &drawn, &program.funcs, &states, &null_state)? {
                for (&k, st) in stage_randc.iter().zip(work) {
                    randc_work[k] = st;
                }
                break drawn;
            }
            tries += 1;
            if tries >= MAX_CHECK_TRIES {
                return Err(Outcome::FunctionSearch);
            }
        };
        for v in 0..n_real {
            if in_stage(v as u32) {
                values[v] = drawn[v].clone();
                known[v] = Some(drawn[v].clone());
            }
        }
    }

    // The real variables are solved after the integral ones, from the same
    // PRNG stream (a class with none draws nothing here).
    let real_writes = run_real(
        program,
        call.h,
        call.rand_mode,
        call.statics,
        &states,
        &null_state,
        Some((&call.var_new, &values)),
        seed,
    )
    .inspect_err(|o| call.real_unsat.set(*o == Outcome::Unsatisfiable))?;
    Ok(Solution {
        values,
        randc_keys,
        randc_work,
        real_writes,
    })
}

/// What [`solve_all`] returns: the solution, the element variables, and the
/// size of every array.
type Solved = (Solution, Vec<(u32, usize)>, Vec<usize>, Vec<(u32, u32)>);

/// Solves the call's constraints `conjuncts` (no soft wrappers left): the
/// array sizes first, then the elements and the scalars for those sizes, trying
/// other sizes when the sizes drawn alone made the whole problem
/// unsatisfiable.
fn solve_all(call: &Call<'_>, conjuncts: &[Expr], seed: &mut u64) -> Result<Solved, Outcome> {
    if call.arrays.iter().any(|a| a.rows.is_some()) {
        return solve_all_rows(call, conjuncts, seed);
    }
    let n_active = call.var_tys.len() as u32;
    let mut blocked: Vec<Vec<usize>> = Vec::new();
    loop {
        let chosen = array::solve_sizes(
            conjuncts,
            &call.arrays,
            &call.var_tys,
            &call.states,
            &blocked,
            seed,
        )
        .map_err(|e| outcome_of_size(e, &call.null_state))?;
        let x = array::expand_with(
            conjuncts,
            &call.arrays,
            &chosen.sizes,
            n_active,
            &call.states,
            &call.program.funcs,
            &call.program.dists,
        )
        .map_err(|e| outcome_of_expand(e, &call.null_state))?;
        match solve_expanded(call, &x, seed) {
            Ok(s) => return Ok((s, x.elem_vars, chosen.sizes, Vec::new())),
            // The sizes were drawn without the element constraints, so they
            // may be what made the whole problem unsatisfiable: block them.
            Err(Outcome::Unsatisfiable) if !chosen.sized.is_empty() => {
                blocked.push(chosen.tuple);
                if blocked.len() >= array::MAX_SIZE_RETRIES {
                    return Err(Outcome::ArraySizeSearch);
                }
            }
            Err(o) => return Err(o),
        }
    }
}

/// [`solve_all`] for a program with an array of dynamic arrays or queues
/// (`rand int a[][]`, LRM 18.4): the sizes are solved in two stages, the outer
/// array's first, then those of the rows it has ([`array::lower_rows`]), and
/// every row is its own array of the expansion. A row-size tuple the
/// constraints cannot satisfy is blocked like an outer one.
fn solve_all_rows(call: &Call<'_>, conjuncts: &[Expr], seed: &mut u64) -> Result<Solved, Outcome> {
    let mut tries = 0usize;
    rows_stage(call, conjuncts, &call.arrays, &[], seed, &mut tries)
}

/// One stage of [`solve_all_rows`]: sizes the arrays of `arrays` that
/// constraints size, then either binds the rows of the arrays of arrays whose
/// rows are not bound yet (a row that is itself an array of arrays comes out
/// unbound and is sized by the next stage: `int a[][][]`) or, with every row
/// bound, expands and solves. A stage whose rows cannot be satisfied blocks
/// the size tuple it chose and tries another; `bases` are the row bases earlier
/// stages bound.
fn rows_stage(
    call: &Call<'_>,
    conjuncts: &[Expr],
    arrays: &[array::ArrayState],
    bases: &[(u32, u32)],
    seed: &mut u64,
    tries: &mut usize,
) -> Result<Solved, Outcome> {
    let n_active = call.var_tys.len() as u32;
    let mut blocked: Vec<Vec<usize>> = Vec::new();
    let unbound = arrays
        .iter()
        .any(|a| a.rows.as_ref().is_some_and(|r| !r.lowered));
    loop {
        *tries += 1;
        if *tries >= array::MAX_SIZE_RETRIES {
            return Err(Outcome::ArraySizeSearch);
        }
        let sz = array::solve_sizes(
            conjuncts,
            arrays,
            &call.var_tys,
            &call.states,
            &blocked,
            seed,
        )
        // No sizes fit (the stage above blocks the sizes it chose and retries).
        .map_err(|e| outcome_of_size(e, &call.null_state))?;
        let res = if unbound {
            let low = array::lower_rows(conjuncts, arrays, &sz.sizes, &call.states)
                .map_err(|e| outcome_of_expand(e, &call.null_state))?;
            let mut all = bases.to_vec();
            all.extend_from_slice(&low.bases);
            rows_stage(call, &low.conjuncts, &low.arrays, &all, seed, tries)
        } else {
            let x = array::expand_with(
                conjuncts,
                arrays,
                &sz.sizes,
                n_active,
                &call.states,
                &call.program.funcs,
                &call.program.dists,
            )
            .map_err(|e| outcome_of_expand(e, &call.null_state))?;
            solve_expanded(call, &x, seed)
                .map(|s| (s, x.elem_vars, sz.sizes.clone(), bases.to_vec()))
        };
        match res {
            Err(Outcome::Unsatisfiable) if !sz.sized.is_empty() => blocked.push(sz.tuple),
            other => return other,
        }
    }
}

/// Solves `program` for the object `h` and, on success, writes the result
/// (module docs). `rand_mode[i]` is whether property `i` is active; `statics`
/// are the `(id, handle)` pairs of the static-property objects the call site
/// reaches.
fn run(program: &Program, h: u64, rand_mode: &[bool], statics: &[(u32, u64)]) -> Outcome {
    // The constraint blocks `constraint_mode(0)` switched off (LRM 18.9) are
    // not part of this call, whatever they hold. A static block whose object
    // the call site did not pass cannot have been switched off through this
    // call's handle, so it stays on.
    let mut off: Vec<&ProgBlock> = Vec::new();
    for b in &program.blocks {
        let Ok(o) = owner(b.home, h, statics) else {
            continue;
        };
        match objects::constraint_mode_of(o, b.ordinal) {
            Some(true) => {}
            Some(false) => off.push(b),
            None => return Outcome::DeadHandle,
        }
    }
    if off.is_empty() {
        return run_blocks_on(program, h, rand_mode, statics);
    }
    match reduce::without_blocks(program, &off) {
        Ok(p) => run_blocks_on(&p, h, rand_mode, statics),
        Err(o) => o,
    }
}

/// [`run`] for a program none of whose blocks is switched off.
fn run_blocks_on(program: &Program, h: u64, rand_mode: &[bool], statics: &[(u32, u64)]) -> Outcome {
    let Some(seed0) = objects::prng_seed(h) else {
        return Outcome::DeadHandle;
    };
    let mut var_owner = Vec::with_capacity(program.vars.len());
    for v in &program.vars {
        match owner(v.home, h, statics) {
            Ok(o) => var_owner.push(o),
            Err(o) => return o,
        }
    }
    let mut state_owner = Vec::with_capacity(program.states.len());
    for s in &program.states {
        match owner(s.home, h, statics) {
            Ok(o) => state_owner.push(o),
            Err(o) => return o,
        }
    }
    let mut array_owner = Vec::with_capacity(program.arrays.len());
    for a in &program.arrays {
        match owner(a.home, h, statics) {
            Ok(o) => array_owner.push(o),
            Err(o) => return o,
        }
    }
    let active = |v: &ProgVar| match v.prop_index {
        Some(i) => rand_mode.get(i).copied(),
        None => Some(true),
    };
    // Dense renumbering of the active variables; inactive ones become extra
    // state variables after the program's own, read like any other state.
    let mut var_new: Vec<Option<u32>> = Vec::with_capacity(program.vars.len());
    let mut var_tys: Vec<Ty> = Vec::new();
    let mut active_ids: Vec<usize> = Vec::new();
    let mut inactive_state: Vec<Option<u32>> = Vec::with_capacity(program.vars.len());
    let mut inactive_ids: Vec<usize> = Vec::new();
    for (i, v) in program.vars.iter().enumerate() {
        match active(v) {
            None => return Outcome::Failed,
            Some(true) => {
                var_new.push(Some(var_tys.len() as u32));
                inactive_state.push(None);
                var_tys.push(v.ty);
                active_ids.push(i);
            }
            Some(false) => {
                var_new.push(None);
                inactive_state.push(Some((program.states.len() + inactive_ids.len()) as u32));
                inactive_ids.push(i);
            }
        }
    }

    let mut states: Vec<Option<BigUint>> = Vec::with_capacity(program.states.len());
    let mut null_state: Vec<bool> = Vec::with_capacity(program.states.len());
    for (s, &o) in program.states.iter().zip(&state_owner) {
        match read_state(o, s) {
            Ok(Reading::Value(v)) => {
                states.push(v);
                null_state.push(false);
            }
            Ok(Reading::NullHandle) => {
                states.push(None);
                null_state.push(true);
            }
            Err(o) => return o,
        }
    }
    for &i in &inactive_ids {
        let v = &program.vars[i];
        match read(var_owner[i], v.slot, v.window, v.ty) {
            Ok(x) => states.push(x),
            Err(o) => return o,
        }
        null_state.push(false);
    }
    let mut arrays = Vec::with_capacity(program.arrays.len());
    for (a, &o) in program.arrays.iter().zip(&array_owner) {
        let on = a.rand
            && match a.prop_index {
                Some(i) => match rand_mode.get(i) {
                    Some(&b) => b,
                    None => return Outcome::Failed,
                },
                None => true,
            };
        match read_array(a, o, on) {
            Ok(s) => arrays.push(s),
            Err(o) => return o,
        }
    }
    // Tell each array of arrays which array stands for its rows.
    // A template's `template_of` names the array it is the row template of; a
    // deeper level's names the template above it, so the chain leads to the
    // array that holds the rows.
    for t in 0..arrays.len() {
        let Some(mut o) = arrays[t].template_of else {
            continue;
        };
        let mut level = 0;
        while let Some(up) = arrays.get(o as usize).and_then(|a| a.template_of) {
            o = up;
            level += 1;
        }
        if let Some(rows) = arrays.get_mut(o as usize).and_then(|a| a.rows.as_mut()) {
            rows.set_template(level, t as u32);
        }
    }

    // The conjuncts left out of this call: the enum-domain constraint of an
    // inactive variable (LRM 18.8: it is state, not a random variable).
    let mut dropped = vec![false; program.conjuncts.len()];
    for &i in &inactive_ids {
        if let Some(d) = program.vars[i].domain_conjunct {
            match dropped.get_mut(d) {
                Some(slot) => *slot = true,
                None => return Outcome::Failed,
            }
        }
    }
    let call = Call {
        program,
        h,
        rand_mode,
        statics,
        var_owner,
        var_new,
        var_tys,
        active_ids,
        arrays,
        array_owner,
        states,
        null_state,
        real_unsat: std::cell::Cell::new(false),
    };

    // The constraints one choice of discarded soft constraints leaves: the
    // soft wrappers resolved (module docs of [`super::priority`]), the field
    // variables renumbered densely (the dists' selector variables are
    // renumbered once the element variables exist), and every call whose
    // arguments are all fixed (state, constants) evaluated now (LRM 18.5.11:
    // calls are evaluated before solving), so a size constraint or an index
    // may read its result.
    let has_softs = !program.softs.is_empty();
    let prepare = |discard: &[bool]| -> Result<Vec<Expr>, Outcome> {
        let mut out = Vec::with_capacity(program.conjuncts.len());
        for (i, c) in program.conjuncts.iter().enumerate() {
            if dropped[i] {
                continue;
            }
            let resolved;
            let c = if has_softs {
                resolved = priority::resolve_softs(c, discard).map_err(|_| Outcome::Failed)?;
                &resolved
            } else {
                c
            };
            let c = c.substitute_vars(&mut |v, t| {
                if v >= SELECTOR_BASE {
                    return Expr::Var(v, t);
                }
                match (call.var_new[v as usize], inactive_state[v as usize]) {
                    (Some(n), _) => Expr::Var(n, t),
                    (None, Some(s)) => Expr::State(s, t),
                    (None, None) => unreachable!("every variable is active or inactive"),
                }
            });
            out.push(if program.funcs.is_empty() {
                c
            } else {
                func::fold_ground_calls(&c, &program.funcs, &call.states)
                    .map_err(|e| outcome_of_func(e, &call.null_state))?
            });
        }
        Ok(out)
    };

    let mut seed = seed0;
    let solved = if has_softs {
        // Whether the problem has a solution is what a soft constraint trades
        // against; every other outcome is the call's.
        priority::solve_relaxing(
            &program.softs,
            &mut seed,
            |discard, seed| solve_all(&call, &prepare(discard)?, seed),
            |o| matches!(o, Outcome::Unsatisfiable | Outcome::ArraySizeSearch),
        )
    } else {
        prepare(&[]).and_then(|c| solve_all(&call, &c, &mut seed))
    };
    let (solution, elem_vars, sizes, row_bases) = match solved {
        Ok(s) => s,
        Err(o) => return o,
    };

    // Pack everything first so a layout mismatch writes nothing at all.
    let mut writes = solution.real_writes;
    writes.reserve(call.active_ids.len());
    for (k, &i) in call.active_ids.iter().enumerate() {
        let v = &program.vars[i];
        match Write::new(call.var_owner[i], v.slot, v.window, &solution.values[k]) {
            Some(w) => writes.push(w),
            None => return Outcome::Failed,
        }
    }
    // Each active array's new contents, element words flat.
    let mut new_arrays: Vec<(usize, Vec<u64>)> = Vec::new();
    for (ai, a) in call.arrays.iter().enumerate() {
        if !a.active {
            continue;
        }
        let ew = program.arrays[ai].elem_words;
        if program.arrays[ai].nested {
            // One new row collection per row (and per row of a row, for an
            // array nested deeper); the outer holds their handles.
            let mut out = RowWriter {
                pa: &program.arrays[ai],
                elem_vars: &elem_vars,
                values: &solution.values[call.active_ids.len()..],
                bases: &row_bases,
                sizes: &sizes,
                made: Vec::new(),
            };
            match out.elements(ai as u32, program.arrays[ai].row_depth.max(1)) {
                Some(flat) => new_arrays.push((ai, flat)),
                None => {
                    out.made.iter().for_each(|&h| collections::release(h));
                    return Outcome::Failed;
                }
            }
            continue;
        }
        let mut flat = Vec::with_capacity(sizes[ai] * ew);
        for (e, &(arr, _)) in elem_vars.iter().enumerate() {
            if arr as usize != ai {
                continue;
            }
            match pack(&solution.values[call.active_ids.len() + e], ew) {
                Some(w) => flat.extend(w),
                None => return Outcome::Failed,
            }
        }
        new_arrays.push((ai, flat));
    }
    for w in writes {
        if !w.apply() {
            return Outcome::DeadHandle;
        }
    }
    for (ai, flat) in new_arrays {
        let pa = &program.arrays[ai];
        let o = call.array_owner[ai];
        let (old_h, _) = match read_unknown(o, pa.slot, pa.window, 64) {
            Ok(x) => x,
            Err(o) => return o,
        };
        let new = if pa.nested {
            // The outer's elements are the rows themselves (inline) or their
            // handles built above; the old rows are not owned by the outer and
            // stay alive.
            let shape = collections::Shape {
                elem_words: row_elem_words(pa, pa.row_depth.max(1)),
                assoc: false,
                key: collections::KeyKind::Int {
                    width: 32,
                    signed: false,
                },
                obj: false,
                nested: collections::Nested::NONE,
            };
            collections::from_words(&shape, &flat)
        } else if pa.assoc {
            // Same keys, new values: an associative array is never resized.
            match collections::map_with_values(old_h.to_u64().unwrap_or(0), pa.elem_words, &flat) {
                Some(h) => h,
                None => return Outcome::Failed,
            }
        } else {
            let shape = collections::Shape {
                elem_words: pa.elem_words,
                assoc: false,
                key: collections::KeyKind::Int {
                    width: 32,
                    signed: false,
                },
                obj: false,
                nested: collections::Nested::NONE,
            };
            collections::from_words(&shape, &flat)
        };
        let Some(w) = Write::new(o, pa.slot, pa.window, &BigUint::from(new)) else {
            collections::release(new);
            return Outcome::Failed;
        };
        if !w.apply() {
            collections::release(new);
            return Outcome::DeadHandle;
        }
        collections::release(old_h.to_u64().unwrap_or(0));
    }
    for ((o, offset), st) in solution.randc_keys.into_iter().zip(solution.randc_work) {
        if !objects::set_randc_states(o, vec![(offset, st)]) {
            return Outcome::DeadHandle;
        }
    }
    objects::set_prng_seed(h, seed);
    Outcome::Solved
}

/// The words of one element of a collection whose elements are rows `levels`
/// levels above the leaves: a row handle (2 words) or, for the innermost level
/// of an array whose last dimension is fixed, the row's elements inline
/// (`int a[][4]`, LRM 1800-2023 7.4, 7.5).
fn row_elem_words(pa: &ProgArray, levels: u32) -> usize {
    if levels == 1 && pa.inner_fixed > 0 {
        (2 * pa.inner_fixed as usize * pa.elem_ty.width as usize)
            .div_ceil(64)
            .max(1)
    } else {
        2
    }
}

/// Builds the new collections of one array of arrays from a solution.
struct RowWriter<'a> {
    pa: &'a ProgArray,
    elem_vars: &'a [(u32, usize)],
    /// The value of each element variable.
    values: &'a [BigUint],
    /// `(array of arrays, the array standing for its row 0)` of every stage.
    bases: &'a [(u32, u32)],
    sizes: &'a [usize],
    /// The collections made so far (released if the write fails).
    made: Vec<u64>,
}

impl RowWriter<'_> {
    fn base(&self, arr: u32) -> Option<u32> {
        self.bases.iter().find(|&&(o, _)| o == arr).map(|&(_, b)| b)
    }

    fn shape(elem_words: usize) -> collections::Shape {
        collections::Shape {
            elem_words,
            assoc: false,
            key: collections::KeyKind::Int {
                width: 32,
                signed: false,
            },
            obj: false,
            nested: collections::Nested::NONE,
        }
    }

    /// The element words of the collection standing for `arr`, whose rows
    /// are `levels` levels above the leaves.
    fn elements(&mut self, arr: u32, levels: u32) -> Option<Vec<u64>> {
        let base = self.base(arr)?;
        let mut out = Vec::new();
        for k in 0..*self.sizes.get(arr as usize)? {
            let row = base + k as u32;
            if levels > 1 {
                let words = self.elements(row, levels - 1)?;
                let h = collections::from_words(
                    &Self::shape(row_elem_words(self.pa, levels - 1)),
                    &words,
                );
                self.made.push(h);
                out.extend(pack(&BigUint::from(h), 2)?);
            } else if self.pa.inner_fixed > 0 {
                // The row is stored inline: `inner_fixed` leaf elements in one
                // flat value, lowest index first. The constraints pin every
                // row to that many.
                let n = self.pa.inner_fixed as usize;
                let w = self.pa.elem_ty.width as usize;
                let mut val = BigUint::zero();
                let mut count = 0usize;
                for (e, &(a, _)) in self.elem_vars.iter().enumerate() {
                    if a == row {
                        val |= &self.values[e] << (count * w);
                        count += 1;
                    }
                }
                if count != n {
                    return None;
                }
                out.extend(pack(&val, row_elem_words(self.pa, 1))?);
            } else {
                let ew = self.pa.elem_words;
                let mut flat = Vec::new();
                for (e, &(a, _)) in self.elem_vars.iter().enumerate() {
                    if a == row {
                        flat.extend(pack(&self.values[e], ew)?);
                    }
                }
                let h = collections::from_words(&Self::shape(ew), &flat);
                self.made.push(h);
                out.extend(pack(&BigUint::from(h), 2)?);
            }
        }
        Some(out)
    }
}

/// One local variable an inline constraint reads (LRM 18.7): its value is
/// taken when the call is made and is a constant of the solve.
#[derive(Clone, Copy, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct Capture {
    /// The fragment state that stands for the local ([`Spec::frag`]).
    pub state: u32,
    /// Its bit width.
    pub width: u32,
}

impl Capture {
    /// How many 64-bit words the call site passes for it: the 4-state packed
    /// value, as everywhere in the object store.
    pub fn words(&self) -> usize {
        (2 * self.width as usize).div_ceil(64).max(1)
    }
}

/// Where one property a `randomize(v, ...)` argument list names lives (LRM
/// 18.11), in the same terms a [`Program`] locates its variables.
#[derive(Clone, Copy, Debug, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct Target {
    /// The object the property is a field of.
    pub home: Home,
    /// The property.
    pub slot: FieldSlot,
    /// The leaf of an unpacked aggregate property it names, or `None` for the
    /// whole property (every leaf of it, for an aggregate).
    pub window: Option<Window>,
}

/// What one `randomize(...)` call site adds to its class's constraints: the
/// inline constraints of `with {}` (C19), the argument list of `randomize(v,
/// ...)` / `randomize(null)` (C20). Built by the compiler once per call site and
/// registered ([`register_spec`]); the call passes only its id and the values of
/// the locals it captured.
#[derive(Clone, Debug, Default, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub struct Spec {
    /// The inline constraints, as a [`Program`] over the receiver's *static*
    /// class: its variables, arrays and states name properties by where they
    /// live, so [`joint::overlay`] lays it over the program of whatever dynamic
    /// class the receiver turns out to be. No constraint blocks of the class
    /// are in it.
    pub frag: Program,
    /// The locals the fragment reads, in the order their words follow the
    /// static-property pairs in the call's buffer.
    pub captures: Vec<Capture>,
    /// `Some(list)`: the complete set of random variables of the call (LRM
    /// 18.11); everything else is state. `Some(vec![])` is `randomize(null)`,
    /// a checker. `None`: the object's own `rand` variables, as `rand_mode`
    /// leaves them.
    pub only: Option<Vec<Target>>,
}

impl Spec {
    /// How many words of captured values a call to this spec passes.
    pub fn capture_words(&self) -> usize {
        self.captures.iter().map(Capture::words).sum()
    }

    /// For a scope randomize ([`randomize_scope`]): how many words the solved
    /// variables occupy, the extent of the scratch area [`Self::frag`] lays them
    /// out in.
    pub fn scope_words(&self) -> usize {
        let ints = self.frag.vars.iter().map(|v| v.slot.offset + v.slot.words);
        let reals = self
            .frag
            .real_vars
            .iter()
            .map(|v| v.slot.offset + v.slot.words);
        // a queue / dynamic array of the call keeps its handle in one word
        let arrays = self
            .frag
            .arrays
            .iter()
            .map(|v| v.slot.offset + v.slot.words);
        ints.chain(reals).chain(arrays).max().unwrap_or(0)
    }
}

type SpecTable = HashMap<u32, Arc<Spec>>;

fn specs() -> &'static Mutex<SpecTable> {
    static T: OnceLock<Mutex<SpecTable>> = OnceLock::new();
    T.get_or_init(|| Mutex::new(HashMap::new()))
}

/// The next id [`register_spec`] hands out.
static NEXT_SPEC: AtomicU32 = AtomicU32::new(1);

/// Registers `spec` and returns its id (`1..`; `0` is "no spec", a plain
/// `obj.randomize()`).
pub fn register_spec(spec: Spec) -> u32 {
    let id = NEXT_SPEC.fetch_add(1, Ordering::Relaxed);
    specs()
        .lock()
        .unwrap_or_else(|e| e.into_inner())
        .insert(id, Arc::new(spec));
    id
}

/// Registers `spec` under the id it had in the process that built a design
/// image ([`wire::preload`]): the id is baked into the machine code of the
/// call site, so the runner must not mint its own. Later [`register_spec`]
/// calls continue above it.
pub(super) fn register_spec_at(id: u32, spec: Spec) {
    NEXT_SPEC.fetch_max(id + 1, Ordering::Relaxed);
    specs()
        .lock()
        .unwrap_or_else(|e| e.into_inner())
        .insert(id, Arc::new(spec));
}

/// Every registered spec, ascending by id (a hash table has no order of its
/// own, and a design image must encode deterministically).
pub(super) fn all_specs() -> Vec<(u32, Arc<Spec>)> {
    let mut v: Vec<_> = specs()
        .lock()
        .unwrap_or_else(|e| e.into_inner())
        .iter()
        .map(|(&id, s)| (id, Arc::clone(s)))
        .collect();
    v.sort_by_key(|(id, _)| *id);
    v
}

/// The spec registered under `id`.
pub fn spec(id: u32) -> Option<Arc<Spec>> {
    specs()
        .lock()
        .unwrap_or_else(|e| e.into_inner())
        .get(&id)
        .cloned()
}

/// How many specs this process has registered: a design whose `randomize()`
/// call sites registered one carries solver state that exists only here.
pub fn spec_count() -> usize {
    specs().lock().unwrap_or_else(|e| e.into_inner()).len()
}

static OBJECT_SITES: AtomicU32 = AtomicU32::new(0);

/// Records that an `obj.randomize()` call site was lowered: it reads the class
/// programs registered with [`register_program`], which exist only in the
/// process that lowered the design.
pub fn note_object_site() {
    OBJECT_SITES.fetch_add(1, Ordering::Relaxed);
}

/// How many `obj.randomize()` call sites this process has lowered
/// ([`note_object_site`]).
pub fn object_site_count() -> u32 {
    OBJECT_SITES.load(Ordering::Relaxed)
}

/// How many words of captured values a call of spec `id` passes (`0` for no spec
/// or an unknown id).
pub fn spec_capture_words(id: u32) -> usize {
    spec(id).map_or(0, |s| s.capture_words())
}

/// The captured values `words` (packed per [`Capture::words`]) as the constants
/// of the fragment's states. An unknown (X/Z) bit in a captured local is a
/// [`Outcome::StateUnknown`]: a 4-state value in a constraint is an error (LRM
/// 18.3), and the local was named by the constraint.
fn capture_consts(spec: &Spec, words: &[u64]) -> Result<Vec<Option<BigUint>>, Outcome> {
    let mut consts: Vec<Option<BigUint>> = vec![None; spec.frag.states.len()];
    let mut at = 0;
    for c in &spec.captures {
        let n = c.words();
        let chunk = words.get(at..at + n).ok_or(Outcome::Failed)?;
        at += n;
        let (val, unk) = unpack(chunk, c.width);
        if !unk.is_zero() {
            return Err(Outcome::StateUnknown);
        }
        *consts.get_mut(c.state as usize).ok_or(Outcome::Failed)? = Some(val);
    }
    Ok(consts)
}

/// `obj.constraint_mode(on)` with no block named (LRM 18.9): every non-`static`
/// constraint block of `h`'s dynamic class. The `static` blocks live in the
/// class's static-property object, one per class, so the call site addresses
/// those itself. `Outcome::DeadHandle` for a null or stale `h`,
/// `Outcome::NoProgram` for a class whose program could not be built.
pub fn set_all_constraint_modes(h: u64, on: bool) -> Outcome {
    let Some(template) = objects::dynamic_template(h) else {
        return Outcome::DeadHandle;
    };
    let Some(entry) = program(template) else {
        return Outcome::NoProgram;
    };
    let Ok(prog) = entry.as_ref() else {
        return Outcome::NoProgram;
    };
    for b in prog.blocks.iter().filter(|b| b.home == Home::Instance) {
        if !objects::set_constraint_mode_of(h, b.ordinal, on) {
            return Outcome::DeadHandle;
        }
    }
    Outcome::Solved
}

/// `obj.randomize()` for the object `h` (module docs); `statics` are the
/// `(id, handle)` pairs of the static-property objects the call site reaches
/// ([`Home::Static`]).
pub fn randomize(h: u64, statics: &[(u32, u64)]) -> Outcome {
    randomize_spec(h, statics, 0, &[])
}

/// `obj.randomize(...)` with the additions of spec `spec_id` (`0`: none);
/// `captures` are the packed values of the locals it captured
/// ([`Spec::captures`]).
pub fn randomize_spec(h: u64, statics: &[(u32, u64)], spec_id: u32, captures: &[u64]) -> Outcome {
    let Some(template) = objects::dynamic_template(h) else {
        return Outcome::DeadHandle;
    };
    let Some(base) = program(template) else {
        return Outcome::NoProgram;
    };
    let Ok(base_prog) = base.as_ref() else {
        return Outcome::NoProgram;
    };
    let Some(meta) = objects::rand_meta(h) else {
        return Outcome::DeadHandle;
    };
    let mut rand_mode = meta.rand_mode;
    let entry = if spec_id == 0 {
        base.clone()
    } else {
        let Some(spec) = spec(spec_id) else {
            return Outcome::Failed;
        };
        let consts = match capture_consts(&spec, captures) {
            Ok(c) => c,
            Err(o) => return o,
        };
        let mut p = match joint::overlay(base_prog, &spec.frag, &consts) {
            Ok(p) => p,
            Err(o) => return o,
        };
        if let Some(only) = &spec.only
            && let Err(o) = joint::restrict(&mut p, &mut rand_mode, only)
        {
            return o;
        }
        Arc::new(Ok(p))
    };
    let Ok(prog) = entry.as_ref() else {
        return Outcome::NoProgram;
    };
    // An element switched off alone with `obj.a[i].rand_mode(0)` is state.
    let entry = match joint::apply_leaf_modes(prog, &mut rand_mode, &meta.leaf_off, &meta.leaf_on) {
        Some(p) => Arc::new(Ok(p)),
        None => entry,
    };
    let Ok(prog) = entry.as_ref() else {
        return Outcome::NoProgram;
    };
    // A `static` variable switched off with `rand_mode(0)` (through any
    // instance, LRM 18.8) is state for this call.
    let entry = match joint::apply_static_modes(prog, &mut rand_mode, statics) {
        Some(p) => Arc::new(Ok(p)),
        None => entry,
    };
    let Ok(prog) = entry.as_ref() else {
        return Outcome::NoProgram;
    };
    // The objects randomized together with `h` (LRM 18.5.8): `h` alone unless
    // it holds an active, non-null `rand` object member.
    let closure = match joint::closure(h, &entry, &rand_mode, statics) {
        Ok(c) => c,
        Err(o) => return o,
    };
    if closure.members.len() == 1 {
        // A handle that leads back to `h` (`me.x`) reads one of its own
        // random variables; only the merge turns that read into the variable.
        match joint::self_alias(&closure, prog, statics) {
            Ok(joint::SelfAlias::None) => return run(prog, h, &rand_mode, statics),
            Ok(joint::SelfAlias::Integral) => {}
            Err(o) => return o,
        }
    }
    match joint::merge(&closure, statics) {
        Ok(m) => run(&m.program, h, &m.rand_mode, statics),
        Err(o) => o,
    }
}

/// The template of the scratch object a scope randomize solves in: it has no
/// class, no `rand` properties and no program, only field storage for the
/// variables (see [`randomize_scope`]).
const SCOPE_TEMPLATE: ClassTemplateId = ClassTemplateId(u32::MAX - 1);

/// `std::randomize(v, ...)` (LRM 1800-2023 18.12): solves the spec `spec_id`
/// registered for the call site. Its variables belong to no object: the spec's
/// fragment places variable `i` at words of a scratch area, which is solved in
/// a temporary object and copied to `out` only when the solve succeeds (18.6.1:
/// a failed call changes nothing). `captures` are the packed values of the
/// locals the constraint block reads, as for [`randomize_spec`]; `seed` is the
/// state of the generator the draw uses (the calling process's, LRM 18.13).
/// With no variable the call is a checker (18.12): nothing is drawn or
/// written, and [`Outcome::Solved`] means every constraint held.
pub fn randomize_scope(spec_id: u32, captures: &[u64], out: &mut [u64], seed: u64) -> Outcome {
    let Some(spec) = spec(spec_id) else {
        return Outcome::Failed;
    };
    // a call site whose buffers do not match its spec is a compiler bug
    if out.len() != spec.scope_words() || captures.len() != spec.capture_words() {
        return Outcome::Failed;
    }
    let consts = match capture_consts(&spec, captures) {
        Ok(c) => c,
        Err(o) => return o,
    };
    let prog = match joint::overlay(&Program::default(), &spec.frag, &consts) {
        Ok(p) => p,
        Err(o) => return o,
    };
    let h = objects::alloc(SCOPE_TEMPLATE, out.len());
    objects::set_prng_seed(h, seed);
    let slot = FieldSlot {
        offset: 0,
        words: out.len(),
    };
    // The caller's current values go in first: an aggregate's non-random
    // members (a `string`) are not solved and must come back unchanged.
    if !out.is_empty() && !objects::field_set(h, slot, out) {
        objects::release(h);
        return Outcome::Failed;
    }
    let outcome = run(&prog, h, &[], &[]);
    if outcome == Outcome::Solved && !out.is_empty() && !objects::field_get(h, slot, out) {
        objects::release(h);
        return Outcome::Failed;
    }
    objects::release(h);
    outcome
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::constraints::ir::BinOp;
    use crate::objects::{RandKind, RandProp, alloc, register_rand_props, release};

    pub(super) fn u(w: u32) -> Ty {
        Ty::unsigned(w)
    }
    pub(super) fn var(i: u32, t: Ty) -> Expr {
        Expr::Var(i, t)
    }
    pub(super) fn k(t: Ty, v: u64) -> Expr {
        Expr::constant(t, v)
    }
    pub(super) fn bin(op: BinOp, a: Expr, b: Expr, t: Ty) -> Expr {
        Expr::Binary(op, Box::new(a), Box::new(b), t)
    }

    /// `randomize` on a call site that reaches no static-property object.
    fn randomize(h: u64) -> Outcome {
        super::randomize(h, &[])
    }

    /// Each test uses its own template id: the registries are process-wide
    /// and `cargo test` is concurrent. A template has `n` 8-bit rand fields
    /// (`x0`, `x1`, ...) at words `0..n`, then one 8-bit state field `s` at
    /// word `n`.
    pub(super) fn setup(id: u32, n: usize, conjuncts: Vec<Expr>) -> (ClassTemplateId, u64) {
        setup_with_softs(id, n, conjuncts, Vec::new())
    }

    fn setup_with_softs(
        id: u32,
        n: usize,
        conjuncts: Vec<Expr>,
        softs: Vec<Soft>,
    ) -> (ClassTemplateId, u64) {
        let t = ClassTemplateId(id);
        let vars = (0..n)
            .map(|i| ProgVar {
                ty: u(8),
                slot: FieldSlot {
                    offset: i,
                    words: 1,
                },
                home: Home::Instance,
                prop_index: Some(i),
                domain_conjunct: None,
                randc: false,
                window: None,
            })
            .collect();
        register_rand_props(
            t,
            (0..n)
                .map(|i| RandProp {
                    slot: FieldSlot {
                        offset: i,
                        words: 1,
                    },
                    kind: RandKind::Rand,
                })
                .collect(),
        );
        register_program(
            t,
            Ok(Program {
                vars,
                states: vec![ProgState {
                    class_of: false,
                    root_bit: 0,
                    ty: u(8),
                    slot: FieldSlot {
                        offset: n,
                        words: 1,
                    },
                    window: None,
                    home: Home::Instance,
                    via: Vec::new(),
                }],
                conjuncts,
                before: Vec::new(),
                dists: Vec::new(),
                softs,
                ..Program::default()
            }),
        );
        let h = alloc(t, n + 1);
        objects::set_prng_seed(h, 0x1234_5678);
        (t, h)
    }

    /// A soft constraint on `x0` at priority `seq` (later is higher).
    fn soft_on_x0(seq: u32) -> Soft {
        Soft {
            priority: priority::Priority {
                object: 0,
                level: 0,
                seq,
            },
            dists: Vec::new(),
            keys: vec![priority::SoftKey::Var(0)],
            disabled: false,
            disabled_by: Vec::new(),
        }
    }

    #[test]
    fn soft_constraints_hold_unless_a_hard_or_higher_soft_conflicts() {
        // soft x0 == 5 (low), soft x0 == 6 (high): the higher one wins.
        let eq = |v: u64| bin(BinOp::Eq, var(0, u(8)), k(u(8), v), Ty::BIT);
        let c = vec![priority::wrap_soft(0, eq(5)), priority::wrap_soft(1, eq(6))];
        let (_, h) = setup_with_softs(0x7000_0f01, 1, c, vec![soft_on_x0(0), soft_on_x0(1)]);
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!(get(h, 0), 6);
        }
        release(h);

        // A hard x0 in [1, 3] discards both; the result is still random over the hard range.
        let c = vec![
            bin(BinOp::Ge, var(0, u(8)), k(u(8), 1), Ty::BIT),
            bin(BinOp::Le, var(0, u(8)), k(u(8), 3), Ty::BIT),
            priority::wrap_soft(0, eq(5)),
            priority::wrap_soft(1, eq(6)),
        ];
        let (_, h) = setup_with_softs(0x7000_0f02, 1, c, vec![soft_on_x0(0), soft_on_x0(1)]);
        let mut seen = std::collections::BTreeSet::new();
        for _ in 0..100 {
            assert_eq!(randomize(h), Outcome::Solved);
            seen.insert(get(h, 0));
        }
        assert_eq!(seen.len(), 3, "{seen:?}");
        release(h);

        // A hard contradiction stays a failure whatever the softs say.
        let c = vec![
            bin(BinOp::Gt, var(0, u(8)), k(u(8), 5), Ty::BIT),
            bin(BinOp::Lt, var(0, u(8)), k(u(8), 3), Ty::BIT),
            priority::wrap_soft(0, eq(4)),
        ];
        let (_, h) = setup_with_softs(0x7000_0f03, 1, c, vec![soft_on_x0(0)]);
        set(h, 0, 0x42);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        assert_eq!(get(h, 0), 0x42, "a failed randomize writes nothing");
        release(h);
    }

    pub(super) fn get(h: u64, off: usize) -> u64 {
        let mut b = [0u64];
        assert!(objects::field_get(
            h,
            FieldSlot {
                offset: off,
                words: 1
            },
            &mut b
        ));
        b[0]
    }
    fn set(h: u64, off: usize, v: u64) {
        assert!(objects::field_set(
            h,
            FieldSlot {
                offset: off,
                words: 1
            },
            &[v]
        ));
    }

    #[test]
    fn solves_writes_two_state_values_and_advances_the_seed() {
        // x0 in [10, 12].
        let c = vec![
            bin(BinOp::Ge, var(0, u(8)), k(u(8), 10), Ty::BIT),
            bin(BinOp::Le, var(0, u(8)), k(u(8), 12), Ty::BIT),
        ];
        let (_, h) = setup(0x7000_0001, 1, c);
        let before = objects::prng_seed(h);
        let mut seen = std::collections::BTreeSet::new();
        for _ in 0..200 {
            assert_eq!(randomize(h), Outcome::Solved);
            let v = get(h, 0);
            assert!((10..=12).contains(&v), "{v}");
            seen.insert(v);
        }
        assert_eq!(seen.len(), 3, "all three legal values are reachable");
        assert_ne!(objects::prng_seed(h), before);
        release(h);
    }

    #[test]
    fn failure_writes_nothing_and_consumes_no_draws() {
        // x0 > 5 && x0 < 3 is unsatisfiable.
        let c = vec![
            bin(BinOp::Gt, var(0, u(8)), k(u(8), 5), Ty::BIT),
            bin(BinOp::Lt, var(0, u(8)), k(u(8), 3), Ty::BIT),
        ];
        let (_, h) = setup(0x7000_0002, 2, c);
        set(h, 0, 0x77);
        set(h, 1, 0x88);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        assert_eq!((get(h, 0), get(h, 1)), (0x77, 0x88), "values unchanged");
        assert_eq!(objects::prng_seed(h), seed, "stream not perturbed");
        release(h);
    }

    #[test]
    fn determinism_by_seed() {
        let (_, a) = setup(0x7000_0003, 2, vec![]);
        let b = alloc(ClassTemplateId(0x7000_0003), 3);
        objects::set_prng_seed(b, 0x1234_5678);
        for _ in 0..5 {
            assert_eq!(randomize(a), Outcome::Solved);
            assert_eq!(randomize(b), Outcome::Solved);
            assert_eq!((get(a, 0), get(a, 1)), (get(b, 0), get(b, 1)));
        }
        objects::set_prng_seed(b, 99);
        let mut diff = false;
        for _ in 0..8 {
            randomize(a);
            randomize(b);
            diff |= get(a, 0) != get(b, 0);
        }
        assert!(diff, "different seeds give different streams");
        release(a);
        release(b);
    }

    #[test]
    fn rand_mode_off_variable_is_state_not_solved() {
        // x0 + x1 == 100 with x0 inactive at 30: x1 must be 70, x0 untouched.
        let c = vec![bin(
            BinOp::Eq,
            bin(BinOp::Add, var(0, u(8)), var(1, u(8)), u(8)),
            k(u(8), 100),
            Ty::BIT,
        )];
        let (_, h) = setup(0x7000_0004, 2, c);
        set(h, 0, 30);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!((get(h, 0), get(h, 1)), (30, 70));
        }
        // An inactive variable pinned outside the constraint makes the
        // problem unsatisfiable: with nothing left to solve it is a checker.
        let c2 = vec![bin(BinOp::Lt, var(0, u(8)), k(u(8), 10), Ty::BIT)];
        let (_, h2) = setup(0x7000_0005, 1, c2);
        set(h2, 0, 200);
        let mut m = objects::rand_meta(h2).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h2, m);
        assert_eq!(randomize(h2), Outcome::Unsatisfiable, "acts as a checker");
        assert_eq!(get(h2, 0), 200);
        release(h);
        release(h2);
    }

    #[test]
    fn all_variables_inactive_checks_the_constraints() {
        let c = vec![bin(BinOp::Eq, var(0, u(8)), k(u(8), 5), Ty::BIT)];
        let (_, h) = setup(0x7000_0006, 1, c);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        set(h, 0, 5);
        assert_eq!(randomize(h), Outcome::Solved);
        set(h, 0, 6);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        release(h);
    }

    /// XC-059: one property (word 0, a 24-bit value then its 24 unknown bits)
    /// holding three byte leaves: `lo` (bit 0) and `hi` (bit 16) are solved
    /// (`lo` in 10..=12, `hi == lo + 1`) or read as state, and the middle byte
    /// (X-filled) is never touched.
    fn windowed(id: u32, randc_hi: bool) -> (ClassTemplateId, u64) {
        let t = ClassTemplateId(id);
        let slot = FieldSlot {
            offset: 0,
            words: 1,
        };
        register_rand_props(
            t,
            vec![RandProp {
                slot,
                kind: RandKind::Rand,
            }],
        );
        let leaf = |bit| {
            Some(Window {
                bit,
                width: 8,
                field_width: 24,
            })
        };
        let c = vec![
            bin(BinOp::Ge, var(0, u(8)), k(u(8), 10), Ty::BIT),
            bin(BinOp::Le, var(0, u(8)), k(u(8), 12), Ty::BIT),
            bin(
                BinOp::Eq,
                var(1, u(8)),
                bin(BinOp::Add, var(0, u(8)), k(u(8), 1), u(8)),
                Ty::BIT,
            ),
        ];
        let mk = |bit, randc| ProgVar {
            ty: u(8),
            slot,
            home: Home::Instance,
            prop_index: Some(0),
            domain_conjunct: None,
            randc,
            window: leaf(bit),
        };
        register_program(
            t,
            Ok(Program {
                vars: vec![mk(0, false), mk(16, randc_hi)],
                conjuncts: c,
                ..Program::default()
            }),
        );
        let h = alloc(t, 2);
        // The middle byte is 0x5a with all eight of its bits unknown.
        set(h, 0, (0x5au64 << 8) | (0xffu64 << (24 + 8)));
        set(h, 1, 0xdead);
        (t, h)
    }

    #[test]
    fn leaf_windows_of_one_property_are_solved_and_written_in_place() {
        let (_, h) = windowed(0x7000_0f10, false);
        let mut seen = std::collections::BTreeSet::new();
        for _ in 0..60 {
            assert_eq!(randomize(h), Outcome::Solved);
            let w = get(h, 0);
            let (lo, mid, hi) = (w & 0xff, (w >> 8) & 0xff, (w >> 16) & 0xff);
            assert!((10..=12).contains(&lo), "{lo}");
            assert_eq!(hi, lo + 1);
            assert_eq!(mid, 0x5a, "the neighbouring leaf keeps its value");
            assert_eq!(w >> 24, 0xff << 8, "the neighbour's unknown bits survive");
            assert_eq!(get(h, 1), 0xdead, "the next property is untouched");
            seen.insert(lo);
        }
        assert_eq!(seen.len(), 3, "all three legal values are reachable");
        release(h);
    }

    /// An inactive leaf (its property's `rand_mode` off) is state read through
    /// its window: it pins the other leaf; one holding X is a loud error.
    #[test]
    fn an_inactive_leaf_is_read_through_its_window() {
        let (_, h) = windowed(0x7000_0f11, false);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        // lo = 11 (known), hi = 12: the constraints hold, nothing is written.
        set(h, 0, 11 | (0x5 << 8) | (12 << 16));
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 11 | (0x5 << 8) | (12 << 16));
        // hi = 13 breaks `hi == lo + 1`: the call checks, and fails.
        set(h, 0, 11 | (13 << 16));
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        // An X bit in `hi` (unknown bit 16 of the 24-bit value) is an error;
        // an X bit in the unread middle byte is not.
        set(h, 0, 11 | (12 << 16) | (1u64 << (24 + 16)));
        assert_eq!(randomize(h), Outcome::StateUnknown);
        set(h, 0, 11 | (12 << 16) | (1u64 << (24 + 8)));
        assert_eq!(randomize(h), Outcome::Solved);
        release(h);
    }

    /// Two leaves of one property are two `randc` cycles, keyed apart.
    #[test]
    fn randc_cycles_of_two_leaves_of_one_property_are_independent() {
        let (_, h) = windowed(0x7000_0f12, true);
        assert_eq!(randomize(h), Outcome::Solved);
        let hi_key = randc_key(
            FieldSlot {
                offset: 0,
                words: 1,
            },
            Some(Window {
                bit: 16,
                width: 8,
                field_width: 24,
            }),
        );
        assert_ne!(hi_key, 0, "a leaf's key differs from its property's");
        assert!(objects::randc_state(h, hi_key).unwrap().live);
        assert!(!objects::randc_state(h, 0).unwrap().live);
        // `hi == lo + 1` over lo in 10..=12 leaves three values: one cycle.
        let mut cycle = vec![get(h, 0) >> 16 & 0xff];
        for _ in 0..2 {
            assert_eq!(randomize(h), Outcome::Solved);
            cycle.push(get(h, 0) >> 16 & 0xff);
        }
        cycle.sort_unstable();
        assert_eq!(cycle, vec![11, 12, 13]);
        release(h);
    }

    #[test]
    fn enum_domain_dropped_only_while_inactive() {
        // x0 in {1, 3} (the domain conjunct, index 0).
        let dom = bin(
            BinOp::LogOr,
            bin(BinOp::Eq, var(0, u(8)), k(u(8), 1), Ty::BIT),
            bin(BinOp::Eq, var(0, u(8)), k(u(8), 3), Ty::BIT),
            Ty::BIT,
        );
        let (t, h) = setup(0x7000_0007, 1, vec![dom]);
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.vars[0].domain_conjunct = Some(0);
        register_program(t, Ok(p));
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert!(matches!(get(h, 0), 1 | 3));
        }
        // Inactive: the current (non-domain) value is kept and no error.
        set(h, 0, 2);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 2);
        release(h);
    }

    #[test]
    fn x_state_is_a_loud_error_and_changes_nothing() {
        // x0 == s, with s holding an X bit (unk bit 8 set in the packed word).
        let c = vec![bin(BinOp::Eq, var(0, u(8)), Expr::State(0, u(8)), Ty::BIT)];
        let (_, h) = setup(0x7000_0008, 1, c);
        set(h, 0, 9);
        set(h, 1, 1 << 8);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h), Outcome::StateUnknown);
        assert_eq!(get(h, 0), 9);
        assert_eq!(objects::prng_seed(h), seed);
        // A known state works.
        set(h, 1, 0x42);
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 0x42);
        release(h);
    }

    #[test]
    fn unreferenced_x_state_is_not_an_error() {
        let (_, h) = setup(0x7000_0009, 1, vec![]);
        set(h, 1, 1 << 8);
        assert_eq!(randomize(h), Outcome::Solved);
        release(h);
    }

    #[test]
    fn dead_handle_missing_program_and_failed_program() {
        assert_eq!(randomize(0), Outcome::DeadHandle);
        let t = ClassTemplateId(0x7000_000a);
        let h = alloc(t, 1);
        assert_eq!(randomize(h), Outcome::NoProgram, "nothing registered");
        register_program(t, Err("unsupported thing".into()));
        assert_eq!(randomize(h), Outcome::NoProgram, "build failure");
        assert_eq!(
            program(t).unwrap().as_ref().clone(),
            Err("unsupported thing".to_string())
        );
        release(h);
        assert_eq!(randomize(h), Outcome::DeadHandle, "stale handle");
    }

    #[test]
    fn four_state_field_round_trip_packs_value_low_unknown_high() {
        // 40-bit field: 80 packed bits over two words.
        let (v, x) = unpack(&[0xde_adbe_ef12, 0], 40);
        assert_eq!(v, BigUint::from(0xde_adbe_ef12u64));
        assert!(x.is_zero());
        let (_, x) = unpack(&[0, 1 << 8], 40);
        assert!(!x.is_zero(), "bit 72 of the packed value is unknown bit 32");
        assert_eq!(pack(&BigUint::from(7u8), 2), Some(vec![7, 0]));
        assert_eq!(pack(&(BigUint::from(1u8) << 70), 1), None);
    }

    /// `x0 < 2 && (x0 == 1 -> x1 == 0)` over two 8-bit variables with the
    /// given `before` edges: 257 models, only one of them with `x0 == 1`.
    fn skewed(id: u32, before: Vec<(u32, u32)>) -> (ClassTemplateId, u64) {
        let c = vec![
            bin(BinOp::Lt, var(0, u(8)), k(u(8), 2), Ty::BIT),
            bin(
                BinOp::LogImpl,
                bin(BinOp::Eq, var(0, u(8)), k(u(8), 1), Ty::BIT),
                bin(BinOp::Eq, var(1, u(8)), k(u(8), 0), Ty::BIT),
                Ty::BIT,
            ),
        ];
        let (t, h) = setup(id, 2, c);
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.before = before;
        register_program(t, Ok(p));
        (t, h)
    }

    fn count_x0_is_one(h: u64, n: u32) -> u32 {
        let mut ones = 0;
        for _ in 0..n {
            assert_eq!(randomize(h), Outcome::Solved);
            ones += u32::from(get(h, 0) == 1);
        }
        ones
    }

    #[test]
    fn solve_before_orders_the_solve_but_not_the_solution_space() {
        // Unordered: P(x0 == 1) = 1/257. `solve x0 before x1`: 1/2 (LRM
        // 18.5.9 Table 18-2). `solve x1 before x0`: x1 is solved first and
        // x1 == 0 is the only value compatible with x0 == 1, but x0 == 0 is
        // compatible with every x1, so P(x0 == 1) = P(x1 == 0) * 1/2 ~ 1/512.
        let (_, h) = skewed(0x7000_0020, vec![]);
        let ones = count_x0_is_one(h, 3000);
        assert!(ones < 40, "unordered: {ones}/3000");
        let (_, h) = skewed(0x7000_0021, vec![(0, 1)]);
        let ones = count_x0_is_one(h, 3000);
        assert!((1350..1650).contains(&ones), "x0 before x1: {ones}/3000");
        let (_, h) = skewed(0x7000_0022, vec![(1, 0)]);
        let ones = count_x0_is_one(h, 3000);
        assert!(ones < 40, "x1 before x0: {ones}/3000");
    }

    #[test]
    fn an_edge_through_an_inactive_variable_is_ignored() {
        let (_, h) = skewed(0x7000_0023, vec![(0, 1)]);
        set(h, 0, 1);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!(
                (get(h, 0), get(h, 1)),
                (1, 0),
                "x0 is state, x1 forced to 0"
            );
        }
    }

    #[test]
    fn a_circular_or_out_of_range_order_is_a_failed_program_not_a_guess() {
        let (_, h) = skewed(0x7000_0024, vec![(0, 1), (1, 0)]);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h), Outcome::Failed);
        assert_eq!(objects::prng_seed(h), seed);
        let (_, h) = skewed(0x7000_0025, vec![(0, 9)]);
        assert_eq!(randomize(h), Outcome::Failed);
    }

    #[test]
    fn outcome_codes_round_trip_and_every_error_has_a_message() {
        for c in 0..=20u64 {
            let o = Outcome::from_code(c).unwrap();
            assert_eq!(o.code(), c);
            assert_eq!(o.error_message().is_some(), c >= 2, "{o:?}");
        }
        assert_eq!(Outcome::from_code(21), None);
    }

    #[test]
    fn every_sat_fallback_failure_has_its_own_outcome() {
        use crate::constraints::bdd::BddBuildError;
        let none: &[bool] = &[];
        for (e, want) in [
            (
                SolveError::Build(BddBuildError::TooLarge {
                    budget: 1,
                    during: "x",
                }),
                Outcome::TooLarge,
            ),
            (
                SolveError::Build(BddBuildError::CnfTooLarge {
                    limit: 1,
                    during: "x",
                }),
                Outcome::TooLarge,
            ),
            (SolveError::SatTimeout, Outcome::SatTimeout),
            (
                SolveError::SatUnsupported { what: "x" },
                Outcome::SatUnsupported,
            ),
            (SolveError::SatModelRejected, Outcome::Failed),
            (SolveError::SatSolverFailure { what: "x" }, Outcome::Failed),
        ] {
            assert_eq!(outcome_of(e.clone(), none), want, "{e}");
        }
        // The messages say which limit was hit.
        assert!(
            Outcome::TooLarge
                .error_message()
                .unwrap()
                .contains("SAT fallback")
        );
        assert!(
            Outcome::SatTimeout
                .error_message()
                .unwrap()
                .contains("time limit")
        );
        assert!(
            Outcome::SatUnsupported
                .error_message()
                .unwrap()
                .contains("does not support")
        );
    }

    /// `x0 dist { 0 := s, 1 := 1 }` over one 8-bit variable, `s` the state
    /// field read as a signed 8-bit weight.
    fn dist_program(id: u32) -> (ClassTemplateId, u64) {
        use crate::constraints::dist::{Dist, Item, SELECTOR_BASE, Span};
        let x = var(0, u(8));
        let item = |v: u64, w: Expr| Item {
            member: bin(BinOp::Eq, x.clone(), k(u(8), v), Ty::BIT),
            ty: u(8),
            span: Span::Point(k(u(8), v)),
            weight: w,
            per_range: false,
        };
        let d = Dist {
            subject_ty: u(8),
            plain_var: Some(0),
            vars: vec![0],
            items: vec![
                item(
                    0,
                    Expr::Resize(Box::new(Expr::State(0, u(8))), Ty::signed(8)),
                ),
                item(1, k(Ty::signed(8), 1)),
            ],
            default: None,
            subject: None,
        };
        let (t, h) = setup(id, 1, vec![d.conjunct(SELECTOR_BASE)]);
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.dists = vec![d];
        register_program(t, Ok(p));
        (t, h)
    }

    #[test]
    fn a_dist_weight_is_read_from_the_state_at_each_call() {
        let (_, h) = dist_program(0x7000_0040);
        // LRM 18.5.3: `0 := 3, 1 := 1` is 3:1.
        set(h, 1, 3);
        let mut zeros = 0;
        for _ in 0..2000 {
            assert_eq!(randomize(h), Outcome::Solved);
            let x = get(h, 0);
            assert!(x <= 1, "x = {x}");
            zeros += u32::from(x == 0);
        }
        assert!(
            (1400..1600).contains(&zeros),
            "x == 0: {zeros}/2000 (want 1500)"
        );
        // A weight of 0 excludes its value; the weight is re-read.
        set(h, 1, 0);
        for _ in 0..50 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!(get(h, 0), 1);
        }
    }

    #[test]
    fn a_negative_dist_weight_fails_the_call_and_changes_nothing() {
        let (_, h) = dist_program(0x7000_0041);
        set(h, 1, 3);
        assert_eq!(randomize(h), Outcome::Solved);
        let (before, seed) = (get(h, 0), objects::prng_seed(h));
        set(h, 1, 200); // -56 as a signed byte
        assert_eq!(randomize(h), Outcome::BadDistWeight);
        assert_eq!((get(h, 0), objects::prng_seed(h)), (before, seed));
        // An X state weight is the usual state-unknown error.
        set(h, 1, 1 << 8);
        assert_eq!(randomize(h), Outcome::StateUnknown);
    }

    #[test]
    fn a_dist_on_an_inactive_variable_is_a_membership_test_on_its_value() {
        let (_, h) = dist_program(0x7000_0042);
        set(h, 1, 3);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        set(h, 0, 1);
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 1);
        // 7 is in no item, and a value of weight 0 is excluded too.
        set(h, 0, 7);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        set(h, 0, 0);
        set(h, 1, 0);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
    }

    /// LRM 18.5.3: `x dist {[0:3] :/ 8, default :/ 8}` over a byte: the range
    /// weighs 8 (2 per value) and the other 252 values share the default's 8,
    /// so x <= 3 half of the time and every other draw is one of 4..=255.
    #[test]
    fn a_dist_default_spreads_its_weight_over_the_values_no_item_names() {
        use crate::constraints::dist::{DefaultWeight, Dist, Item, SELECTOR_BASE, Span};
        let x = var(0, u(8));
        let d = Dist {
            subject_ty: u(8),
            plain_var: Some(0),
            vars: vec![0],
            items: vec![Item {
                member: bin(BinOp::Le, x.clone(), k(u(8), 3), Ty::BIT),
                ty: u(8),
                span: Span::Range {
                    lo: Some(k(u(8), 0)),
                    hi: Some(k(u(8), 3)),
                },
                weight: k(u(32), 8),
                per_range: true,
            }],
            default: Some(DefaultWeight {
                weight: k(u(32), 8),
                per_range: true,
            }),
            subject: None,
        };
        let (t, h) = setup(0x7000_0043, 1, vec![d.conjunct(SELECTOR_BASE)]);
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.dists = vec![d];
        register_program(t, Ok(p));
        let (mut low, mut distinct) = (0u32, std::collections::BTreeSet::new());
        for _ in 0..4000 {
            assert_eq!(randomize(h), Outcome::Solved);
            let v = get(h, 0);
            if v <= 3 {
                low += 1;
            } else {
                distinct.insert(v);
            }
        }
        assert!(
            (1850..2150).contains(&low),
            "x <= 3: {low}/4000 (want 2000)"
        );
        assert!(
            distinct.len() > 100,
            "the default values are spread: {}",
            distinct.len()
        );
    }

    /// `randc x0 < limit` (and `x0 >= s`, `s` the state field) with an
    /// optional `rand x1 > x0` over a two-variable template.
    fn randc_program(id: u32, limit: u64) -> (ClassTemplateId, u64) {
        let c = vec![
            bin(BinOp::Lt, var(0, u(8)), k(u(8), limit), Ty::BIT),
            bin(BinOp::Ge, var(0, u(8)), Expr::State(0, u(8)), Ty::BIT),
            bin(BinOp::Gt, var(1, u(8)), var(0, u(8)), Ty::BIT),
        ];
        let (t, h) = setup(id, 2, c);
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.vars[0].randc = true;
        register_program(t, Ok(p));
        (t, h)
    }

    fn draw_cycle(h: u64, n: usize) -> Vec<u64> {
        (0..n)
            .map(|_| {
                assert_eq!(randomize(h), Outcome::Solved);
                get(h, 0)
            })
            .collect()
    }

    #[test]
    fn randc_visits_every_legal_value_once_per_cycle() {
        // LRM 18.4.2: every window of `limit` consecutive calls (cycles are
        // aligned: the engine starts one at the first call) is a permutation.
        let (_, h) = randc_program(0x7000_0030, 6);
        let mut orders = std::collections::BTreeSet::new();
        for _ in 0..40 {
            let mut cyc = draw_cycle(h, 6);
            orders.insert(cyc.clone());
            cyc.sort_unstable();
            assert_eq!(cyc, vec![0, 1, 2, 3, 4, 5]);
        }
        assert!(orders.len() > 10, "cycles are shuffled, not a fixed order");
        release(h);
    }

    #[test]
    fn randc_state_is_committed_only_when_the_call_succeeds() {
        let (_, h) = randc_program(0x7000_0031, 4);
        let first = draw_cycle(h, 2);
        // s = 200 makes `x0 >= s` unsatisfiable: the call fails and the
        // cycle must not move (LRM 18.6.3: a failed call changes nothing).
        let saved = objects::randc_state(h, 0).unwrap();
        set(h, 2, 200);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        assert_eq!(objects::randc_state(h, 0).unwrap(), saved);
        assert_eq!(objects::prng_seed(h), seed);
        set(h, 2, 0);
        let rest = draw_cycle(h, 2);
        let mut all = [first, rest].concat();
        all.sort_unstable();
        assert_eq!(all, vec![0, 1, 2, 3], "the interrupted cycle completes");
        release(h);
    }

    #[test]
    fn randc_constraint_change_starts_a_new_cycle() {
        // LRM 18.4.2: a changed constraint set restarts the permutation.
        let (_, h) = randc_program(0x7000_0032, 8);
        draw_cycle(h, 3);
        set(h, 2, 6); // x0 in {6, 7} now
        let next = draw_cycle(h, 2);
        let mut sorted = next.clone();
        sorted.sort_unstable();
        assert_eq!(sorted, vec![6, 7], "{next:?}: a fresh cycle of the new set");
        release(h);
    }

    #[test]
    fn randc_interacts_with_rand_without_failing() {
        // x1 > x0 with x0 == 5 leaves x1 only 6..=255; every cycle of x0
        // still completes and every x1 satisfies the constraint.
        let (_, h) = randc_program(0x7000_0033, 6);
        for _ in 0..10 {
            let mut cyc = Vec::new();
            for _ in 0..6 {
                assert_eq!(randomize(h), Outcome::Solved);
                assert!(get(h, 1) > get(h, 0));
                cyc.push(get(h, 0));
            }
            cyc.sort_unstable();
            assert_eq!(cyc, vec![0, 1, 2, 3, 4, 5]);
        }
        release(h);
    }

    #[test]
    fn an_inactive_randc_variable_is_state_and_keeps_its_cycle() {
        let (_, h) = randc_program(0x7000_0034, 4);
        draw_cycle(h, 2);
        let saved = objects::randc_state(h, 0).unwrap();
        set(h, 0, 2);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        for _ in 0..5 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!(get(h, 0), 2, "not redrawn");
            assert!(get(h, 1) > 2);
        }
        assert_eq!(objects::randc_state(h, 0).unwrap(), saved);
        release(h);
    }

    /// Instance `x0` made a `static randc` living at word 0 of a separate
    /// static-property object (`Home::Static(7)`), shared by every instance.
    fn static_randc(id: u32) -> (u64, u64, u64) {
        let (t, a) = randc_program(id, 4);
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.vars[0].home = Home::Static(7);
        p.vars[0].prop_index = None;
        register_program(t, Ok(p));
        let b = alloc(t, 3);
        objects::set_prng_seed(b, 0x9999);
        let st = alloc(ClassTemplateId(id + 0x100), 1);
        (a, b, st)
    }

    #[test]
    fn a_static_randc_cycles_across_all_instances() {
        // LRM 18.4.2/8.9: one variable, one cycle, however many objects
        // randomize it. Alternating two objects still sees each value once
        // per four calls.
        let (a, b, st) = static_randc(0x7000_0035);
        let pairs = [(7u32, st)];
        for _ in 0..10 {
            let mut cyc = Vec::new();
            for i in 0..4 {
                let h = if i % 2 == 0 { a } else { b };
                assert_eq!(super::randomize(h, &pairs), Outcome::Solved);
                let mut w = [0u64];
                assert!(objects::field_get(
                    st,
                    FieldSlot {
                        offset: 0,
                        words: 1
                    },
                    &mut w
                ));
                cyc.push(w[0]);
                assert_eq!(get(h, 0), 0, "the instance's own word is untouched");
            }
            cyc.sort_unstable();
            assert_eq!(cyc, vec![0, 1, 2, 3]);
        }
        assert_eq!(
            objects::randc_state(a, 0).unwrap(),
            RandcState::default(),
            "the cycle lives in the static object, not the instance"
        );
        assert_ne!(objects::randc_state(st, 0).unwrap(), RandcState::default());
        release(a);
        release(b);
        release(st);
    }

    #[test]
    fn instance_randc_cycles_are_per_object() {
        // The contrast: an instance randc keeps one cycle per object.
        let (_, a) = randc_program(0x7000_0036, 4);
        let b = alloc(ClassTemplateId(0x7000_0036), 3);
        objects::set_prng_seed(b, 0x4242);
        for _ in 0..6 {
            let mut ca = Vec::new();
            let mut cb = Vec::new();
            for _ in 0..4 {
                assert_eq!(randomize(a), Outcome::Solved);
                ca.push(get(a, 0));
                assert_eq!(randomize(b), Outcome::Solved);
                cb.push(get(b, 0));
            }
            ca.sort_unstable();
            cb.sort_unstable();
            assert_eq!((ca, cb), (vec![0, 1, 2, 3], vec![0, 1, 2, 3]));
        }
        release(a);
        release(b);
    }

    #[test]
    fn a_missing_static_object_is_a_loud_error_that_changes_nothing() {
        let (a, _, st) = static_randc(0x7000_0037);
        let seed = objects::prng_seed(a);
        assert_eq!(super::randomize(a, &[]), Outcome::StaticUnavailable);
        assert_eq!(super::randomize(a, &[(8, st)]), Outcome::StaticUnavailable);
        assert_eq!(objects::prng_seed(a), seed);
        assert_eq!(super::randomize(a, &[(7, st)]), Outcome::Solved);
        release(a);
        release(st);
    }

    // ---- LRM 18.5.12 guards over object handles ---------------------------
    //
    // `class D { int x; }  class C { rand int x, y; D a, b; ... }` with the
    // template's words: x = 0, y = 1, handle a = 2..4, handle b = 4..6. The
    // state variables are `a.x` (0) and `b.x` (1), each read through a handle.

    const HANDLE_A: usize = 2;
    const HANDLE_B: usize = 4;

    fn handle_slot(offset: usize) -> FieldSlot {
        FieldSlot { offset, words: 2 }
    }

    /// A `D` object whose `x` is `x`.
    fn d_object(id: u32, x: u64) -> u64 {
        let d = alloc(ClassTemplateId(id), 1);
        set(d, 0, x);
        d
    }

    fn set_handle(h: u64, offset: usize, target: u64) {
        assert!(objects::field_set(h, handle_slot(offset), &[target, 0]));
    }

    /// The program of the module comment's class `C` with `conjuncts`, and one
    /// object of it whose handles `a` and `b` point at `a_x` / `b_x` (`None`
    /// = null).
    fn guard_class(id: u32, conjuncts: Vec<Expr>, a_x: Option<u64>, b_x: Option<u64>) -> u64 {
        let t = ClassTemplateId(id);
        let rand_slot = |i: usize| FieldSlot {
            offset: i,
            words: 1,
        };
        register_rand_props(
            t,
            (0..2)
                .map(|i| RandProp {
                    slot: rand_slot(i),
                    kind: RandKind::Rand,
                })
                .collect(),
        );
        let state = |root: usize| ProgState {
            class_of: false,
            root_bit: 0,
            ty: u(8),
            slot: handle_slot(root),
            window: None,
            home: Home::Instance,
            via: vec![rand_slot(0)],
        };
        register_program(
            t,
            Ok(Program {
                vars: (0..2)
                    .map(|i| ProgVar {
                        ty: u(8),
                        slot: rand_slot(i),
                        home: Home::Instance,
                        prop_index: Some(i),
                        domain_conjunct: None,
                        randc: false,
                        window: None,
                    })
                    .collect(),
                states: vec![state(HANDLE_A), state(HANDLE_B)],
                conjuncts,
                before: Vec::new(),
                dists: Vec::new(),
                ..Program::default()
            }),
        );
        let h = alloc(t, 6);
        objects::set_prng_seed(h, 0x5eed_0018);
        if let Some(x) = a_x {
            set_handle(h, HANDLE_A, d_object(id + 0x100, x));
        }
        if let Some(x) = b_x {
            set_handle(h, HANDLE_B, d_object(id + 0x200, x));
        }
        h
    }

    fn x() -> Expr {
        var(0, u(8))
    }
    fn y() -> Expr {
        var(1, u(8))
    }
    fn a_x() -> Expr {
        Expr::State(0, u(8))
    }
    fn b_x() -> Expr {
        Expr::State(1, u(8))
    }
    fn lt_xy() -> Expr {
        bin(BinOp::Lt, x(), y(), Ty::BIT)
    }
    fn a_gt_b() -> Expr {
        bin(BinOp::Gt, a_x(), b_x(), Ty::BIT)
    }
    fn a_is_5() -> Expr {
        bin(BinOp::Eq, a_x(), k(u(8), 5), Ty::BIT)
    }
    fn or(l: Expr, r: Expr) -> Expr {
        bin(BinOp::LogOr, l, r, Ty::BIT)
    }
    fn and(l: Expr, r: Expr) -> Expr {
        bin(BinOp::LogAnd, l, r, Ty::BIT)
    }
    /// `pred -> x + y == 10`, as the builder emits it.
    fn guard_sum(pred: Expr) -> Vec<Expr> {
        vec![Expr::Guard(
            Box::new(pred),
            Box::new(bin(
                BinOp::Eq,
                bin(BinOp::Add, x(), y(), u(8)),
                k(u(8), 10),
                Ty::BIT,
            )),
            Box::new(k(Ty::BIT, 1)),
            Ty::BIT,
        )]
    }

    /// 400 draws of `h`: how many have `x + y == 10` (mod 256) and how many
    /// have `x < y`; and whether `(x < y) -> (x + y == 10)` held on every one.
    fn sum_draws(h: u64) -> (u32, u32, bool) {
        let (mut sums, mut lts, mut implied) = (0, 0, true);
        for _ in 0..400 {
            assert_eq!(randomize(h), Outcome::Solved);
            let (x, y) = (get(h, 0) as u8, get(h, 1) as u8);
            let sum = x.wrapping_add(y) == 10;
            sums += u32::from(sum);
            lts += u32::from(x < y);
            implied &= x >= y || sum;
        }
        (sums, lts, implied)
    }

    /// Every draw satisfies the body, whatever the guard says about `x < y`.
    fn assert_body_unconditional(h: u64) {
        let (sums, _, _) = sum_draws(h);
        assert_eq!(sums, 400, "an unconditional `x + y == 10`");
    }

    /// The body only binds when `x < y`: it holds then, and a draw with
    /// `x >= y` is not forced to satisfy it.
    fn assert_body_conditional(h: u64) {
        let (sums, lts, implied) = sum_draws(h);
        assert!(implied, "(x < y) -> (x + y == 10) always holds");
        assert!(lts < 400 && sums < 400, "not unconditional: {sums}/{lts}");
    }

    /// No constraint at all: the body never binds.
    fn assert_eliminated(h: u64) {
        let (sums, lts, _) = sum_draws(h);
        assert!(sums < 20, "x + y == 10 is a 1/256 accident: {sums}");
        assert!((120..280).contains(&lts), "x and y are free: {lts}/400");
    }

    fn assert_error(h: u64) {
        let (seed, x0) = (objects::prng_seed(h), get(h, 0));
        assert_eq!(randomize(h), Outcome::GuardError);
        assert_eq!((objects::prng_seed(h), get(h, 0)), (seed, x0), "no change");
    }

    /// LRM 18.5.12 example 1: `(x < y || a.x > b.x || a.x == 5) -> x + y == 10`.
    #[test]
    fn lrm_example_1_or_guard() {
        let c = || guard_sum(or(or(lt_xy(), a_gt_b()), a_is_5()));
        // Case 1: a non-null (a.x == 5), b null: `a.x == 5` is TRUE, so the
        // constraint is unconditional.
        assert_body_unconditional(guard_class(0x7100_0001, c(), Some(5), None));
        // Case 2: a null: a.x is ERROR in two operands, TRUE decides nothing.
        assert_error(guard_class(0x7100_0002, c(), None, Some(1)));
        // Case 3: a.x == 10, b.x == 20: only `x < y` is random.
        assert_body_conditional(guard_class(0x7100_0003, c(), Some(10), Some(20)));
    }

    /// LRM 18.5.12 example 2: `(x < y && a.x > b.x && a.x == 5) -> x + y == 10`.
    #[test]
    fn lrm_example_2_and_guard() {
        let c = || guard_sum(and(and(lt_xy(), a_gt_b()), a_is_5()));
        // Case 1: a.x == 6, b null: `a.x == 5` is FALSE, which dominates the
        // ERROR of `a.x > b.x`: the constraint is eliminated, with no error.
        assert_eliminated(guard_class(0x7100_0011, c(), Some(6), None));
        // Case 2: a null: ERROR.
        assert_error(guard_class(0x7100_0012, c(), None, Some(1)));
        // Case 3: a.x == 5, b.x == 2: conditional on `x < y`.
        assert_body_conditional(guard_class(0x7100_0013, c(), Some(5), Some(2)));
    }

    /// LRM 18.5.12 example 3: `(x < y && (a.x > b.x || a.x == 5)) -> ...`.
    #[test]
    fn lrm_example_3_nested_guard() {
        let c = || guard_sum(and(lt_xy(), or(a_gt_b(), a_is_5())));
        // Case 1: b null, a.x == 5: `ERROR || TRUE` is TRUE; conditional.
        assert_body_conditional(guard_class(0x7100_0021, c(), Some(5), None));
        // Case 2: b null, a.x == 8: `ERROR || FALSE` is ERROR.
        assert_error(guard_class(0x7100_0022, c(), Some(8), None));
        // Case 3: a null: ERROR.
        assert_error(guard_class(0x7100_0023, c(), None, Some(1)));
        // Case 4: a.x == 5, b.x == 2: conditional.
        assert_body_conditional(guard_class(0x7100_0024, c(), Some(5), Some(2)));
    }

    /// The else arm of a guard is taken when the predicate is FALSE, and an
    /// erroring guard inside the arm that is not taken raises nothing.
    #[test]
    fn a_false_guard_selects_the_else_arm_and_never_examines_the_other() {
        // if (a.x == 5) { if (b.x == 1) x == 9; } else y == 3;
        let inner = Expr::Guard(
            Box::new(bin(BinOp::Eq, b_x(), k(u(8), 1), Ty::BIT)),
            Box::new(bin(BinOp::Eq, x(), k(u(8), 9), Ty::BIT)),
            Box::new(k(Ty::BIT, 1)),
            Ty::BIT,
        );
        let c = vec![Expr::Guard(
            Box::new(a_is_5()),
            Box::new(inner),
            Box::new(bin(BinOp::Eq, y(), k(u(8), 3), Ty::BIT)),
            Ty::BIT,
        )];
        // a.x == 6: else arm; the null `b` in the then arm is never read.
        let h = guard_class(0x7100_0031, c.clone(), Some(6), None);
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!(get(h, 1), 3);
        }
        // a.x == 5, b null: the then arm runs, and its own guard is ERROR.
        assert_error(guard_class(0x7100_0032, c.clone(), Some(5), None));
        // a.x == 5, b.x == 1: x == 9.
        let h = guard_class(0x7100_0033, c, Some(5), Some(1));
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 9);
    }

    /// A read through a null handle outside any guard is not an X: it has its
    /// own outcome, and an X/Z handle or value keeps `StateUnknown`.
    #[test]
    fn a_null_handle_outside_a_guard_fails_the_call_with_its_own_outcome() {
        let c = vec![bin(BinOp::Eq, x(), a_x(), Ty::BIT)];
        let h = guard_class(0x7100_0041, c.clone(), None, None);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h), Outcome::NullHandle);
        assert_eq!(objects::prng_seed(h), seed);
        // The same constraint with a live handle solves.
        let h = guard_class(0x7100_0042, c.clone(), Some(77), None);
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 77);
        // A deleted target is as good as null.
        let h = guard_class(0x7100_0043, c.clone(), Some(77), None);
        let mut buf = [0u64; 2];
        assert!(objects::field_get(h, handle_slot(HANDLE_A), &mut buf));
        release(buf[0]);
        assert_eq!(randomize(h), Outcome::NullHandle);
        // An X bit in the handle is StateUnknown, not a null.
        let h = guard_class(0x7100_0044, c, Some(77), None);
        assert!(objects::field_set(h, handle_slot(HANDLE_A), &[1, 1]));
        assert_eq!(randomize(h), Outcome::StateUnknown);
    }

    /// A guard whose operand reads an X/Z value is an ERROR too (the value is
    /// not null, but it is not a value either).
    #[test]
    fn an_unknown_value_in_a_guard_is_an_error() {
        let h = guard_class(0x7100_0051, guard_sum(a_is_5()), Some(5), None);
        // Poison a.x's X bits: the D object is the one `a` designates.
        let mut buf = [0u64; 2];
        assert!(objects::field_get(h, handle_slot(HANDLE_A), &mut buf));
        assert!(objects::field_set(
            buf[0],
            FieldSlot {
                offset: 0,
                words: 1
            },
            &[5 | (1 << 8)]
        ));
        assert_error(h);
    }

    /// A handle chain longer than one hop: `n.n.v` through three objects, the
    /// middle link of which is null in the second call.
    #[test]
    fn a_two_hop_handle_chain_reads_the_far_member_and_fails_on_a_null_link() {
        // Node = { handle n (words 0..2), int v (word 2) }.
        let node = |id: u32, v: u64| {
            let o = alloc(ClassTemplateId(id), 3);
            set(o, 2, v);
            o
        };
        let t = ClassTemplateId(0x7100_0061);
        register_rand_props(
            t,
            vec![RandProp {
                slot: FieldSlot {
                    offset: 0,
                    words: 1,
                },
                kind: RandKind::Rand,
            }],
        );
        let root = |offset| ProgState {
            class_of: false,
            root_bit: 0,
            ty: u(8),
            slot: handle_slot(offset),
            window: None,
            home: Home::Instance,
            via: vec![
                handle_slot(0),
                FieldSlot {
                    offset: 2,
                    words: 1,
                },
            ],
        };
        // x == a.n.v: `a` is the root handle at words 1..3.
        register_program(
            t,
            Ok(Program {
                vars: vec![ProgVar {
                    ty: u(8),
                    slot: FieldSlot {
                        offset: 0,
                        words: 1,
                    },
                    home: Home::Instance,
                    prop_index: Some(0),
                    domain_conjunct: None,
                    randc: false,
                    window: None,
                }],
                states: vec![root(1)],
                conjuncts: vec![bin(BinOp::Eq, x(), Expr::State(0, u(8)), Ty::BIT)],
                before: Vec::new(),
                dists: Vec::new(),
                ..Program::default()
            }),
        );
        let h = alloc(t, 3);
        objects::set_prng_seed(h, 1);
        let (n0, n1) = (node(0x7100_0062, 1), node(0x7100_0063, 42));
        set_handle(h, 1, n0);
        set_handle(n0, 0, n1);
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(get(h, 0), 42);
        set_handle(n0, 0, 0);
        assert_eq!(randomize(h), Outcome::NullHandle);
    }

    // ---- Task C9: real variables ----

    use crate::constraints::real_domain::{
        CmpOp, RealCond, RealDist, RealDistItem, RealExpr, RealSpan,
    };

    fn rslot(offset: usize) -> FieldSlot {
        FieldSlot { offset, words: 2 }
    }
    fn rk(x: f64) -> RealExpr {
        RealExpr::Const(real_domain::Real::new(x), FloatKind::F64)
    }
    fn rcmp(op: CmpOp, a: RealExpr, b: RealExpr) -> RealCond {
        RealCond::Cmp(op, a, b)
    }
    fn rget(h: u64, off: usize) -> f64 {
        let mut b = [0u64; 2];
        assert!(objects::field_get(h, rslot(off), &mut b));
        assert_eq!(b[1], 0, "a solved real has no unknown bits");
        f64::from_bits(b[0])
    }
    fn rset_bits(h: u64, off: usize, bits: u64, unk: u64) {
        assert!(objects::field_set(h, rslot(off), &[bits, unk]));
    }

    /// A template with the real rand variable `r` at word 0 (property 0), the
    /// 8-bit integral rand variable `x` at word 2 (property 1) and a real state
    /// `s` at word 3 (the program's state 0).
    fn setup_real(id: u32, real: RealProblem, conjuncts: Vec<Expr>) -> u64 {
        let t = ClassTemplateId(id);
        register_rand_props(
            t,
            vec![
                RandProp {
                    slot: rslot(0),
                    kind: RandKind::Rand,
                },
                RandProp {
                    slot: FieldSlot {
                        offset: 2,
                        words: 1,
                    },
                    kind: RandKind::Rand,
                },
            ],
        );
        register_program(
            t,
            Ok(Program {
                vars: vec![ProgVar {
                    ty: u(8),
                    slot: FieldSlot {
                        offset: 2,
                        words: 1,
                    },
                    home: Home::Instance,
                    prop_index: Some(1),
                    domain_conjunct: None,
                    randc: false,
                    window: None,
                }],
                states: vec![ProgState {
                    class_of: false,
                    root_bit: 0,
                    ty: u(64),
                    slot: rslot(3),
                    window: None,
                    home: Home::Instance,
                    via: Vec::new(),
                }],
                conjuncts,
                real_vars: vec![ProgRealVar {
                    kind: FloatKind::F64,
                    slot: rslot(0),
                    home: Home::Instance,
                    prop_index: Some(0),
                    window: None,
                }],
                real,
                ..Program::default()
            }),
        );
        let h = alloc(t, 5);
        objects::set_prng_seed(h, 0x5eed_0c09);
        h
    }

    fn unit_interval() -> RealProblem {
        RealProblem {
            kinds: vec![FloatKind::F64],
            conds: vec![
                rcmp(CmpOp::Ge, RealExpr::Var(0), rk(1.0)),
                rcmp(CmpOp::Lt, RealExpr::Var(0), rk(2.0)),
            ],
            ..RealProblem::default()
        }
    }

    #[test]
    fn real_variable_is_solved_with_the_integral_ones_and_the_seed_advances() {
        // 1.0 <= r < 2.0 alongside x == 7.
        let c = vec![bin(BinOp::Eq, var(0, u(8)), k(u(8), 7), Ty::BIT)];
        let h = setup_real(0x7000_0c01, unit_interval(), c);
        let before = objects::prng_seed(h);
        let mut bins = [0u32; 4];
        for _ in 0..400 {
            assert_eq!(randomize(h), Outcome::Solved);
            let r = rget(h, 0);
            assert!((1.0..2.0).contains(&r), "{r}");
            assert_eq!(get(h, 2), 7);
            bins[((r - 1.0) * 4.0) as usize] += 1;
        }
        assert!(
            bins.iter().all(|&n| n > 60),
            "uniform over the interval: {bins:?}"
        );
        assert_ne!(objects::prng_seed(h), before);
        release(h);
    }

    #[test]
    fn unsatisfiable_real_constraint_writes_nothing_and_keeps_the_seed() {
        let mut p = unit_interval();
        p.conds.push(rcmp(CmpOp::Gt, RealExpr::Var(0), rk(5.0)));
        let h = setup_real(0x7000_0c02, p, Vec::new());
        rset_bits(h, 0, 3.25f64.to_bits(), 0);
        set(h, 2, 99);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        assert_eq!(rget(h, 0), 3.25);
        assert_eq!(get(h, 2), 99, "the integral variable is untouched too");
        assert_eq!(objects::prng_seed(h), seed);
        release(h);
    }

    #[test]
    fn inactive_real_variable_is_a_constant_and_is_not_written() {
        let h = setup_real(0x7000_0c03, unit_interval(), Vec::new());
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        rset_bits(h, 0, 1.5f64.to_bits(), 0);
        for _ in 0..10 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert_eq!(rget(h, 0), 1.5);
        }
        // Outside the constraint it acts as a checker.
        rset_bits(h, 0, 2.0f64.to_bits(), 0);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        assert_eq!(rget(h, 0), 2.0);
        // An X bit in it is an error, never a silent 0.0.
        rset_bits(h, 0, 0, 1);
        assert_eq!(randomize(h), Outcome::StateUnknown);
        release(h);
    }

    #[test]
    fn real_state_variable_bounds_the_solution_and_division_by_zero_is_a_loud_error() {
        // r < s, with s a real state at word 3.
        let p = RealProblem {
            kinds: vec![FloatKind::F64],
            conds: vec![
                rcmp(CmpOp::Ge, RealExpr::Var(0), rk(0.0)),
                rcmp(
                    CmpOp::Lt,
                    RealExpr::Var(0),
                    RealExpr::State(0, FloatKind::F64),
                ),
            ],
            ..RealProblem::default()
        };
        let h = setup_real(0x7000_0c04, p, Vec::new());
        rset_bits(h, 3, 0.5f64.to_bits(), 0);
        for _ in 0..50 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert!((0.0..0.5).contains(&rget(h, 0)));
        }
        // Every comparison with a NaN is false (IEEE 754), so `r < NaN` has no
        // solution: that is an ordinary unsatisfiable problem, not an error.
        rset_bits(h, 3, f64::NAN.to_bits(), 0);
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        rset_bits(h, 3, 0, 1);
        assert_eq!(randomize(h), Outcome::StateUnknown);
        release(h);

        // A division by a state that is 0.0 has no value: a loud error.
        let p = RealProblem {
            kinds: vec![FloatKind::F64],
            conds: vec![rcmp(
                CmpOp::Lt,
                RealExpr::Div(
                    Box::new(RealExpr::Var(0)),
                    Box::new(RealExpr::State(0, FloatKind::F64)),
                ),
                rk(1.0),
            )],
            ..RealProblem::default()
        };
        let h = setup_real(0x7000_0c08, p, Vec::new());
        rset_bits(h, 3, 2.0f64.to_bits(), 0);
        assert_eq!(randomize(h), Outcome::Solved);
        assert!(rget(h, 0) < 2.0);
        rset_bits(h, 3, 0.0f64.to_bits(), 0);
        assert_eq!(randomize(h), Outcome::RealDomain);
        release(h);
    }

    #[test]
    fn real_dist_follows_its_weights() {
        // r dist { 1.0 := 3, [10.0 : 20.0] :/ 1 }: the point has weight 3 and the
        // range a total of 1.
        let p = RealProblem {
            kinds: vec![FloatKind::F64],
            dists: vec![RealDist {
                var: 0,
                items: vec![
                    RealDistItem {
                        span: RealSpan::Point(rk(1.0)),
                        weight: k(u(32), 3),
                    },
                    RealDistItem {
                        span: RealSpan::Range {
                            lo: Some(rk(10.0)),
                            hi: Some(rk(20.0)),
                        },
                        weight: k(u(32), 1),
                    },
                ],
                default: None,
            }],
            ..RealProblem::default()
        };
        let h = setup_real(0x7000_0c05, p, Vec::new());
        let (mut point, mut range) = (0u32, 0u32);
        for _ in 0..2000 {
            assert_eq!(randomize(h), Outcome::Solved);
            let r = rget(h, 0);
            if r == 1.0 {
                point += 1;
            } else {
                assert!((10.0..=20.0).contains(&r), "{r}");
                range += 1;
            }
        }
        // Expected 1500 / 500; 5 sigma is about 100.
        assert!((1400..=1600).contains(&point), "{point} / {range}");
        release(h);
    }

    #[test]
    fn the_integral_solution_is_drawn_before_the_real_one() {
        // From the same seed the integral variable gets the same value with or
        // without a real problem next to it, and an all-inactive real problem
        // draws nothing at all.
        let c = vec![bin(BinOp::Ge, var(0, u(8)), k(u(8), 3), Ty::BIT)];
        let (_, plain) = setup(0x7000_0c06, 1, c.clone());
        let h = setup_real(0x7000_0c07, unit_interval(), c);
        objects::set_prng_seed(h, objects::prng_seed(plain).unwrap());
        let seed = objects::prng_seed(plain).unwrap();
        assert_eq!(randomize(plain), Outcome::Solved);
        assert_eq!(randomize(h), Outcome::Solved);
        // `setup` puts its variable at word 0, `setup_real` at word 2.
        assert_eq!(get(plain, 0), get(h, 2));
        assert_ne!(
            objects::prng_seed(h),
            objects::prng_seed(plain),
            "real draws follow"
        );
        // All real variables inactive: the stream ends where the integral part left it.
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        rset_bits(h, 0, 1.5f64.to_bits(), 0);
        objects::set_prng_seed(h, seed);
        assert_eq!(randomize(h), Outcome::Solved);
        assert_eq!(objects::prng_seed(h), objects::prng_seed(plain));
        release(plain);
        release(h);
    }
}

/// Dynamic arrays and queues in a program (Task C14): sizes, elements, state.
#[cfg(test)]
mod array_tests {
    use super::*;
    use crate::collections::{KeyKind, Shape};
    use crate::constraints::ir::{ArrayNode, BinOp, LoopId, ReduceOp};
    use crate::objects::{RandKind, RandProp, alloc, register_rand_props, release};

    fn u8t() -> Ty {
        Ty::unsigned(8)
    }
    fn s32() -> Ty {
        Ty::signed(32)
    }
    fn bin(op: BinOp, a: Expr, b: Expr, t: Ty) -> Expr {
        Expr::Binary(op, Box::new(a), Box::new(b), t)
    }
    fn k(t: Ty, v: u64) -> Expr {
        Expr::constant(t, v)
    }
    fn node(n: ArrayNode) -> Expr {
        Expr::Array(n)
    }
    fn lp(id: LoopId) -> Expr {
        node(ArrayNode::Loop(id, s32()))
    }
    fn elem(a: u32, i: Expr) -> Expr {
        node(ArrayNode::Elem {
            array: a,
            index: Box::new(i),
            ty: u8t(),
        })
    }
    fn shape() -> Shape {
        Shape {
            elem_words: 1,
            assoc: false,
            key: KeyKind::Int {
                width: 32,
                signed: false,
            },
            obj: false,
            nested: collections::Nested::NONE,
        }
    }
    fn slot(o: usize) -> FieldSlot {
        FieldSlot {
            offset: o,
            words: 1,
        }
    }
    fn contents(h: u64) -> Vec<u64> {
        let mut b = [0u64];
        assert!(objects::field_get(h, slot(0), &mut b));
        collections::elements(b[0])
            .into_iter()
            .map(|e| e[0])
            .collect()
    }

    /// `rand byte a[]` at word 0 (property 0) and `rand byte len` at word 1
    /// (property 1); the program's constraints are `conjuncts`.
    fn setup(id: u32, conjuncts: Vec<Expr>, initial: &[u64]) -> u64 {
        let t = ClassTemplateId(id);
        register_rand_props(
            t,
            vec![
                RandProp {
                    slot: slot(0),
                    kind: RandKind::Rand,
                },
                RandProp {
                    slot: slot(1),
                    kind: RandKind::Rand,
                },
            ],
        );
        register_program(
            t,
            Ok(Program {
                vars: vec![ProgVar {
                    ty: u8t(),
                    slot: slot(1),
                    home: Home::Instance,
                    prop_index: Some(1),
                    domain_conjunct: None,
                    randc: false,
                    window: None,
                }],
                conjuncts,
                arrays: vec![ProgArray {
                    elem_ty: u8t(),
                    elem_words: 1,
                    slot: slot(0),
                    home: Home::Instance,
                    rand: true,
                    prop_index: Some(0),
                    elem_domain: None,
                    assoc: false,
                    nested: false,
                    template_of: None,
                    inner_fixed: 0,
                    row_depth: 0,
                    window: None,
                }],
                ..Program::default()
            }),
        );
        let h = alloc(t, 2);
        objects::set_prng_seed(h, 0xA11A_5EED);
        let c = collections::from_words(&shape(), initial);
        assert!(objects::field_set(h, slot(0), &[c]));
        h
    }

    /// LRM 18.4: `data.size == len` with `len inside {[2:4]}` and every
    /// element above its index. The array is resized and each element drawn.
    #[test]
    fn a_size_constraint_resizes_and_randomizes_every_element() {
        let size_eq = bin(
            BinOp::Eq,
            node(ArrayNode::Size(0)),
            Expr::Resize(Box::new(Expr::Var(0, u8t())), s32()),
            Ty::BIT,
        );
        let lo = bin(BinOp::Ge, Expr::Var(0, u8t()), k(u8t(), 2), Ty::BIT);
        let hi = bin(BinOp::Le, Expr::Var(0, u8t()), k(u8t(), 4), Ty::BIT);
        let each = node(ArrayNode::Foreach {
            array: 0,
            var: 0,
            body: Box::new(bin(
                BinOp::Gt,
                Expr::Resize(Box::new(elem(0, lp(0))), s32()),
                lp(0),
                Ty::BIT,
            )),
        });
        let h = setup(0x7a00_0001, vec![size_eq, lo, hi, each], &[9]);
        let mut sizes = std::collections::BTreeSet::new();
        for _ in 0..60 {
            assert_eq!(randomize(h, &[]), Outcome::Solved);
            let a = contents(h);
            let mut len = [0u64];
            assert!(objects::field_get(h, slot(1), &mut len));
            assert_eq!(a.len() as u64, len[0], "size == len");
            assert!((2..=4).contains(&a.len()));
            for (i, v) in a.iter().enumerate() {
                assert!(*v > i as u64, "element {i} = {v}");
            }
            sizes.insert(a.len());
        }
        assert_eq!(sizes.len(), 3, "every size 2..=4 is reached: {sizes:?}");
        release(h);
    }

    /// An array with no size constraint keeps its size; its elements are
    /// still drawn (LRM 18.4).
    #[test]
    fn an_unsized_array_keeps_its_length_but_gets_new_elements() {
        let each = node(ArrayNode::Foreach {
            array: 0,
            var: 0,
            body: Box::new(bin(BinOp::Ge, elem(0, lp(0)), k(u8t(), 200), Ty::BIT)),
        });
        let h = setup(0x7a00_0002, vec![each], &[1, 2, 3]);
        assert_eq!(randomize(h, &[]), Outcome::Solved);
        let a = contents(h);
        assert_eq!(a.len(), 3);
        assert!(a.iter().all(|v| *v >= 200), "{a:?}");
        release(h);
    }

    /// `rand_mode(0)` on the array makes it state: untouched, and its current
    /// elements are what the constraints read.
    #[test]
    fn an_inactive_array_is_state_and_unchanged() {
        let sum = node(ArrayNode::Reduce {
            op: ReduceOp::Sum,
            array: 0,
            var: 0,
            index_var: 1,
            body: Box::new(Expr::Resize(
                Box::new(node(ArrayNode::Loop(0, u8t()))),
                s32(),
            )),
        });
        // len == a.sum()
        let c = bin(
            BinOp::Eq,
            Expr::Resize(Box::new(Expr::Var(0, u8t())), s32()),
            sum,
            Ty::BIT,
        );
        let h = setup(0x7a00_0003, vec![c], &[3, 4, 5]);
        let mut m = objects::rand_meta(h).unwrap();
        m.rand_mode[0] = false;
        objects::set_rand_meta(h, m);
        assert_eq!(randomize(h, &[]), Outcome::Solved);
        assert_eq!(contents(h), vec![3, 4, 5]);
        let mut len = [0u64];
        assert!(objects::field_get(h, slot(1), &mut len));
        assert_eq!(len[0], 12);
        release(h);
    }

    /// An element read outside the array is its own loud outcome, and the
    /// failed call changes nothing (not the array, not the seed).
    #[test]
    fn an_out_of_range_element_fails_loudly_and_changes_nothing() {
        let c = bin(BinOp::Eq, elem(0, k(s32(), 7)), k(u8t(), 1), Ty::BIT);
        let h = setup(0x7a00_0004, vec![c], &[1, 2]);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h, &[]), Outcome::ArrayIndexOutOfRange);
        assert_eq!(contents(h), vec![1, 2]);
        assert_eq!(objects::prng_seed(h), seed);
        release(h);
    }

    /// Sizes that satisfy the size constraint alone but not the elements are
    /// retried: `size inside {[1:3]}` and `a[2] == 5` only works for size 3.
    #[test]
    fn a_size_that_fails_the_element_constraints_is_retried() {
        let lo = bin(BinOp::Ge, node(ArrayNode::Size(0)), k(s32(), 1), Ty::BIT);
        let hi = bin(BinOp::Le, node(ArrayNode::Size(0)), k(s32(), 3), Ty::BIT);
        // `size > 2 -> a[2] == 5` would be a guard; use the unconditional form
        // under a size guard so a smaller size is merely unsatisfiable.
        let guarded = Expr::Guard(
            Box::new(bin(
                BinOp::Gt,
                node(ArrayNode::Size(0)),
                k(s32(), 2),
                Ty::BIT,
            )),
            Box::new(bin(BinOp::Eq, elem(0, k(s32(), 2)), k(u8t(), 5), Ty::BIT)),
            Box::new(k(Ty::BIT, 0)),
            Ty::BIT,
        );
        let h = setup(0x7a00_0005, vec![lo, hi, guarded], &[]);
        for _ in 0..20 {
            assert_eq!(randomize(h, &[]), Outcome::Solved);
            let a = contents(h);
            assert_eq!(a.len(), 3);
            assert_eq!(a[2], 5);
        }
        release(h);
    }

    #[test]
    fn an_impossible_size_is_unsatisfiable_not_an_error() {
        let c = bin(BinOp::Lt, node(ArrayNode::Size(0)), k(s32(), 0), Ty::BIT);
        let h = setup(0x7a00_0006, vec![c], &[1]);
        assert_eq!(randomize(h, &[]), Outcome::Unsatisfiable);
        assert_eq!(contents(h), vec![1]);
        release(h);
    }

    /// LRM 18.4: "The size and index values of an associative array are not
    /// randomizable": a `rand` associative array keeps its keys (and its
    /// `default:`), and every value at those keys is drawn again.
    #[test]
    fn a_rand_associative_array_keeps_its_keys_and_redraws_its_values() {
        use crate::collections::Key;
        let t = ClassTemplateId(0x7a00_0007);
        register_rand_props(
            t,
            vec![RandProp {
                slot: slot(0),
                kind: RandKind::Rand,
            }],
        );
        register_program(
            t,
            Ok(Program {
                arrays: vec![ProgArray {
                    elem_ty: u8t(),
                    elem_words: 1,
                    slot: slot(0),
                    home: Home::Instance,
                    rand: true,
                    prop_index: Some(0),
                    elem_domain: None,
                    assoc: true,
                    nested: false,
                    template_of: None,
                    inner_fixed: 0,
                    row_depth: 0,
                    window: None,
                }],
                ..Program::default()
            }),
        );
        let h = alloc(t, 1);
        objects::set_prng_seed(h, 0xA550_0001);
        let src = collections::frozen_map(
            vec![
                (Key::Int(7), vec![1]),
                (Key::Int(3), vec![1]),
                (Key::Int(40), vec![1]),
            ],
            Some(vec![9]),
        );
        let c = collections::clone(src);
        assert!(objects::field_set(h, slot(0), &[c]));
        let mut seen = std::collections::BTreeSet::new();
        for _ in 0..30 {
            assert_eq!(randomize(h, &[]), Outcome::Solved);
            let mut b = [0u64];
            assert!(objects::field_get(h, slot(0), &mut b));
            assert_eq!(
                collections::keys(b[0]),
                vec![Key::Int(3), Key::Int(7), Key::Int(40)],
                "the keys never change"
            );
            assert_eq!(collections::size(b[0]), 3);
            let mut dflt = [0u64];
            assert!(collections::lookup(b[0], &Key::Int(1000), &mut dflt));
            assert_eq!(dflt[0], 9, "the default survives");
            for e in collections::elements(b[0]) {
                seen.insert(e[0]);
            }
        }
        assert!(seen.len() > 20, "the values are redrawn: {seen:?}");
        release(h);
    }
}

/// Constraint blocks and rand variables switched off through `constraint_mode()` /
/// `rand_mode()` (Task C20; LRM 18.8, 18.9).
#[cfg(test)]
mod mode_tests {
    use super::tests::{bin, get, k, setup, u, var};
    use super::*;
    use crate::constraints::ir::BinOp;
    use crate::objects::{alloc, register_rand_props, release};

    fn slot(offset: usize) -> FieldSlot {
        FieldSlot { offset, words: 1 }
    }

    fn randomize(h: u64) -> Outcome {
        super::randomize(h, &[])
    }

    /// Re-registers `t`'s program with `blocks` over its conjuncts.
    fn with_blocks(t: ClassTemplateId, blocks: Vec<ProgBlock>) {
        let mut p = program(t).unwrap().as_ref().clone().unwrap();
        p.blocks = blocks;
        register_program(t, Ok(p));
    }

    fn block(home: Home, ordinal: u32, conjuncts: std::ops::Range<usize>) -> ProgBlock {
        ProgBlock {
            home,
            ordinal,
            conjuncts,
            items: BlockItems::default(),
        }
    }

    /// LRM 18.9: `constraint_mode(0)` leaves a block out of the solve, and only
    /// that block; switching it on again restores it.
    #[test]
    fn a_constraint_block_switched_off_is_left_out_of_the_solve() {
        // block 0: x0 > 200; block 1: x0 < 100: together unsatisfiable.
        let c = vec![
            bin(BinOp::Gt, var(0, u(8)), k(u(8), 200), Ty::BIT),
            bin(BinOp::Lt, var(0, u(8)), k(u(8), 100), Ty::BIT),
        ];
        let (t, h) = setup(0x7c00_0001, 1, c);
        with_blocks(
            t,
            vec![
                block(Home::Instance, 0, 0..1),
                block(Home::Instance, 1, 1..2),
            ],
        );
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        assert!(objects::set_constraint_mode_of(h, 0, false));
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert!(get(h, 0) < 100, "block 1 still holds");
        }
        assert!(objects::set_constraint_mode_of(h, 0, true));
        assert!(objects::set_constraint_mode_of(h, 1, false));
        for _ in 0..20 {
            assert_eq!(randomize(h), Outcome::Solved);
            assert!(get(h, 0) > 200, "block 0 holds again, block 1 is off");
        }
        assert!(objects::set_constraint_mode_of(h, 1, true));
        assert_eq!(randomize(h), Outcome::Unsatisfiable);
        release(h);
    }

    /// The modes are per object: switching a block off on one instance changes
    /// no other.
    #[test]
    fn constraint_mode_is_per_object() {
        let c = vec![
            bin(BinOp::Gt, var(0, u(8)), k(u(8), 200), Ty::BIT),
            bin(BinOp::Lt, var(0, u(8)), k(u(8), 100), Ty::BIT),
        ];
        let (t, a) = setup(0x7c00_0002, 1, c);
        with_blocks(
            t,
            vec![
                block(Home::Instance, 0, 0..1),
                block(Home::Instance, 1, 1..2),
            ],
        );
        let b = alloc(t, 2);
        objects::set_prng_seed(b, 7);
        assert!(objects::set_constraint_mode_of(a, 0, false));
        assert_eq!(randomize(a), Outcome::Solved);
        assert_eq!(randomize(b), Outcome::Unsatisfiable);
        release(a);
        release(b);
    }

    /// LRM 18.9: a `static` block's mode lives in the class, so it is read from
    /// the static-property object, and every instance sees it.
    #[test]
    fn a_static_blocks_mode_is_shared_by_every_instance() {
        let c = vec![
            bin(BinOp::Gt, var(0, u(8)), k(u(8), 200), Ty::BIT),
            bin(BinOp::Lt, var(0, u(8)), k(u(8), 100), Ty::BIT),
        ];
        let (t, a) = setup(0x7c00_0004, 1, c);
        with_blocks(
            t,
            vec![
                block(Home::Static(9), 0, 0..1),
                block(Home::Instance, 1, 1..2),
            ],
        );
        let b = alloc(t, 2);
        objects::set_prng_seed(b, 11);
        let st = alloc(ClassTemplateId(0x7c00_0104), 1);
        let pairs = [(9u32, st)];
        assert_eq!(super::randomize(a, &pairs), Outcome::Unsatisfiable);
        assert!(objects::set_constraint_mode_of(st, 0, false));
        assert_eq!(super::randomize(a, &pairs), Outcome::Solved);
        assert_eq!(super::randomize(b, &pairs), Outcome::Solved);
        // A call site that did not pass the static object cannot see its mode.
        assert_eq!(super::randomize(a, &[]), Outcome::Unsatisfiable);
        release(a);
        release(b);
        release(st);
    }

    /// LRM 18.8: a `static` `rand` variable switched off through any instance
    /// is state for every instance's call.
    #[test]
    fn a_static_rand_mode_is_shared_and_makes_the_variable_state() {
        let t = ClassTemplateId(0x7c00_0005);
        register_rand_props(t, Vec::new());
        register_program(
            t,
            Ok(Program {
                vars: vec![ProgVar {
                    ty: u(8),
                    slot: slot(0),
                    home: Home::Static(5),
                    prop_index: None,
                    domain_conjunct: None,
                    randc: false,
                    window: None,
                }],
                conjuncts: vec![bin(BinOp::Gt, var(0, u(8)), k(u(8), 200), Ty::BIT)],
                ..Program::default()
            }),
        );
        let a = alloc(t, 1);
        objects::set_prng_seed(a, 3);
        let st = alloc(ClassTemplateId(0x7c00_0105), 1);
        let pairs = [(5u32, st)];
        assert!(objects::field_set(st, slot(0), &[7]));
        // Active: the constraint redraws it above 200.
        assert_eq!(super::randomize(a, &pairs), Outcome::Solved);
        assert!(get(st, 0) > 200);
        // Off: it is a constant 7, so `> 200` fails and the value is kept.
        assert!(objects::field_set(st, slot(0), &[7]));
        assert!(objects::set_static_rand_mode(st, 0, false));
        assert_eq!(super::randomize(a, &pairs), Outcome::Unsatisfiable);
        assert_eq!(get(st, 0), 7);
        assert!(objects::set_static_rand_mode(st, 0, true));
        assert_eq!(super::randomize(a, &pairs), Outcome::Solved);
        release(a);
        release(st);
    }
}

/// Functions called from constraints (Task C13; LRM 18.5.11).
#[cfg(test)]
mod func_tests {
    use super::*;
    use crate::constraints::func::{Stmt, tests::count_ones};
    use crate::constraints::ir::{ArrayNode, BinOp};
    use crate::objects::{RandKind, RandProp, alloc, register_rand_props, release};

    fn u(w: u32) -> Ty {
        Ty::unsigned(w)
    }
    fn s32() -> Ty {
        Ty::signed(32)
    }
    fn var(i: u32, t: Ty) -> Expr {
        Expr::Var(i, t)
    }
    fn k(t: Ty, v: u64) -> Expr {
        Expr::constant(t, v)
    }
    fn bin(op: BinOp, a: Expr, b: Expr, t: Ty) -> Expr {
        Expr::Binary(op, Box::new(a), Box::new(b), t)
    }
    fn widen(x: Expr, t: Ty) -> Expr {
        Expr::Resize(Box::new(x), t)
    }
    fn call(func: u32, args: Vec<Expr>, ty: Ty) -> Expr {
        Expr::Array(ArrayNode::Call { func, args, ty })
    }
    fn slot(o: usize) -> FieldSlot {
        FieldSlot {
            offset: o,
            words: 1,
        }
    }

    /// `function byte twice(byte y); twice = y + y; endfunction`
    fn twice() -> Func {
        Func {
            name: "twice".into(),
            slots: vec![u(8), u(8)],
            n_params: 1,
            ret: 1,
            body: vec![Stmt::Assign(
                1,
                bin(BinOp::Add, var(0, u(8)), var(0, u(8)), u(8)),
            )],
        }
    }

    /// A function that always returns 0.
    fn zero() -> Func {
        Func {
            name: "zero".into(),
            slots: vec![u(8), u(8)],
            n_params: 1,
            ret: 1,
            body: vec![Stmt::Assign(1, k(u(8), 0))],
        }
    }

    /// `n` 8-bit rand fields at words `0..n`; the constraints and functions
    /// are the test's.
    fn setup(id: u32, n: usize, funcs: Vec<Func>, conjuncts: Vec<Expr>) -> u64 {
        let t = ClassTemplateId(id);
        register_rand_props(
            t,
            (0..n)
                .map(|i| RandProp {
                    slot: slot(i),
                    kind: RandKind::Rand,
                })
                .collect(),
        );
        register_program(
            t,
            Ok(Program {
                vars: (0..n)
                    .map(|i| ProgVar {
                        ty: u(8),
                        slot: slot(i),
                        home: Home::Instance,
                        prop_index: Some(i),
                        domain_conjunct: None,
                        randc: false,
                        window: None,
                    })
                    .collect(),
                conjuncts,
                funcs,
                ..Program::default()
            }),
        );
        let h = alloc(t, n);
        objects::set_prng_seed(h, 0xF00D_0001);
        h
    }

    fn get(h: u64, off: usize) -> u64 {
        let mut b = [0u64];
        assert!(objects::field_get(h, slot(off), &mut b));
        b[0]
    }

    /// LRM 18.5.11 C1: `len == count_ones(v)`. The argument `v` is solved
    /// first (uniform over its 256 values), so `len` follows it; `len` is
    /// binomial (4 is far likelier than 0), not uniform over its values.
    #[test]
    fn a_return_value_follows_its_argument_which_is_solved_first() {
        // v = var 0, len = var 1.
        let c = bin(
            BinOp::Eq,
            widen(var(1, u(8)), s32()),
            call(0, vec![widen(var(0, u(8)), u(10))], s32()),
            Ty::BIT,
        );
        let h = setup(0x7a00_0008, 2, vec![count_ones()], vec![c]);
        let mut by_len = [0u32; 9];
        for _ in 0..400 {
            assert_eq!(randomize(h, &[]), Outcome::Solved);
            let (v, len) = (get(h, 0), get(h, 1));
            assert_eq!(len, u64::from(v.count_ones()), "len == count_ones({v})");
            by_len[len as usize] += 1;
        }
        assert!(by_len[4] > 60, "len 4 is the likeliest: {by_len:?}");
        assert!(by_len[0] < 10, "len 0 needs v == 0: {by_len:?}");
        release(h);
    }

    /// LRM 18.5.11: `x <= F(y)` with `y inside {2, 4, 8}` solves `y` first,
    /// so each `y` is drawn with probability 1/3 whatever number of `x` it
    /// admits (a joint solve would favour 8, 17 of 31 pairs).
    #[test]
    fn the_argument_is_drawn_uniformly_before_the_variable_it_bounds() {
        // x = var 0, y = var 1.
        let le = bin(
            BinOp::Le,
            widen(var(0, u(8)), u(8)),
            call(0, vec![var(1, u(8))], u(8)),
            Ty::BIT,
        );
        let y = var(1, u(8));
        let inside = [2u64, 4, 8]
            .into_iter()
            .map(|v| bin(BinOp::Eq, y.clone(), k(u(8), v), Ty::BIT))
            .reduce(|a, b| bin(BinOp::LogOr, a, b, Ty::BIT))
            .unwrap();
        let h = setup(0x7a00_0009, 2, vec![twice()], vec![le, inside]);
        let mut hits = [0u32; 3];
        for _ in 0..300 {
            assert_eq!(randomize(h, &[]), Outcome::Solved);
            let (x, y) = (get(h, 0), get(h, 1));
            assert!(x <= 2 * y, "x={x} y={y}");
            hits[match y {
                2 => 0,
                4 => 1,
                8 => 2,
                other => panic!("y = {other}"),
            }] += 1;
        }
        assert!(
            hits.iter().all(|&n| n > 75),
            "each y about a third of the time: {hits:?}"
        );
        release(h);
    }

    /// LRM 18.5.11: "a circular dependency ... shall be an error".
    #[test]
    fn a_circular_implicit_order_is_a_loud_outcome() {
        let cs = vec![
            bin(
                BinOp::Eq,
                var(0, u(8)),
                call(0, vec![var(1, u(8))], u(8)),
                Ty::BIT,
            ),
            bin(
                BinOp::Eq,
                var(1, u(8)),
                call(0, vec![var(0, u(8))], u(8)),
                Ty::BIT,
            ),
        ];
        let h = setup(0x7a00_000a, 2, vec![twice()], cs);
        let seed = objects::prng_seed(h);
        assert_eq!(randomize(h, &[]), Outcome::ImplicitOrderCycle);
        assert_eq!(objects::prng_seed(h), seed, "a failed call leaves the seed");
        release(h);
    }

    /// A check over one stage that no draw satisfies is a loud outcome, not a
    /// hang or a quiet pick.
    #[test]
    fn an_unsatisfiable_check_is_function_search_not_a_wrong_value() {
        let c = bin(
            BinOp::Eq,
            call(0, vec![var(0, u(8))], u(8)),
            k(u(8), 1),
            Ty::BIT,
        );
        let h = setup(0x7a00_000b, 1, vec![zero()], vec![c]);
        assert_eq!(randomize(h, &[]), Outcome::FunctionSearch);
        release(h);
    }

    /// A check some draws satisfy is solved by rejection sampling.
    #[test]
    fn a_satisfiable_check_is_found_by_sampling() {
        // twice(x) == 6: x is 3 (or 131, the byte wraps).
        let c = bin(
            BinOp::Eq,
            call(0, vec![var(0, u(8))], u(8)),
            k(u(8), 6),
            Ty::BIT,
        );
        let h = setup(0x7a00_000c, 1, vec![twice()], vec![c]);
        for _ in 0..10 {
            assert_eq!(randomize(h, &[]), Outcome::Solved);
            assert!(matches!(get(h, 0), 3 | 131));
        }
        release(h);
    }
}

/// `std::randomize()`: solving a spec with no object (Task C21; LRM 18.12).
#[cfg(test)]
mod scope_tests {
    use super::tests::{bin, k, u, var};
    use super::*;
    use crate::constraints::ir::BinOp;

    fn scope_var(offset: usize, width: u32) -> ProgVar {
        ProgVar {
            ty: u(width),
            slot: FieldSlot {
                offset,
                words: (2 * width as usize).div_ceil(64).max(1),
            },
            home: Home::Instance,
            prop_index: None,
            domain_conjunct: None,
            randc: false,
            window: None,
        }
    }

    fn captured_state(width: u32) -> ProgState {
        ProgState {
            class_of: false,
            root_bit: 0,
            ty: u(width),
            slot: FieldSlot {
                offset: 0,
                words: 1,
            },
            home: Home::Instance,
            via: Vec::new(),
            window: None,
        }
    }

    fn register(vars: Vec<ProgVar>, states: Vec<ProgState>, conjuncts: Vec<Expr>) -> u32 {
        let captures = states
            .iter()
            .enumerate()
            .map(|(i, s)| Capture {
                state: i as u32,
                width: s.ty.width,
            })
            .collect();
        register_spec(Spec {
            frag: Program {
                vars,
                states,
                conjuncts,
                ..Program::default()
            },
            captures,
            only: None,
        })
    }

    fn lt(a: Expr, b: Expr) -> Expr {
        bin(BinOp::Lt, a, b, Ty::BIT)
    }

    #[test]
    fn a_scope_randomize_solves_without_any_object_and_returns_the_values() {
        // a < b, b <= 10: the two variables at words 0 and 1 of the output
        let id = register(
            vec![scope_var(0, 8), scope_var(1, 8)],
            Vec::new(),
            vec![
                lt(var(0, u(8)), var(1, u(8))),
                bin(BinOp::Le, var(1, u(8)), k(u(8), 10), Ty::BIT),
            ],
        );
        let mut distinct = std::collections::BTreeSet::new();
        for seed in 1..60u64 {
            let mut out = [0xffu64; 2];
            assert_eq!(randomize_scope(id, &[], &mut out, seed), Outcome::Solved);
            assert!(out[0] < out[1] && out[1] <= 10, "{out:?}");
            distinct.insert((out[0], out[1]));
        }
        assert!(
            distinct.len() > 10,
            "the draw follows the seed: {distinct:?}"
        );
    }

    #[test]
    fn the_same_seed_draws_the_same_values() {
        let id = register(
            vec![scope_var(0, 16)],
            Vec::new(),
            vec![lt(var(0, u(16)), k(u(16), 1000))],
        );
        let (mut a, mut b) = ([0u64], [0u64]);
        assert_eq!(randomize_scope(id, &[], &mut a, 77), Outcome::Solved);
        assert_eq!(randomize_scope(id, &[], &mut b, 77), Outcome::Solved);
        assert_eq!(a, b);
    }

    #[test]
    fn captured_locals_are_constants_of_the_solve() {
        // x == s + 1 with s captured
        let id = register(
            vec![scope_var(0, 8)],
            vec![captured_state(8)],
            vec![bin(
                BinOp::Eq,
                var(0, u(8)),
                bin(BinOp::Add, Expr::State(0, u(8)), k(u(8), 1), u(8)),
                Ty::BIT,
            )],
        );
        for s in [0u64, 41, 200] {
            let mut out = [0u64];
            assert_eq!(randomize_scope(id, &[s], &mut out, 5), Outcome::Solved);
            assert_eq!(out[0], s + 1);
        }
    }

    #[test]
    fn an_unsatisfiable_scope_randomize_writes_nothing() {
        let id = register(
            vec![scope_var(0, 8)],
            Vec::new(),
            vec![
                bin(BinOp::Gt, var(0, u(8)), k(u(8), 5), Ty::BIT),
                lt(var(0, u(8)), k(u(8), 3)),
            ],
        );
        let mut out = [0x77u64];
        assert_eq!(
            randomize_scope(id, &[], &mut out, 1),
            Outcome::Unsatisfiable
        );
        assert_eq!(out, [0x77], "a failed randomize changes nothing (18.6.1)");
    }

    #[test]
    fn with_no_variable_the_call_is_a_checker() {
        // x < y over two captured locals
        let id = register(
            Vec::new(),
            vec![captured_state(8), captured_state(8)],
            vec![lt(Expr::State(0, u(8)), Expr::State(1, u(8)))],
        );
        let mut none: [u64; 0] = [];
        assert_eq!(randomize_scope(id, &[3, 9], &mut none, 1), Outcome::Solved);
        assert_eq!(
            randomize_scope(id, &[9, 3], &mut none, 1),
            Outcome::Unsatisfiable
        );
        assert_eq!(
            randomize_scope(id, &[4, 4], &mut none, 1),
            Outcome::Unsatisfiable
        );
    }

    #[test]
    fn an_unknown_bit_in_a_captured_local_is_an_error_not_a_value() {
        let id = register(
            Vec::new(),
            vec![captured_state(8)],
            vec![lt(Expr::State(0, u(8)), k(u(8), 9))],
        );
        let mut none: [u64; 0] = [];
        // bit 0 of the 8-bit local is X: its unknown mask (the upper half) is set
        let x_bit = 1u64 << 8;
        assert_eq!(
            randomize_scope(id, &[x_bit], &mut none, 1),
            Outcome::StateUnknown
        );
    }

    #[test]
    fn a_wide_variable_spans_words_and_keeps_its_pinned_bits() {
        // a 70-bit variable: 140 packed bits = 3 words; its top 6 bits == 0x2a
        let wide = scope_var(0, 70);
        assert_eq!(wide.slot.words, 3);
        let top = bin(
            BinOp::Eq,
            Expr::Slice(Box::new(var(0, u(70))), 64, u(6)),
            k(u(6), 0x2a),
            Ty::BIT,
        );
        let id = register(vec![wide], Vec::new(), vec![top]);
        let mut seen_low = std::collections::BTreeSet::new();
        for seed in 1..20u64 {
            let mut out = [0u64; 3];
            assert_eq!(randomize_scope(id, &[], &mut out, seed), Outcome::Solved);
            assert_eq!(out[1] & 0x3f, 0x2a, "{out:x?}");
            assert_eq!(out[2], 0, "no unknown bits: {out:x?}");
            seen_low.insert(out[0]);
        }
        assert!(seen_low.len() > 10, "the other bits are random");
    }

    #[test]
    fn a_call_that_does_not_match_its_spec_fails_loudly() {
        let id = register(
            vec![scope_var(0, 8)],
            vec![captured_state(8)],
            vec![lt(var(0, u(8)), Expr::State(0, u(8)))],
        );
        let spec = spec(id).expect("registered");
        assert_eq!((spec.scope_words(), spec.capture_words()), (1, 1));
        let mut one = [0u64];
        let mut two = [0u64; 2];
        assert_eq!(randomize_scope(id, &[], &mut one, 1), Outcome::Failed);
        assert_eq!(randomize_scope(id, &[5], &mut two, 1), Outcome::Failed);
        assert_eq!(randomize_scope(0, &[], &mut one, 1), Outcome::Failed);
        assert_eq!(randomize_scope(u32::MAX, &[], &mut one, 1), Outcome::Failed);
    }
}