A problem about subsumption

[DerZc]

Hi,

I find a problem in subsumption. Consider the following program:

.decl wfsz(A:float, B:number)
.decl uzud(A:unsigned, B:symbol)
.decl skyf(A:symbol, B:number, C:unsigned)
.decl cmbm(A:number, B:float, C:number, D:number)
.decl buyh(A:number, B:number, C:number, D:unsigned, E:unsigned) inline
.decl xxte(A:symbol, B:unsigned, C:symbol, D:unsigned, E:unsigned) magic
.decl rqmj(A:float, B:number, C:number, D:float, E:float, F:float, G:number, H:float) inline btree
.decl ngfb(A:number, B:float, C:number) brie
.decl fnzy(A:symbol, B:number, C:symbol, D:unsigned, E:symbol, F:symbol, G:number)
.decl ffmn(A:unsigned) magic
.decl xcjc(A:symbol, B:number, C:unsigned, D:unsigned, E:symbol, F:number) brie
.decl sczf(A:float, B:number, C:float)
.decl dirb(A:unsigned, B:float, C:unsigned) btree
.decl hvax(A:number, B:number, C:symbol, D:symbol, E:symbol, F:symbol, G:float, H:symbol) brie
.decl wfxz(A:unsigned, B:unsigned, C:float, D:float, E:float, F:unsigned, G:float, H:float) btree
.decl ibvt(A:float, B:float, C:float, D:unsigned, E:float) magic
.decl uvwt(A:float, B:unsigned, C:number, D:float, E:unsigned, F:float, G:unsigned, H:float) magic brie
.decl qjgu(A:symbol, B:unsigned, C:unsigned, D:unsigned, E:unsigned) brie
.decl mrrv(A:float, B:number, C:number, D:float, E:number, F:number) btree
.decl hjth(A:symbol, B:unsigned) brie
.decl evhv(A:symbol, B:float, C:number, D:symbol, E:float, F:float) magic
.decl bgqw(A:number, B:number, C:unsigned, D:number, E:unsigned, F:number, G:float, H:number) btree
.decl obeu(A:unsigned, B:unsigned, C:symbol)
.decl jrzp(A:unsigned, B:unsigned) no_inline brie
.decl zolw(A:symbol, B:symbol, C:number, D:unsigned, E:number, F:symbol, G:float) brie
.decl rsxv(A:symbol, B:number, C:symbol) btree
.decl nics(A:float, B:number, C:symbol, D:unsigned, E:number) brie
.decl jvvc(A:float, B:number, C:number, D:float, E:number, F:float, G:number, H:float) btree
.decl uqfl(A:unsigned) no_magic brie
.decl jvcx(A:unsigned) brie
.decl kuym(A:number, B:number, C:number, D:symbol) btree
.decl gfjg(A:unsigned, B:float, C:float, D:float, E:number, F:unsigned, G:unsigned)
.decl tdck(A:float, B:float, C:symbol, D:float, E:float) brie
.decl xcgl(A:symbol, B:float, C:float) magic
.decl eozn(A:unsigned, B:symbol)


wfsz(-5.727, -5).
wfsz(4.764, 4).
wfsz(-7.828, 8).
wfsz(-7.609, -9).
wfsz(-2.581, 2).
uzud(0, "h").
uzud(1, "R").
uzud(3, "c").
uzud(3, "m").
uzud(8, "k").
uzud(10, "v").
skyf("D", -2, 6).
skyf("X", 0, 7).
skyf("b", 8, 3).
skyf("9", 0, 7).


cmbm(B, A, B, B) :- wfsz(A, B).
buyh(A, A, A, C, C) :- skyf(B, A, C).
xxte(H, I, H, I, I) :- skyf(H, F, I), cmbm(G, A, _, D), cmbm(C, A, E, G), 1 = 1, 1.584 >= A.
rqmj(A, B, B, A, A, A, B, A) :- wfsz(A, B).
ngfb(E, C, E) :- rqmj(B, E, D, _, C, A, E, C).
fnzy(C, A, C, E, C, C, B) :- buyh(B, A, B, D, E), uzud(D, C).
ffmn(B) :- uzud(B, A), uzud(B, A).
xcjc(E, C, F, G, E, A) :- buyh(D, B, C, G, F), buyh(A, C, B, F, F), skyf(E, B, G).
sczf(A, B, A) :- ngfb(B, A, C), ngfb(C, A, C).
dirb(F, A, F) :- buyh(D, D, C, F, F), rqmj(B, E, D, B, B, B, E, A).
wfxz(G, G, B, B, A*-9.622, G, A, B) :- sczf(A, C, B), buyh(F, E, C, G, G), cmbm(E, B, D, E).
uvwt(A, E, C, A, E, A, E, A) :- ngfb(C, A, B), skyf(D, C, E).
qjgu(B, C, C, C, C) :- xcjc(B, A, C, C, B, A).
mrrv(E, F, F, A, F, F) :- wfsz(D, F), rqmj(E, F, G, E, B, A, F, A), E <= A.
gfjg(E, C, A, C, D, E, E) :- uvwt(C, E, D, _, E, A, E, A).
tdck(A, A, D, A, A) :- mrrv(A, C, C, A, C, C), ffmn(E), qjgu(D, E, E, E, E), C > sum BBB : { ngfb(BBB, AAA, BBB)}.
xcgl(C, B, A) :- tdck(B, A, C, B, B).
eozn(E, D) :- buyh(B, B, B, E, E), xcgl(D, A, A).
eozn(E1, D) <= eozn(E2, D) :- E1>E2.

.output eozn

I run it with souffle -w example.dl and get the result:

3       b
6       b
7       b

As the subsumption eozn(E1, D) <= eozn(E2, D) :- E1>E2., 6 b and 7 b shouldn't appear in the result, right?

I use the last release version of Souffle.

[DerZc]

I get a simplest test case:

.decl buyh(A:number, B:number, C:number, D:unsigned, E:unsigned)
.decl xcgl(A:symbol, B:float, C:float) magic

.decl eozn(A:unsigned, B:symbol)

buyh(-2, -2, -2, 6, 6).
buyh(0, 0, 0, 7, 7).
buyh(8, 8, 8, 3, 3).
xcgl("b", -2.581, -2.581).
xcgl("b", -7.8280000000000003, -7.8280000000000003).
xcgl("b", 4.7640000000000002, 4.7640000000000002).

eozn(E, D) :- buyh(B, B, B, E, E), xcgl(D, A, A).
eozn(E1, D) <= eozn(E2, D) :- E1>E2.

.output eozn

If I remove the magic of xcgl, the result will become correct.

[DerZc]

Maybe this simpler test case more useful:

.decl buyh(A:unsigned) magic
.decl eozn(A:unsigned)

buyh(6).
buyh(7).
buyh(3).

eozn(E) :- buyh(E).
eozn(E1) <= eozn(E2) :- E1<E2.

.output eozn

The correct result should be 7, but I get the result

3
6
7

[b-scholz]

We don't have a theory for subsumption and the magic-set transformation. So subsumptive relations must be excluded from the magic-set operation (similar to equivalence relations) and well spotted!

[b-scholz]

Subsumptive relations need to be added to the set of StronglyIgnoredRelations.