Some times we want to impose constraints on aggregations of arrays, such as the sum of a group of variables and the number of appearances of a value in of a group of attribute variables. For this purpose, we use the aggregation expression in the following form:
sum(Expression,EnumeratorConstraint,...,EnumeratorConstraint)Any attribute variable in Expression must appear at least once in the enumerator constraints. For each tuple of values that satisfy the enumerator constraints, the Expression got a value. The sum function means the sum of all such values for the Expression.
For example, the following constraint ensures that the total of the elements in the attribute array a is greater than 100:
sum(a[i],i in 0..a.length-1) > 100The following constraint ensures that the total number of attribute variables in attrs that are equal to the variable u must be less than 5:
sum(1,i in 0..a.length-1, a[i]==u) < 5When an enumerator constraint cannot be evaluated because some variables have not yet been sufficiently instantiated, the evaluation of sum functions will be delayed.