Weird "Ungrounded variable" error reporting

[butterunderflow]

Hey! Thank you for building this powerful language!

I've been learning and hacking about souffle recently.

.decl fib (x : number, result : number) 
fib(1, 1).
fib(2, 1).
fib(x, result) :- 
    x = t1 + 1, fib(t1, r1), 
    x = t2 + 2, fib(t2, r2), 
    temp = r2,
    result = r1 + temp, 
    temp = result - r1, 
    x <= 10.

.output fib

When I try to feed the above Fibonacci program to souffle, it blames a ungrounded error like the below:

Error: Ungrounded variable result in file codegen_fib_error.dl at line 5
fib(x, result) :- 
-------^-----------
1 errors generated, evaluation aborted

That's kind of weird for me, since the "grounded constraints" of result are satisfied as following:

          r1 (grounded, because there's fib(t1, r1))
         /
result 
         \
          temp -- r2 (grounded, because there's fib(t2, r2))

Reported error depends on the order of atoms

What's more weird is, when tweaking the order of some atoms, the souffle's error reporting also changes.

1. Putting temp = r2 at the end won't trigger error:

   .decl fib (x : number, result : number) 
   fib(1, 1).
   fib(2, 1).
   fib(x, result) :- 
   x = t1 + 1, fib(t1, r1), 
   x = t2 + 2, fib(t2, r2), 
   result = r1 + temp, 
   temp = result - r1, 
   temp = r2,   // <--- moved to here
   x <= 10.
   .output fib

2. Changing temp = r2 to r2 = temp and putting it at the end, the error still reported:

   .decl fib (x : number, result : number) 
   fib(1, 1).
   fib(2, 1).
   fib(x, result) :- 
   x = t1 + 1, fib(t1, r1), 
   x = t2 + 2, fib(t2, r2), 
   result = r1 + temp, 
   temp = result - r1, 
   r2 = temp,    // <--- moved to here, and flip the equation
   x <= 10.
   .output fib

   Error: Ungrounded variable result in file codegen_fib_error.dl at line 4
   fib(x, result) :- 
   -------^-----------
   1 errors generated, evaluation aborted

Some exploration of souffle internal

After some exploration, I found that the original program passed the SemanticChecker.cpp, but ResolveAliases.cpp transformed the original program as follows.

- .decl fib (x : number, result : number) 
- fib(1, 1).
- fib(2, 1).
- fib(x, result) :- 
-     x = t1 + 1, fib(t1, r1), 
-     x = t2 + 2, fib(t2, r2), 
-     temp = r2,
-     result = r1 + temp, 
-     temp = result - r1, 
-     x <= 10.
- 
- .output fib
+ .decl fib(x:number, result:number) 
+ fib(1,1).
+ fib(2,1).
+ fib((t2+2),result) :- 
+    (t2+2) = (t1+1),
+    fib(t1,r1),
+    fib(t2,r2),
+    (result-r1) = r2,
+    result = (r1+(result-r1)),
+    (t2+2) <= 10.
+ 
+ .output fib(IO="file",name="fib",operation="output",output-dir=".")

It folds the variable temp into result = r1 + temp and temp = r2 with result - r1, which breaks the grounded constraint between result and temp! Then the GroundedTermsChecker.cpp can't recognize that the result is grounded anymore, and then report the ungrounded error.

Is this a bug or it's an expected "feature"? Thanks for any help or advice.

[quentin]

I am not an expert of this part of the code, but it looks more like a bug of the ResolveAliases pass that may not behave correcly in presence of such circular constraints.

[butterunderflow]

Thank you for responding. Does souffle team have any plan to fix this?

[quentin]

Currently the Souffle project has few active developers. Any help would be appreciated if you want to work on this issue and submit a fix.

[butterunderflow]

Thank you, I'll look further into it later.