Incorrect result with eqrel and magic-transform?

[bertram-gil]

Hi guys,

Consider the following program:

.decl notEqrel(x:number,y:number)
.decl isEqrel(x:number, y:number) eqrel
.decl a__(a:number, b:number) 
.decl b__(a:number) 
.decl c__(a:number, b:number) 

.output c__ // Output relation

notEqrel(x, y) :- isEqrel(x, y).
isEqrel(x, y) :- notEqrel(x, y).
isEqrel(0,1).
notEqrel(1,2).


a__(b, b) :- notEqrel(b, b).

b__(b) :- isEqrel(b, a).

c__(a, c) :- a__(e, g), a__(a, e), b__(e), b__(c).
c__(b, b) :- b__(b).

If I run this program in interpreter mode with --magic-transform=*, I get:

$ ./souffle_ea4eb/src/souffle -w --magic-transform=* prog.dl && cat c__.csv 
0	0
0	1
0	2
1	0
1	1
1	2
2	0
2	1
2	2

If however I add the rule a__(b, b) :- isEqrel(a, b), !isEqrel(a, b). to get the following new program, the result for c__ should not change:

.decl notEqrel(x:number,y:number)
.decl isEqrel(x:number, y:number) eqrel
.decl a__(a:number, b:number) 
.decl b__(a:number) 
.decl c__(a:number, b:number) 

.output c__ // Output relation

notEqrel(x, y) :- isEqrel(x, y).
isEqrel(x, y) :- notEqrel(x, y).
isEqrel(0,1).
notEqrel(1,2).




a__(b, b) :- notEqrel(b, b).
a__(b, b) :- isEqrel(a, b), !isEqrel(a, b).  // new rule

b__(b) :- isEqrel(b, a).

c__(a, c) :- a__(e, g), a__(a, e), b__(e), b__(c).
c__(b, b) :- b__(b).

But I get:

$ ./souffle_ea4eb/src/souffle -w --magic-transform=* new_prog.dl && cat c__.csv 
0	0
0	1
0	2
1	0
1	1
1	2
2	2

Running both programs without --magic-transform=* computes the following for c__:

0	0
0	1
0	2
1	0
1	1
1	2
2	0
2	1
2	2

I am using the latest Souffle revision: ea4ebd4

I believe this bug might be related to this previous bug I reported which is now fixed: #2163

[XiaowenHu96]

em... I couldn't reproduce the result using the master branch.
Could you double-check? And could you make sure the issue only exists in the interpreter mode (Run the example in synthesizer mode with -c)?

[XiaowenHu96]

Sorry I stand corrected (I was using the master branch from my own fork...)
I can confirm the issue exists and only happens in the interpreter mode.
I'll have a look...

[b-scholz]

Magic set transformation won't see the underlying rules of reflexivity, symmetry, and transitivity. We should stop applying a magic set transformation when it encounters an eqrel.