Constraints for a queue/array: Need help to understand how to implement this #3 condition

Hi Dave,

Aren’t we restricting the randomization here ?
constraint q_c {
foreach (list[i]) {
if (i< 18 && list[i] == ADD) {
list[i+1] != ADD;
list[i+2] != ADD;
}
There is no restriction for second add instruction here after it gets generated once
if (list[i]==ADD && list[j]==ADD) j-i >= 3;
but here aren’t we restricting the randomization by making at least two add instructions get generated?

Thanks

I’m not sure what you mean by restriction. It might help to unroll a few iterations of the foreach loop. The original example unrolls as follows.

if (list[0]==ADD) { list[1]!=ADD && list[2] !=ADD}
if (list[1]==ADD) { list[2]!=ADD && list[3] !=ADD}
if (list[2]==ADD) { list[3]!=ADD && list[4] !=ADD}
...
if (list[17]==ADD) { list[18]!=ADD && list[19] !=ADD}

My example unrolls as follows

if (list[0]==ADD && list[1]==ADD)  0; //   1-0 >= 3
if (list[0]==ADD && list[2]==ADD)  0; //   2-0 >= 3
if (list[0]==ADD && list[3]==ADD)  1; //   3-0 >= 3
...
if (list[0]==ADD && list[19]==ADD)  1; //   19-0 >= 3
if (list[1]==ADD && list[2]==ADD)   0; //   2-1 >= 3
if (list[1]==ADD && list[3]==ADD)   0; //   3-1 >= 3
if (list[1]==ADD && list[4]==ADD)   1; //   4-1 >= 3
...
if (list[2]==ADD && list[3]==ADD)   0; //   3-2 >= 3
...

Remember that these are Boolean implications. If the left-hand side (LHS) expression inside the parentheses is true, the right-hand side (RHS) constraint must also be true. However, if the LHS is false, the RHS can be either true or false. In other words, if the RHS is true, there’s no obligation for the LHS to be true as well.