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.

Lowered

The constraints and arrays of the second sizing stage (lower_rows).

RowsState

The rows of an array of dynamic arrays or queues as one randomize() call sees them.

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).

lower_rows

Binds the rows of every array of arrays whose rows are not bound yet, for one stage of the sizing (module docs of ArrayNode::RowScope): sizes are the sizes the stage before chose. Every such array gets one row array per row (the row_base ids), becomes inactive with that many placeholder elements, and the conjuncts name rows directly. A row that is itself an array of arrays (int a[][][]) comes out unlowered, with a template of its own for its rows, and is bound by the next call once its size is chosen.

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).