Aggregates: wrong transformation

[b-scholz]

Aggregates in recursive rules are incorrectly transformed:

.decl point(x:number, y:number)
.input point()

.decl out(r:number, x:number)
.output out
out(0,0).
out(r+1, z) :- r < 30, out(r,_), z = count : { point(x,y), x <= r + 1, x >= -r - 1, y <= r + 1, y >= -r - 1 }.

is transformed to

.decl point(x:number, y:number) 
.decl out(r:number, x:number) 
.decl __agg_body_rel_0(r:number, x:number, y:number,  _0:number,  _1:number,  _2:number,  _3:number) 
out(0,0).

out((r+1),count : { __agg_body_rel_0(r,_,_,_,_,_,_) }) :- 
   r < 30,
   out(r,_).

__agg_body_rel_0(r,x,y, _0, _1, _2, _3) :- 
   point(x,y),
   x <= (r+1),
   x >= (negate(r)-1),
   y <= (r+1),
   y >= (negate(r)-1),
   out(r, _0),
   out(r, _1),
   out(r, _2),
   out(r, _3).
.input point

.output out

[b-scholz]

The issue is that predicate out() appears wrongly in relation __agg_body_rel_0. The domain for argument r is extended using out but out is a recursive relation.

[rdowavic]

The part where it adds out(r, x) to the materialised aggregate body multiple times is a mistake that I need to fix. But other than that, I don't know a clear solution to this. There is nothing but out(r, ) to ground r in the scope of the aggregate.

The user can synthesise their own unary relation to ground r, like Boundary(r), otherwise I can see no way for this aggregate to be materialised and survive.

Like if we did

Boundary(r+1) :- Boundary(r), r < 30.

and then used Boundary to ground r instead of using out(r, _), this would be fine, but I can see that it's annoying.