Maintains a resource usage profile.
Maintains a cluster of the indexes of array: cluster(j) = {i in index of values | values[i] == j} This is considered as a dense cluster because Cluster is an array and must cover all the possibles values of the values in the array values
Maintains a count of the indexes of array: count(j) = #{i in index of values | values[i] == j} This is considered as a dense count because counts is an array and must cover all the possibles values of the values in the array values
maintains the reverse references.
{ i in index(values) | cond(values[i] }
inputarray[index]
Union(i in index) (array[i])
if (ifVar >0) then thenVar else elveVar
inputarray[index] on an array of IntSetVar
This is a helper to define an invariant from an Int -> Int function.
This is a helper to define an invariant from an Int x Int -> Int function.
{i in index of values | values[i] <= boundary} It is based on two heap data structure, hence updates are log(n) and all updates are allowed
{i \in index of values | values[i] <= boundary} It is based on a queue for the values above the boundary, hence all updates must be accepted by this scheme:
maintains a sorting of the values array:
maintains a cluster of the indexes of array: cluster(j) = {i in index of values | values[i] == j} This is considered as a sparse cluster because Cluster is a map and must not cover all possibles values of the values in the array values
This is a helper object for the DenseCluster and SparseCluster invariants.
Helper object for the sort invariant, creates the necessary variables