Write constraint for an integer array with 10 elements such that exactly 3 of them are same and rest are unique

In reply to totochan1985:

sum() is one of the array reduction methods (See section 7.12.3 Array reduction methods).

When used in a constraint, these methods get unrolled into a big expression (Section 18.5.8.2 Array reduction iterative constraints)

‘item’ is replaced with each element of the array.

val.sum() with (int'(item==val3))

becomes

int'(val[0]==val3) + int'(val[1]==val3) + int'(val[2]==val3) + ... +int'(val[9]==val3)

The cast to int is needed because otherwise the sum would be limited to 1-bit, which is the result of the equality operator.