Cardinality aggterm should not have "1" as a subterm

[Ingmar Dasseville]

As an example of a bad consequence of this, the transformation UnnestDomainTermsFromNonBuiltins introduces unnecessary complexity in the theory

Executing 32UnnestDomainTermsFromNonBuiltins on: 
theory T : mx_voc2 {
  (? var3[s0..3] : ((var3  =  sum(#{ x[getal] : f(x) })) & (var3  =  sum(#{ x[getal] : g(x) })))).
}

Warning: Introduced a variable with sort nat for term 1.
Resulted in: 
theory T : mx_voc2 {
  (? var3[s0..3] : ((var3  =  sum(#{ var4[nat] x[getal] : (=(var4,1) & f(x)) })) & (var3  =  sum(#{ var5[nat] x[getal] : (=(var5,1) & g(x)) })))).
}

This can not easily be fixed without very dirty hacks. The architecture of Aggterms would need a revision for this

[Broes De Cat]

That's not the "real" problem. For generality, cardinalities should preferably always be handled as sum aggregates with term "1" instead of specifying the code for cardinality. Instead, the problem is that for unnesting "1", it should not introduce a type that is too large, but instead make a smaller one consisting of just "1". Apparently, there is no such issue yet.

[Bart Bogaerts]

Zoals het nu is, is het eigenlijk de invariant dat een kardinaliteit altijd term 1 heeft... Deze invariatn wordt geschonden door die 1 te gaan ontnesten dus dat is ook een probleem.

Akkoord: het zou beter zijn om kardinaliteiten intern gewoon als sommen te behandelen...