Relax overly strict stratification conditions for aggregates

[mkroetzsch]

Aggregations currently need to be stratified, that is: the value of aggregates must not recursively depend on inferences that may still change based on the aggregate value. To ensure this, Nemo requires that all body atoms in aggregation rules are from strictly lower strata.

This condition is too restrictive. It is enough if we ensure that all atoms that contain variables that occur inside the aggregate function are from a lower stratum. The idea is that one could then always split the rule into two: the part of the body that contains the aggregated variables can be moved to an auxiliary rule, the head of which contains the same aggregate and regular (group by) variables that occur in the lower-stratum body at all. The original rule is then modified to use this auxiliary inference in its body, joining it with the remaining (same-stratum) atoms and copying the aggregate value to the head position.

Here is an example program that should work but currently doesn't. Using the method described above, we could rewrite it into the working program. However, this rewriting is not desirable, since it means that we pre-compute the aggregate for cases where it is never relevant. The rule works as it is; we just need to allow it to pass the stratification check.