formulog
formulog copied to clipboard
Compiler generates invalid query plans
The Formulog-to-Souffle transpiler generates invalid query plans in the presence of the CODEGEN_PROJECT
relation, which it seems to treat as being in the same stratum as the predicate being defined.
$ cat foo.flg
rel a(i32)
rel b(i32, i32)
b(3, 42).
a(0).
a(1).
a(X + 2) :- a(X), a(X + 1), !b(X + 2, _).
$ java -Doptimize=5 -jar target/formulog-0.7.0-SNAPSHOT-jar-with-dependencies.jar foo.flg -c
$ cd codegen
$ cmake -B build -S .
...
$ cmake --build build
-- Configuring done
-- Generating done
-- Build files have been written to: /root/codegen/build
[ 6%] Generating formulog.cpp
Error: Invalid execution order in plan (expected 2 atoms, not 3) in file formulog.dl at line 30
.plan 0: (1,2,3), 1: (2,1,3)
---------^-------------------
Error: Invalid execution order in plan (expected 2 atoms, not 3) in file formulog.dl at line 30
.plan 0: (1,2,3), 1: (2,1,3)
---------------------^-------
2 errors generated, evaluation aborted
gmake[2]: *** [CMakeFiles/flg.dir/build.make:74: formulog.cpp] Error 1
gmake[1]: *** [CMakeFiles/Makefile2:82: CMakeFiles/flg.dir/all] Error 2
gmake: *** [Makefile:91: all] Error 2
The offending rule in the generated Souffle is
a_(@expr_5(X)) :-
a_(X),
a_(@expr_4(X)),
!CODEGEN_PROJECT_b_10(@expr_5(X)).
.plan 0: (1,2,3), 1: (2,1,3)
Actually, it looks like this bug arises in the case of negation more generally, such as in this program:
rel a(i32)
rel b(i32)
b(2).
a(0).
a(1).
a(X + 2) :- a(X), !b(X).
The invalid query plan is here:
a_(@expr_4(X)) :-
a_(X),
!b_(X).
.plan 0: (1,2)
It works fine if the query plan is changed to
.plan 0: (1)
Surprisingly this program works okay:
rel a(i32)
rel b(i32)
b(2).
a(0).
a(1).
a(X) :- a(X), !b(X).
with the Souffle rule
a_(X) :-
a_(X),
!b_(X).
.plan 0: (1,2)
I'm not sure why Souffle accepts one rule but not the other. The surface difference is that there's a functor call in the head of the rule. Moreover, it seems like it's necessary for the functor call to use a variable to trigger the issue.
Query plans are applied after optimizations (https://github.com/souffle-lang/souffle/issues/2370), and so it risky for us to generate query plans since we do not know what optimizations Souffle will do. A safer alternative is that users specify a SIPS when they compile the Souffle program we generate.