Module array 

Array constraints (plan C11, C12, C14; LRM 18.4, 18.5.7).

The builder turns A.size, A[i], foreach (A[i]) ... and A.sum() with (...) into array-level IR (ArrayNode) that does not know how many elements A has. Two steps at randomize() time turn that into the plain scalar IR the BDD solver understands:

1. Sizes (solve_sizes). LRM 18.4: “a constraint on the size of a dynamic array or queue … resizes the array”; an array whose size no constraint mentions keeps its size. Every rand-active array whose size appears in a constraint with no element/loop reference gets a 32-bit size variable, and the constraints connected to it (through shared variables) form a small sub-problem solved first.
2. Expansion (expand). With the sizes fixed, foreach unrolls, reductions fold, size is a constant and every element of a rand- active array is a fresh random variable (LRM 18.4: the elements are all randomized); an element of an inactive or non-rand array is a state variable holding its current value.

The size sub-problem cannot see element constraints, so a size that satisfies it may leave the full problem unsatisfiable: the caller blocks that size tuple (solve_sizes’s blocked) and asks again, up to MAX_SIZE_RETRIES times (an exhausted search is its own loud outcome, not “unsatisfiable”).

Limits (stated, not silent)

• An array size is drawn uniformly from the sizes that satisfy its constraints and are at most SIZE_TIERS[0] (1024); if there are none, at most SIZE_TIERS[1] (65536). A constraint that only allows larger sizes is SizeError::TooLarge, never a silent clamp.
• An element index must not depend on a random variable (the builder rejects those); after loop-variable substitution it must be a constant.
• An index outside 0..size where the constraint is live is ExpandError::IndexOutOfRange; one in an arm a constant guard (if (i < A.size-1) A[i] < A[i+1]) never selects is not evaluated.

Structs

ArrayState

One array of a program as seen by one randomize() call.

Expanded

The result of expand.

SizeSolution

The array sizes chosen for one attempt.

Enums

ExpandError

Why expand failed.

SizeError

Why solve_sizes failed.

Constants

MAX_SIZE_RETRIES

How many size tuples solve_sizes is asked to block before the search is declared exhausted.

SIZE_TIERS

Size tiers tried in order (module docs).

Functions

expand

Expands the array-level conjuncts for the array sizes sizes (module docs). n_vars0 is how many field variables the conjuncts already number; element variables are numbered after them. states are the caller’s state values (an element of an inactive array becomes a state appended after them).

expand_with

expand for a program with functions: a call whose arguments the expansion makes fixed (an array size, an element of an inactive array, a state) is evaluated into a constant; a call over random variables stays for the staged solve (super::func_order).

solve_sizes

Chooses the sizes of the rand-active arrays whose size the size-eligible conjuncts constrain (module docs). var_tys[v] is the type of field variable v (conjuncts are over 0..var_tys.len()), states the state values, blocked size tuples ruled out by earlier attempts (in the sized order every call reproduces).