A problem about ungrounded variable

[DerZc]

Hi,

I read the document of Souffle, and find the definition of "ungrounded variable" as "All variables of a rule must be grounded, i.e., a variable must occur at least once as an argument of a positive predicate in the body of a rule."

But I get an assertion of ungrounded variable with this program:

.decl pxsg(A:number, B:number, C:symbol, D:number, E:symbol, F:symbol, G:number, H:float)
.decl rlqm(A:number, B:float, C:symbol, D:float, E:symbol) inline
.decl kyak(A:symbol, B:symbol)
.decl icpa(A:symbol, B:symbol, C:number, D:number, E:symbol, F:float, G:symbol, H:number) no_inline

pxsg(-2, -2, "E", -2, "E", "E", -2, 0).
pxsg(-1, -1, "E", -1, "E", "E", -1, -3.73).
rlqm(-2, 0, "E", 0, "E").
rlqm(-1, -3.73, "E", -3.73, "E").
kyak("E", "E").

icpa(F, G, C, D, F, B, F, C) :- pxsg(C, C, H, C, E, F, D, B), rlqm(C, A, F, B, H), kyak(G, F). 

.output icpa

Run the interpreter and get an assertion failure:

souffle: /souffle/src/ast2ram/seminaive/ValueTranslator.cpp:47: virtual souffle::Own<souffle::ram::Expression> souffle::ast2ram::seminaive::ValueTranslator::visit_(souffle::type_identity<souffle::ast::Variable>, const souffle::ast::Variable&): Assertion `index.isDefined(var.getName()) && "variable not grounded"' failed.

I guess the problem in the no_inline of icpa is conflict with the inline of rlqm. The program can execute correctly if I remove one of them.

I use the latest release version of Souffle.

[DerZc]

Sorry for that this reduced example may not represent the bug very well, because in this example I inline an input, which is not allowed as inlining-limitations describes. Maybe there need a syntax checker for this.

This is the original test case which is same with that in my first edit version:

.decl izxa(A:symbol, B:float, C:number)
.decl xbfg(A:number, B:number, C:float, D:float, E:float, F:float, G:number, H:float) magic brie
.decl sewi(A:symbol)
.decl rlqm(A:number, B:float, C:symbol, D:float, E:symbol) inline brie
.decl yekx(A:number, B:symbol, C:number, D:symbol, E:symbol, F:symbol, G:symbol) btree
.decl opat(A:number, B:symbol) btree
.decl keoy(A:number, B:float, C:number, D:symbol, E:number, F:symbol)
.decl hfoi(A:symbol, B:symbol, C:symbol)
.decl bttn(A:symbol, B:symbol, C:symbol, D:symbol, E:symbol, F:number, G:symbol, H:number) no_magic
.decl tvbr(A:float, B:symbol, C:number) inline brie
.decl unec(A:symbol, B:number, C:number, D:symbol, E:number) btree
.decl pxsg(A:number, B:number, C:symbol, D:number, E:symbol, F:symbol, G:number, H:float) no_inline brie
.decl guvk(A:symbol, B:symbol, C:number, D:symbol)
.decl bjpo(A:float, B:number, C:number, D:symbol, E:float, F:number, G:float, H:number) btree
.decl zumt(A:number, B:symbol, C:number, D:number, E:number, F:symbol)
.decl dfml(A:symbol, B:float, C:symbol, D:float, E:float) brie
.decl vmeg(A:symbol, B:symbol, C:symbol, D:symbol, E:symbol, F:symbol, G:symbol, H:symbol)
.decl kyak(A:symbol, B:symbol) no_magic btree
.decl coyp(A:number, B:symbol, C:symbol, D:symbol, E:symbol, F:number, G:number, H:symbol) btree
.decl icpa(A:symbol, B:symbol, C:number, D:number, E:symbol, F:float, G:symbol, H:number) no_inline brie



izxa("E", 0.0, -2).
izxa("E", -3.73, -1).


xbfg(B, B, A, A, A, A, B, A) :- izxa(C, A, B).
sewi(F) :- xbfg(D, C, A, B, A, A, E, A), izxa(F, B, E).
rlqm(E, A, G, B, G) :- xbfg(E, E, B, A, A, B, E, B), sewi(G).
yekx(B, D, B, C, D, C, D) :- rlqm(B, A, C, A, D), sewi(C).
opat(F, G) :- rlqm(E, A, G, B, G), xbfg(E, F, A, B, C, A, F, A).
keoy(E, C, E, F, E, F) :- sewi(F), xbfg(E, D, B, A, B, C, E, A).
hfoi(B, B, B) :- opat(A, B).
bttn(B, B, B, B, B, A, B, A) :- opat(A, B).
tvbr(A, C, B) :- izxa(C, A, B).
unec(B, A, A, C, A) :- sewi(C), yekx(A, B, A, C, B, B, B).
pxsg(B, C, F, B, F, F, C, A) :- keoy(C, A, B, F, B, D), sewi(E), hfoi(G, F, F).
guvk(C, C, B, C) :- izxa(C, A, B).
bjpo(A, C, C, D, A, C, A, C) :- pxsg(C, C, E, C, F, D, B, A), izxa(E, A, B).
zumt(B, C, B, B, B, C) :- tvbr(A, C, B).
dfml(F, A, G, A, A) :- keoy(C, A, E, F, E, I), yekx(D, I, D, G, G, F, H).
vmeg(B, B, B, B, B, B, B, B) :- hfoi(B, B, B).
kyak(C, C) :- unec(C, A, A, C, B).
coyp(A, B, B, B, B, A, A, B) :- opat(A, B).
icpa(F, G, C, D, F, B, F, C) :- pxsg(C, C, H, C, E, F, D, B), rlqm(C, A, F, B, H), kyak(G, F).

.output icpa

And I re-reduce it：

.decl xbfg(A:number, B:number, C:float, D:float, E:float, F:float, G:number, H:float)
.decl sewi(A:symbol)
.decl rlqm(A:number, B:float, C:symbol, D:float, E:symbol) inline
.decl pxsg(A:number, B:number, C:symbol, D:number, E:symbol, F:symbol, G:number, H:float)
.decl kyak(A:symbol, B:symbol)
.decl icpa(A:symbol, B:symbol, C:number, D:number, E:symbol, F:float, G:symbol, H:number) no_inline

sewi("E").
xbfg(-2, -2, 0, 0, 0, 0, -2, 0).
xbfg(-1, -1, -3.73, -3.73, -3.73, -3.73, -1, -3.73).
pxsg(-2, -2, "E", -2, "E", "E", -2, 0).
pxsg(-1, -1, "E", -1, "E", "E", -1, -3.73).
kyak("E", "E").

rlqm(E, A, G, B, G) :- xbfg(E, E, B, A, A, B, E, B), sewi(G).
icpa(F, G, C, D, F, B, F, C) :- pxsg(C, C, H, C, E, F, D, B), rlqm(C, A, F, B, H), kyak(G, F).

.output icpa

Remove the no_inline of icpa or inline of rlqm, the program can execute correctly.
The version of Souffle is 29c5921. Hope this can help you fix this bug.

[langston-barrett]

@DerZc Not sure how you're minimizing these but you may want to try using a test-case minimization tool like halfempty if you're not already.

[DerZc]

@langston-barrett Good advice, I'll try it out, thank you very much!

[DerZc]

Maybe this test case more useful:

.decl sewi(A:symbol)
.decl rlqm(C:symbol, E:symbol) inline
.decl icpa(C:symbol) no_inline

sewi("E").

rlqm(G, G) :- sewi(G).
icpa(H) :- rlqm(H, H).

.output icpa

There must be two symbols in rlqm to trigger this bug.