Sum() function behaviour in constraint

In reply to zalak patel:

Sometimes it helps to unroll the foreach loop and sum() reduction to get a better picture of what is inside it.

Unrolling the foreach:


   arr.sum() with (int'(item==arr[0])) == (arr[0]==d ? 2:1);
   arr.sum() with (int'(item==arr[1])) == (arr[1]==d ? 2:1);
   ...
   arr.sum() with (int'(item==arr[9])) == (arr[9]==d ? 2:1);

Unrolling the sum() on just the first line:

int'(arr[0]==arr[0]) + int'(arr[1]==arr[0]) + int'(arr[2]==arr[0]) ... + int'(arr[9]==arr[0]) 
   == (arr[0]==d ? 2:1);

The sum() is counting the number of times the value of arr[0] appears in the remainder of the array. And the constraint is that value can only appear once or twice depending on the value of d.