Difficulty: Medium · Puzzle 6 of 6 · Topic: Constraint Solving Order Puzzles
Compute P(len==4) for BOTH classes under tuple counting. Then compare size_sorted with the same class when the data elements are free in {0,1} (baseline 4/7): why does the ordering constraint reduce the bias toward long arrays?
class size_content;
rand int unsigned len;
rand byte data[];
constraint c {
len inside {[2:4]};
data.size() == len;
foreach (data[i]) data[i] == i;
}
endclass
class size_sorted;
rand int unsigned len;
rand byte data[];
constraint c {
len inside {[2:4]};
data.size() == len;
foreach (data[i]) data[i] inside {[0:1]};
foreach (data[i]) if (i > 0) data[i] >= data[i-1];
}
endclassFor each legal len, count the data arrays that satisfy the foreach constraints, then sum over len.
1) size_content: len in 2..4, and foreach pins data to {0..len-1}. One array per len: 3 tuples, P(len==4)=1/3.
2) size_sorted: data is a non-decreasing 0/1 sequence of length len, i.e. some zeros followed by some ones. There are len+1 such sequences for each len.
3) Tuples: len=2 -> 3, len=3 -> 4, len=4 -> 5, total 12.
4) P(len==4)=5/12 (~41.67%), P(len==2)=3/12=1/4, P(len==3)=1/3. That is more likely than a uniform length (1/3) but less likely than free elements.
5) Without the ordering constraint each len would have 2**len arrays (4+8+16=28 tuples) and P(len==4)=16/28=4/7.Answer: size_content: P(len==4)=1/3 (one array per len). size_sorted: 12 tuples, P(len==4)=5/12. Size and content are solved jointly, and the content constraints decide how many tuples each size owns.
Checked by running a model of the rule in a Python model. Exact enumeration of the constraint set per the LRM (the LRM defines the distribution; simulator solvers need not be uniform). Verilator returned an empty array for this size+foreach shape, so the tuple counts come from enumerating (len, data[]) pairs here.
Assuming longer arrays automatically get more solutions only holds if elements are free (2**len, giving 4/7 for len 4). Pinning the elements gives exactly 1 per len, and the ordering constraint gives only len+1 per len, so the bias towards long arrays shrinks from 4/7 to 5/12. Read it against the right baseline: 5/12 is more likely than a uniform length (1/3) but less likely than free elements (4/7). (Verilator 5.048 returned an empty array for this size+foreach shape, so the counts come from exact enumeration, not from execution.)
How would allowing data[i] inside {[0:1]} with no ordering change len bias? Model answer: each len owns 2**len arrays: 4 + 8 + 16 = 28 tuples, so P(len==2)=4/28=1/7, P(len==3)=8/28=2/7 and P(len==4)=16/28=4/7. The bias towards long arrays becomes strong.
In size_content, foreach pins the data for each length, so there is one array per length, three tuples, and the chance of length four is one third. In size_sorted the data is a non-decreasing zero-one sequence, so length two has three arrays, length three has four and length four has five, twelve in total, and the chance of length four is five twelfths. The trap is assuming longer arrays always own more solutions; that is only true with free elements, where it would be four sevenths. Next I would check the baseline I am comparing against.