Incorrect result with range() ?

[bertram-gil]

Hi guys,
Consider the following program:

.decl d_i(x: number) 
.decl b_u(x: unsigned) 
.decl d_u(x: unsigned) 
.decl f_u(x: unsigned)
.decl a(x:number, y:number)
.decl b__(a:number, b:number) 
.decl c__(a:unsigned) 
.decl d__(a:unsigned, b:number) 
.decl g__(a:unsigned)
.output g__ // Output rule
d_i(x) :- x = range(5, 1, 0).
b_u(x) :- x = range(5, 1).
d_u(x) :- x = range(5, 1, 0).
a(x,y) :- x = range(1,3), y = range(1,3).

b__(c, b) :- d_i(b), a(c, c).
c__(a) :- f_u(a).
d__(f, e) :- b__(d, e), !c__(f), b_u(c), d_u(f).
g__(a) :- d__(a, b).

If I run this program in interpreter mode, I get:

$ ./souffle_1be0b/src/souffle -w prog.dl && cat g__.csv
5

If I now add a rule c__(a) :- b_u(a), !b_u(a)., the result in the relation g__ should not change. But if I run the following program:

.decl d_i(x: number) 
.decl b_u(x: unsigned) 
.decl d_u(x: unsigned) 
.decl f_u(x: unsigned)
.decl a(x:number, y:number)
.decl b__(a:number, b:number) 
.decl c__(a:unsigned) 
.decl d__(a:unsigned, b:number) 
.decl g__(a:unsigned)
.output g__ // Output rule
d_i(x) :- x = range(5, 1, 0).
b_u(x) :- x = range(5, 1).
d_u(x) :- x = range(5, 1, 0).
a(x,y) :- x = range(1,3), y = range(1,3).

b__(c, b) :- d_i(b), a(c, c).
c__(a) :- f_u(a).
c__(a) :- b_u(a), !b_u(a).    // ****** New rule *******
d__(f, e) :- b__(d, e), !c__(f), b_u(c), d_u(f).
g__(a) :- d__(a, b).

I get an empty result in g__:

$ ./souffle_1be0b/src/souffle -w prog.dl && cat g__.csv

I am using the latest souffle revision: 1be0bf8

[quentin]

The issue might come from a bug in the computation of unsigned range(5,1) in b_u and this code:

souffle/src/include/souffle/utility/EvaluatorUtil.h

Lines 44 to 47 in 7174f14

	template <typename A, typename F /* Tuple<RamDomain,1> -> void */>
	void runRange(A from, A to, F&& go) {
	return runRange(from, to, A(from <= to ? 1 : -1), std::forward<F>(go));
	}

Since from=5 and to=1 and both are RamUnsigned numbers, the step argument -1 is being converted to RamUnsigned which is probably 4294967295 if RamUnsigned is 32 bits.

Then this code is called with from=5, to=, step=4294967295:

souffle/src/include/souffle/utility/EvaluatorUtil.h

Lines 26 to 32 in 7174f14

	template <typename A, typename F /* Tuple<RamDomain,1> -> void */>
	void runRange(A from, A to, A step, F&& go) {
	#define GO(x) go(Tuple<RamDomain, 1>{ramBitCast(x)})
	if (0 < step) {
	for (auto x = from; x < to; x += step) {
	GO(x);
	}

Since step is positive, the 0 < step branch is taken, but since from=5 > to=1 the for loop is never entered. Hence no fact is inserted in relation b_u.

In your example, replace b_u(x) :- x = range(5, 1). by b_u(x) :- n = range(5,1), x = to_unsigned(n)..