Aggregation constraints

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,Enumerator,...,Enumerator)
       minimum(Expression,Enumerator,...,Enumerator)
       maximum(Expression,Enumerator,...,Enumerator)

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) > 100

The following constraint ensures that the total number of attribute variables in a that are equal to the variable u must be less than 5:

       sum(1,i in 0..a.length-1, a[i]==u) < 5

When an enumerator constraint cannot be evaluated because some variables have not yet been sufficiently instantiated, the evaluation of sum functions will be delayed.