souffle icon indicating copy to clipboard operation
souffle copied to clipboard

Assertion failure: `index.isDefined(var.getName()) && "variable not grounded"'

Open adamjseitz opened this issue 2 years ago • 6 comments

Souffle fails an assertion for the example below. This occurs in release 2.3 and latest master (ecee065f54bea9f0caf7b7508b17577948c277ea).

$ souffle -g test.cpp test.dl
souffle: /home/aseitz/Projects/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.
Aborted (core dumped)
.type T = [A:unsigned,B:unsigned]

.decl items(Obj:T)
.input items

.decl ignore_item(A:unsigned)
.input ignore_item

.decl filter_by(Obj:T) inline

.decl filtered_items(Obj:T)
.output filtered_items

filtered_items(Obj):-
    items(Obj),
    filter_by(Obj).

filter_by(Obj):-
    Obj = [A,_],
    !ignore_item(A).

As far as I can tell, this should work - modifying the filter_by rule as follows works fine (but generates a warning for the unused variable B):

filter_by([A,B]):-
    !ignore_item(A).

adamjseitz avatar Jul 12 '22 18:07 adamjseitz

Looks like this may be a duplicate of #2213, but I'll leave this open as it's a somewhat more minimal example.

I am also not sure this is strictly the same issue - I don't see any inline relations there, which seemed to be critical to reproduction in my case.

adamjseitz avatar Jul 12 '22 19:07 adamjseitz

I can confirm that souffle crashes.

b-scholz avatar Jul 18 '22 05:07 b-scholz

This relates to the relaxed semantics of inline relations that permit ungrounded variables.

b-scholz avatar Jul 18 '22 05:07 b-scholz

Note that this program works by inlining by hand.

.type T = [A:unsigned,B:unsigned]

.decl items(Obj:T)
.input items

.decl ignore_item(A:unsigned)
.input ignore_item

.decl filtered_items(Obj:T)
.output filtered_items

filtered_items(X):-
    X = [A,B],
    items(X),
    !ignore_item(A).

b-scholz avatar Jul 18 '22 05:07 b-scholz

The problem is related to the unnamed variable. For example, if you rewrite your code as follows:

.type T = [A:unsigned,B:unsigned]

.decl items(Obj:T)
.input items

.decl ignore_item(A:unsigned)
.input ignore_item

.decl filter_by(Obj:T) inline

.decl filtered_items(Obj:T)
.output filtered_items

filtered_items(Obj):-
    items(Obj),
    filter_by(Obj).

filter_by(Obj):-
    Obj = [A,_B],
    !ignore_item(A).

Using a named unnamed variable will work.

b-scholz avatar Jul 18 '22 05:07 b-scholz

Something goes wrong in the code for ResolveAnonymousRecordAliases.

b-scholz avatar Jul 18 '22 05:07 b-scholz