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)
minimum(Expression,EnumeratorConstraint,...,EnumeratorConstraint)
maximum(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 , minimum means the minimum
value, and maximum means the maximum value of 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.